diff options
| -rw-r--r-- | src/sat/bsat/satSolver.c | 16 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 8 | ||||
| -rw-r--r-- | src/sat/bsat/satVec.h | 38 |
3 files changed, 57 insertions, 5 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index d4726b81..3904f8b0 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -306,6 +306,15 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); size = end - begin; + + // do not allocate memory for the two-literal problem clause + if ( size == 2 && !learnt ) + { + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1]))); + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0]))); + return NULL; + } + // c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); @@ -336,6 +345,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); +// if ( learnt ) +// printf( "%d ", size ); return c; } @@ -1212,6 +1223,7 @@ void sat_solver_delete(sat_solver* s) int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) { + clause * c; lit *i,*j; int maxvar; lbool* values; @@ -1271,7 +1283,9 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) return enqueue(s,*begin,(clause*)0); // create new clause - vecp_push(&s->clauses,clause_new(s,begin,j,0)); + c = clause_new(s,begin,j,0); + if ( c ) + vecp_push(&s->clauses,c); s->stats.clauses++; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index a67e829a..f500b46b 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -36,7 +36,7 @@ ABC_NAMESPACE_HEADER_START //================================================================================================= // Simple types: - +/* #ifndef __cplusplus #ifndef false # define false 0 @@ -64,7 +64,7 @@ static inline int lit_sign (lit l) { return l & 1; } static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } - +*/ //================================================================================================= // Public interface: @@ -84,14 +84,14 @@ extern int sat_solver_nclauses(sat_solver* s); extern int sat_solver_nconflicts(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); - +/* struct stats_t { ABC_INT64_T starts, decisions, propagations, inspects, conflicts; ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; }; typedef struct stats_t stats_t; - +*/ extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ); diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index 6e604d36..4eedbdd0 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -86,6 +86,44 @@ static inline void vecp_push (vecp* v, void* e) +//================================================================================================= +// Simple types: + +#ifndef __cplusplus +#ifndef false +# define false 0 +#endif +#ifndef true +# define true 1 +#endif +#endif + +typedef int lit; +typedef char lbool; + +static const int var_Undef = -1; +static const lit lit_Undef = -2; + +static const lbool l_Undef = 0; +static const lbool l_True = 1; +static const lbool l_False = -1; + +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } + +struct stats_t +{ + ABC_INT64_T starts, decisions, propagations, inspects, conflicts; + ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; +}; +typedef struct stats_t stats_t; + ABC_NAMESPACE_HEADER_END |