small fixes
This commit is contained in:
parent
518ce92bea
commit
03d8a64543
@ -200,7 +200,7 @@
|
|||||||
|
|
||||||
int getRealNumber(char *c, double *number);
|
int getRealNumber(char *c, double *number);
|
||||||
int getIntNumber(char *c, int *number);
|
int getIntNumber(char *c, int *number);
|
||||||
inline int getPosNumber(char *c, int *number);
|
//inline int getPosNumber(char *c, int *number);
|
||||||
int IsRealNumber(char *c);
|
int IsRealNumber(char *c);
|
||||||
int IsPosNumber(const char *c);
|
int IsPosNumber(const char *c);
|
||||||
int IsNumber(const char *c);
|
int IsNumber(const char *c);
|
||||||
|
@ -188,12 +188,13 @@
|
|||||||
|
|
||||||
//#include <stdio.h>
|
//#include <stdio.h>
|
||||||
//#include <stdlib.h>
|
//#include <stdlib.h>
|
||||||
|
#include <unistd.h>
|
||||||
#include "simplecudd.h"
|
#include "simplecudd.h"
|
||||||
#include "problogmath.h"
|
#include "problogmath.h"
|
||||||
#include <signal.h>
|
#include <signal.h>
|
||||||
#include <time.h>
|
#include <time.h>
|
||||||
|
|
||||||
#define VERSION "2.0.1"
|
#define PROBLOGBDD_VERSION "2.0.1"
|
||||||
|
|
||||||
|
|
||||||
#ifndef max
|
#ifndef max
|
||||||
@ -1550,7 +1551,7 @@ int argtype(const char *arg) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
void printhelp(int argc, char **arg) {
|
void printhelp(int argc, char **arg) {
|
||||||
fprintf(stderr, "\n\nProbLogBDD Tool Version: %s\n\n", VERSION);
|
fprintf(stderr, "\n\nProbLogBDD Tool Version: %s\n\n", PROBLOGBDD_VERSION);
|
||||||
fprintf(stderr, "SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html)\n");
|
fprintf(stderr, "SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html)\n");
|
||||||
fprintf(stderr, "SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be)\n");
|
fprintf(stderr, "SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be)\n");
|
||||||
fprintf(stderr, "Copyright Katholieke Universiteit Leuven 2008\n");
|
fprintf(stderr, "Copyright Katholieke Universiteit Leuven 2008\n");
|
||||||
|
@ -400,7 +400,7 @@ int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd,
|
|||||||
// Cudd_AutodynEnable(mana, CUDD_REORDER_EXACT);
|
// Cudd_AutodynEnable(mana, CUDD_REORDER_EXACT);
|
||||||
// Cudd_ReduceHeap(manager, CUDD_REORDER_SIFT, 1);
|
// Cudd_ReduceHeap(manager, CUDD_REORDER_SIFT, 1);
|
||||||
|
|
||||||
ret = Cudd_DumpDot(manager, 1, f, varmap.vars, NULL, fd);
|
ret = Cudd_DumpDot(manager, 1, f, (const char *const *)varmap.vars, NULL, fd);
|
||||||
fclose(fd);
|
fclose(fd);
|
||||||
return ret;
|
return ret;
|
||||||
}
|
}
|
||||||
|
@ -252,8 +252,8 @@ include_directories (
|
|||||||
)
|
)
|
||||||
|
|
||||||
add_lib(real ${REAL_SOURCES})
|
add_lib(real ${REAL_SOURCES})
|
||||||
link_directories(${R_LIBDIR})
|
|
||||||
target_link_libraries (real R libYap)
|
target_link_libraries (real ${LIBR_SO} libYap)
|
||||||
|
|
||||||
check_include_files( "stdio.h;R.h" HAVE_R_H )
|
check_include_files( "stdio.h;R.h" HAVE_R_H )
|
||||||
check_include_files( "R.h;Rembedded.h" HAVE_R_EMBEDDED_H )
|
check_include_files( "R.h;Rembedded.h" HAVE_R_EMBEDDED_H )
|
||||||
|
@ -63,8 +63,8 @@ Solver::Solver() :
|
|||||||
|
|
||||||
Solver::~Solver()
|
Solver::~Solver()
|
||||||
{
|
{
|
||||||
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
|
for (int i = 0; i < learnts.size(); i++) std::free(learnts[i]);
|
||||||
for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
|
for (int i = 0; i < clauses.size(); i++) std::free(clauses[i]);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@ -163,7 +163,7 @@ void Solver::detachClause(Clause& c) {
|
|||||||
|
|
||||||
void Solver::removeClause(Clause& c) {
|
void Solver::removeClause(Clause& c) {
|
||||||
detachClause(c);
|
detachClause(c);
|
||||||
free(&c); }
|
std::free(&c); }
|
||||||
|
|
||||||
|
|
||||||
bool Solver::satisfied(const Clause& c) const {
|
bool Solver::satisfied(const Clause& c) const {
|
||||||
|
@ -147,7 +147,7 @@ template<class V>
|
|||||||
Clause* Clause_new(const V& ps, bool learnt) {
|
Clause* Clause_new(const V& ps, bool learnt) {
|
||||||
assert(sizeof(Lit) == sizeof(uint32_t));
|
assert(sizeof(Lit) == sizeof(uint32_t));
|
||||||
assert(sizeof(float) == sizeof(uint32_t));
|
assert(sizeof(float) == sizeof(uint32_t));
|
||||||
void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
|
void* mem = std::malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
|
||||||
return new (mem) Clause(ps, learnt); }
|
return new (mem) Clause(ps, learnt); }
|
||||||
/*_________________________________________________________________________________________________
|
/*_________________________________________________________________________________________________
|
||||||
|
|
|
|
||||||
|
@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
|
|||||||
//=================================================================================================
|
//=================================================================================================
|
||||||
// Automatically resizable arrays
|
// Automatically resizable arrays
|
||||||
//
|
//
|
||||||
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
|
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with std::realloc)
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
class vec {
|
class vec {
|
||||||
@ -79,9 +79,9 @@ public:
|
|||||||
|
|
||||||
// Stack interface:
|
// Stack interface:
|
||||||
#if 1
|
#if 1
|
||||||
void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
|
void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)std::realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
|
||||||
//void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
|
//void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)std::realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
|
||||||
void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
|
void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)std::realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
|
||||||
void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
|
void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
|
||||||
#else
|
#else
|
||||||
void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
|
void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
|
||||||
@ -106,7 +106,7 @@ void vec<T>::grow(int min_cap) {
|
|||||||
if (min_cap <= cap) return;
|
if (min_cap <= cap) return;
|
||||||
if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
|
if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
|
||||||
else do cap = (cap*3+1) >> 1; while (cap < min_cap);
|
else do cap = (cap*3+1) >> 1; while (cap < min_cap);
|
||||||
data = (T*)realloc(data, cap * sizeof(T)); }
|
data = (T*)std::realloc(data, cap * sizeof(T)); }
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
void vec<T>::growTo(int size, const T& pad) {
|
void vec<T>::growTo(int size, const T& pad) {
|
||||||
@ -127,7 +127,7 @@ void vec<T>::clear(bool dealloc) {
|
|||||||
if (data != NULL){
|
if (data != NULL){
|
||||||
for (int i = 0; i < sz; i++) data[i].~T();
|
for (int i = 0; i < sz; i++) data[i].~T();
|
||||||
sz = 0;
|
sz = 0;
|
||||||
if (dealloc) free(data), data = NULL, cap = 0; } }
|
if (dealloc) std::free(data), data = NULL, cap = 0; } }
|
||||||
|
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
Reference in New Issue
Block a user