summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/aig/cec/cecSolve.c1
-rw-r--r--src/aig/ivy/ivyFraig.c2
-rw-r--r--src/aig/saig/saigConstr2.c3
-rw-r--r--src/sat/bsat/satSolver.c850
-rw-r--r--src/sat/bsat/satSolver.h135
-rw-r--r--src/sat/bsat/satSolver2.c32
-rw-r--r--src/sat/bsat/satSolver2.h2
-rw-r--r--src/sat/bsat/satSolver_old.c1766
-rw-r--r--src/sat/bsat/satSolver_old.h210
-rw-r--r--src/sat/bsat/satUtil.c4
-rw-r--r--src/sat/bsat/vecRec.h27
11 files changed, 2489 insertions, 543 deletions
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index dc1b88eb..e86c2f35 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -376,6 +376,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
+ p->pSat->factors = ABC_CALLOC( double, 1 );
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const0 node - add the clause
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index b53805b4..f7c0743b 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2113,6 +2113,7 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
+ p->pSat->factors = ABC_CALLOC( double, 1 );
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
@@ -2264,6 +2265,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
+ p->pSat->factors = ABC_CALLOC( double, 1 );
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 6665d9f1..7f2eab6a 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -596,7 +596,8 @@ Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConf
pReprR = Aig_Regular(pRepr);
if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
continue;
- value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+// value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+ value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
if ( value == l_Undef )
continue;
// label this node as taken
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 4d851d0f..5a05e3b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -29,7 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
#define SAT_USE_ANALYZE_FINAL
//=================================================================================================
@@ -77,6 +76,62 @@ static inline int irand(double* seed, int size) {
static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
//=================================================================================================
+// Variable datatype + minor functions:
+
+static const int var0 = 1;
+static const int var1 = 0;
+static const int varX = 3;
+
+struct varinfo_t
+{
+ unsigned val : 2; // variable value
+ unsigned pol : 1; // last polarity
+ unsigned tag : 1; // conflict analysis tag
+ unsigned lev : 28; // variable level
+};
+
+static inline int var_level (sat_solver* s, int v) { return s->levels[v]; }
+static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; }
+static inline int var_polar (sat_solver* s, int v) { return s->polarity[v]; }
+
+static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; }
+static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; }
+static inline void var_set_polar (sat_solver* s, int v, int pol) { s->polarity[v] = pol; }
+
+// variable tags
+static inline int var_tag (sat_solver* s, int v) { return s->tags[v]; }
+static inline void var_set_tag (sat_solver* s, int v, int tag) {
+ assert( tag > 0 && tag < 16 );
+ if ( s->tags[v] == 0 )
+ veci_push( &s->tagged, v );
+ s->tags[v] = tag;
+}
+static inline void var_add_tag (sat_solver* s, int v, int tag) {
+ assert( tag > 0 && tag < 16 );
+ if ( s->tags[v] == 0 )
+ veci_push( &s->tagged, v );
+ s->tags[v] |= tag;
+}
+static inline void solver2_clear_tags(sat_solver* s, int start) {
+ int i, * tagged = veci_begin(&s->tagged);
+ for (i = start; i < veci_size(&s->tagged); i++)
+ s->tags[tagged[i]] = 0;
+ veci_resize(&s->tagged,start);
+}
+
+int sat_solver_get_var_value(sat_solver* s, int v)
+{
+ if ( var_value(s, v) == var0 )
+ return l_False;
+ if ( var_value(s, v) == var1 )
+ return l_True;
+ if ( var_value(s, v) == varX )
+ return l_Undef;
+ assert( 0 );
+ return 0;
+}
+
+//=================================================================================================
// Clause datatype + minor functions:
struct clause_t
@@ -85,7 +140,7 @@ struct clause_t
lit lits[0];
};
-static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
+static inline int clause_nlits (clause* c) { return c->size_learnt >> 1; }
static inline lit* clause_begin (clause* c) { return c->lits; }
static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
@@ -95,23 +150,26 @@ static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned
static inline void clause_print (clause* c) {
int i;
printf( "{ " );
- for ( i = 0; i < clause_size(c); i++ )
+ for ( i = 0; i < clause_nlits(c); i++ )
printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
printf( "}\n" );
}
+static inline clause* clause_read( sat_solver* s, int h ) { return (clause *)Vec_RecEntryP(&s->Mem, h); }
+static inline int clause_size( int nLits, int fLearnt ) { int a = nLits + fLearnt + 1; return a + (a & 1); }
+
//=================================================================================================
// Encode literals in clause pointers:
-static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
-static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); }
-static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); }
+static inline int clause_from_lit (lit l) { return l + l + 1; }
+static inline int clause_is_lit (int h) { return (h & 1); }
+static inline lit clause_read_lit (int h) { return (lit)(h >> 1); }
//=================================================================================================
// Simple helpers:
static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
-static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
//=================================================================================================
// Variable order functions:
@@ -153,49 +211,31 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
{
- int* heap;
- int* orderpos;
-
- lbool* values = s->assigns;
-
+ int* heap = veci_begin(&s->order);
+ int* orderpos = s->orderpos;
// Random decision:
if (drand(&s->random_seed) < random_var_freq){
int next = irand(&s->random_seed,s->size);
assert(next >= 0 && next < s->size);
- if (values[next] == l_Undef)
+ if (var_value(s, next) == varX)
return next;
}
-
// Activity based decision:
-
- heap = veci_begin(&s->order);
- orderpos = s->orderpos;
-
-
while (veci_size(&s->order) > 0){
int next = heap[0];
int size = veci_size(&s->order)-1;
int x = heap[size];
-
veci_resize(&s->order,size);
-
orderpos[next] = -1;
-
if (size > 0){
-
int i = 0;
int child = 1;
-
-
while (child < size){
if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
child++;
-
assert(child < size);
-
if (s->activity[x] >= s->activity[heap[child]])
break;
-
heap[i] = heap[child];
orderpos[heap[i]] = i;
i = child;
@@ -204,12 +244,9 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv
heap[i] = x;
orderpos[heap[i]] = i;
}
-
-//printf( "-%d ", next );
- if (values[next] == l_Undef)
+ if (var_value(s, next) == varX)
return next;
}
-
return var_Undef;
}
@@ -227,9 +264,9 @@ static inline void act_var_rescale(sat_solver* s) {
}
static inline void act_clause_rescale(sat_solver* s) {
static int Total = 0;
- clause** cs = (clause**)vecp_begin(&s->learnts);
+ clause** cs = (clause**)veci_begin(&s->learnts);
int i, clk = clock();
- for (i = 0; i < vecp_size(&s->learnts); i++){
+ for (i = 0; i < veci_size(&s->learnts); i++){
float a = clause_activity(cs[i]);
clause_setactivity(cs[i], a * (float)1e-20);
}
@@ -247,6 +284,8 @@ static inline void act_var_bump(sat_solver* s, int v) {
order_update(s,v);
}
static inline void act_var_bump_global(sat_solver* s, int v) {
+ if ( !s->pGlobalVars )
+ return;
s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
if (s->activity[v] > 1e100)
act_var_rescale(s);
@@ -254,6 +293,8 @@ static inline void act_var_bump_global(sat_solver* s, int v) {
order_update(s,v);
}
static inline void act_var_bump_factor(sat_solver* s, int v) {
+ if ( !s->factors )
+ return;
s->activity[v] += (s->var_inc * s->factors[v]);
if (s->activity[v] > 1e100)
act_var_rescale(s);
@@ -278,6 +319,7 @@ static inline void act_var_rescale(sat_solver* s) {
s->var_inc >>= 19;
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
+/*
static inline void act_clause_rescale(sat_solver* s) {
static int Total = 0;
clause** cs = (clause**)vecp_begin(&s->learnts);
@@ -293,6 +335,7 @@ static inline void act_clause_rescale(sat_solver* s) {
// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
+*/
static inline void act_var_bump(sat_solver* s, int v) {
s->activity[v] += s->var_inc;
if (s->activity[v] & 0x80000000)
@@ -300,30 +343,100 @@ static inline void act_var_bump(sat_solver* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,v);
}
-static inline void act_var_bump_global(sat_solver* s, int v) {}
-static inline void act_var_bump_factor(sat_solver* s, int v) {}
+static inline void act_var_bump_global(sat_solver* s, int v) {
+ if ( !s->pGlobalVars )
+ return;
+ s->activity[v] += (int)(s->var_inc * 3 * s->pGlobalVars[v]);
+ if (s->activity[v] & 0x80000000)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+ if ( !s->factors )
+ return;
+ s->activity[v] += (int)(s->var_inc * s->factors[v]);
+ if (s->activity[v] & 0x80000000)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+/*
static inline void act_clause_bump(sat_solver* s, clause*c) {
unsigned a = clause_activity2(c) + s->cla_inc;
clause_setactivity2(c,a);
if (a & 0x80000000)
act_clause_rescale(s);
}
+*/
static inline void act_var_decay(sat_solver* s) { s->var_inc += (s->var_inc >> 4); }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
+//static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
#endif
//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+ int i, j, best_i;
+ void* tmp;
+
+ for (i = 0; i < size-1; i++){
+ best_i = i;
+ for (j = i+1; j < size; j++){
+ if (comp(array[j], array[best_i]) < 0)
+ best_i = j;
+ }
+ tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+ }
+}
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+ if (size <= 15)
+ selectionsort(array, size, comp);
+
+ else{
+ void* pivot = array[irand(seed, size)];
+ void* tmp;
+ int i = -1;
+ int j = size;
+
+ for(;;){
+ do i++; while(comp(array[i], pivot)<0);
+ do j--; while(comp(pivot, array[j])<0);
+
+ if (i >= j) break;
+
+ tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+ }
+
+ sortrnd(array , i , comp, seed);
+ sortrnd(&array[i], size-i, comp, seed);
+ }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+// int i;
+ double seed = 91648253;
+ sortrnd(array,size,comp,&seed);
+// for ( i = 1; i < size; i++ )
+// assert(comp(array[i-1], array[i])<0);
+}
+
+//=================================================================================================
// Clause functions:
/* pre: size > 1 && no variable occurs twice
*/
-static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int size;
clause* c;
- int i;
+ int h, i;
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
@@ -332,23 +445,20 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
// 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;
+ veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
+ veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
+ return 0;
}
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
- c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
+ // create new clause
+ h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) );
+ c = clause_read( s, h );
+ assert( !(h & 1) );
+ if ( s->hLearnts == -1 && learnt )
+ s->hLearnts = h;
c->size_learnt = (size << 1) | learnt;
- assert(((ABC_PTRUINT_T)c & 1) == 0);
-
for (i = 0; i < size; i++)
c->lits[i] = begin[i];
-
if (learnt)
*((float*)&c->lits[size]) = 0.0;
@@ -360,44 +470,35 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
assert(lit_neg(begin[0]) < s->size*2);
assert(lit_neg(begin[1]) < s->size*2);
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
- 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])));
+ //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
+ //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
+ veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
+ veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
- return c;
+ return h;
}
//=================================================================================================
// Minor (solver) functions:
-static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
+static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
{
- lbool* values = s->assigns;
- int v = lit_var(l);
- lbool val = values[v];
- lbool sig;
+ int v = lit_var(l);
#ifdef VERBOSEDEBUG
printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
#endif
-
- sig = !lit_sign(l); sig += sig - 1;
- if (val != l_Undef){
- return val == sig;
- }else{
- int* levels = s->levels;
- clause** reasons = s->reasons;
+ if (var_value(s, v) != varX)
+ return var_value(s, v) == lit_sign(l);
+ else{
// New fact -- store it.
#ifdef VERBOSEDEBUG
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
#endif
- values [v] = sig;
- levels [v] = sat_solver_dl(s);
- reasons[v] = from;
+ var_set_value(s, v, lit_sign(l));
+ var_set_level(s, v, sat_solver_dl(s));
+ s->reasons[v] = from;
s->trail[s->qtail++] = l;
-
order_assigned(s, v);
return true;
}
@@ -406,20 +507,17 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
static inline int sat_solver_assume(sat_solver* s, lit l){
assert(s->qtail == s->qhead);
- assert(s->assigns[lit_var(l)] == l_Undef);
+ assert(var_value(s, lit_var(l)) == varX);
#ifdef VERBOSEDEBUG
printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l));
printf( "act = %.20f\n", s->activity[lit_var(l)] );
#endif
veci_push(&s->trail_lim,s->qtail);
- return sat_solver_enqueue(s,l,(clause*)0);
+ return sat_solver_enqueue(s,l,0);
}
static void sat_solver_canceluntil(sat_solver* s, int level) {
- lit* trail;
- lbool* values;
- clause** reasons;
int bound;
int lastLev;
int c;
@@ -427,9 +525,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
if (sat_solver_dl(s) <= level)
return;
- trail = s->trail;
- values = s->assigns;
- reasons = s->reasons;
bound = (veci_begin(&s->trail_lim))[level];
lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
@@ -440,15 +535,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
////////////////////////////////////////
for (c = s->qtail-1; c >= bound; c--) {
- int x = lit_var(trail[c]);
- values [x] = l_Undef;
- reasons[x] = (clause*)0;
+ int x = lit_var(s->trail[c]);
+ var_set_value(s, x, varX);
+ s->reasons[x] = 0;
if ( c < lastLev )
- s->polarity[x] = !lit_sign(trail[c]);
+ var_set_polar( s, x, !lit_sign(s->trail[c]) );
}
for (c = s->qhead-1; c >= bound; c--)
- order_unassigned(s,lit_var(trail[c]));
+ order_unassigned(s,lit_var(s->trail[c]));
s->qhead = s->qtail = bound;
veci_resize(&s->trail_lim,level);
@@ -458,8 +553,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
- clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
- sat_solver_enqueue(s,*begin,c);
+ int h = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
+ sat_solver_enqueue(s,*begin,h);
///////////////////////////////////
// add clause to internal storage
@@ -472,9 +567,9 @@ static void sat_solver_record(sat_solver* s, veci* cls)
assert(veci_size(cls) > 0);
- if (c != 0) {
- vecp_push(&s->learnts,c);
- act_clause_bump(s,c);
+ if (h != 0) {
+// veci_push(&s->learnts,c);
+// act_clause_bump(s,c);
s->stats.learnts++;
s->stats.learnts_literals += veci_size(cls);
}
@@ -483,82 +578,59 @@ static void sat_solver_record(sat_solver* s, veci* cls)
static double sat_solver_progress(sat_solver* s)
{
- lbool* values = s->assigns;
- int* levels = s->levels;
int i;
-
double progress = 0;
double F = 1.0 / s->size;
for (i = 0; i < s->size; i++)
- if (values[i] != l_Undef)
- progress += pow(F, levels[i]);
+ if (var_value(s, i) != varX)
+ progress += pow(F, var_level(s, i));
return progress / s->size;
}
//=================================================================================================
// Major methods:
-static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
{
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
int top = veci_size(&s->tagged);
- assert(lit_var(l) >= 0 && lit_var(l) < s->size);
- assert(reasons[lit_var(l)] != 0);
+ assert(s->reasons[x] != 0);
veci_resize(&s->stack,0);
- veci_push(&s->stack,lit_var(l));
-
- while (veci_size(&s->stack) > 0){
- clause* c;
- int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
- assert(v >= 0 && v < s->size);
- veci_resize(&s->stack,veci_size(&s->stack)-1);
- assert(reasons[v] != 0);
- c = reasons[v];
-
- if (clause_is_lit(c)){
- int v = lit_var(clause_read_lit(c));
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+ veci_push(&s->stack,x);
+
+ while (veci_size(&s->stack)){
+ int v = veci_pop(&s->stack);
+ assert(s->reasons[v] != 0);
+ if (clause_is_lit(s->reasons[v])){
+ v = lit_var(clause_read_lit(s->reasons[v]));
+ if (!var_tag(s,v) && var_level(s, v)){
+ if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
veci_push(&s->stack,v);
- tags[v] = l_True;
- veci_push(&s->tagged,v);
+ var_set_tag(s, v, 1);
}else{
- int* tagged = veci_begin(&s->tagged);
- int j;
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
+ solver2_clear_tags(s, top);
+ return 0;
}
}
}else{
- lit* lits = clause_begin(c);
- int i, j;
-
- for (i = 1; i < clause_size(c); i++){
+ clause* c = clause_read(s, s->reasons[v]);
+ lit* lits = clause_begin(c);
+ int i;
+ for (i = 1; i < clause_nlits(c); i++){
int v = lit_var(lits[i]);
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
+ if (!var_tag(s,v) && var_level(s, v)){
+ if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
veci_push(&s->stack,lit_var(lits[i]));
- tags[v] = l_True;
- veci_push(&s->tagged,v);
+ var_set_tag(s, v, 1);
}else{
- int* tagged = veci_begin(&s->tagged);
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
+ solver2_clear_tags(s, top);
+ return 0;
}
}
}
}
}
-
- return true;
+ return 1;
}
@@ -613,8 +685,9 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first)
#ifdef SAT_USE_ANALYZE_FINAL
-static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
+static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
{
+ clause* conf = clause_read(s, hConf);
int i, j, start;
veci_resize(&s->conf_final,0);
if ( s->root_level == 0 )
@@ -622,110 +695,87 @@ static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first
assert( veci_size(&s->tagged) == 0 );
// assert( s->tags[lit_var(p)] == l_Undef );
// s->tags[lit_var(p)] = l_True;
- for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
+ for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
{
int x = lit_var(clause_begin(conf)[i]);
- if (s->levels[x] > 0)
- {
- s->tags[x] = l_True;
- veci_push(&s->tagged,x);
- }
+ if (var_level(s, x) > 0)
+ var_set_tag(s, x, 1);
}
start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
int x = lit_var(s->trail[i]);
- if (s->tags[x] == l_True){
- if (s->reasons[x] == NULL){
- assert(s->levels[x] > 0);
+ if (var_tag(s,x)){
+ if (s->reasons[x] == 0){
+ assert(var_level(s, x) > 0);
veci_push(&s->conf_final,lit_neg(s->trail[i]));
}else{
- clause* c = s->reasons[x];
- if (clause_is_lit(c)){
- lit q = clause_read_lit(c);
+ if (clause_is_lit(s->reasons[x])){
+ lit q = clause_read_lit(s->reasons[x]);
assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (s->levels[lit_var(q)] > 0)
- {
- s->tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- }
+ if (var_level(s, lit_var(q)) > 0)
+ var_set_tag(s, lit_var(q), 1);
}
else{
+ clause* c = clause_read(s, s->reasons[x]);
int* lits = clause_begin(c);
- for (j = 1; j < clause_size(c); j++)
- if (s->levels[lit_var(lits[j])] > 0)
- {
- s->tags[lit_var(lits[j])] = l_True;
- veci_push(&s->tagged,lit_var(lits[j]));
- }
+ for (j = 1; j < clause_nlits(c); j++)
+ if (var_level(s, lit_var(lits[j])) > 0)
+ var_set_tag(s, lit_var(lits[j]), 1);
}
}
}
}
- for (i = 0; i < veci_size(&s->tagged); i++)
- s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
- veci_resize(&s->tagged,0);
+ solver2_clear_tags(s,0);
}
#endif
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
{
lit* trail = s->trail;
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
int cnt = 0;
lit p = lit_Undef;
int ind = s->qtail-1;
lit* lits;
int i, j, minl;
- int* tagged;
-
veci_push(learnt,lit_Undef);
-
do{
- assert(c != 0);
-
- if (clause_is_lit(c)){
- lit q = clause_read_lit(c);
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dl(s))
+ assert(h != 0);
+ if (clause_is_lit(h)){
+ int x = lit_var(clause_read_lit(h));
+ if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+ var_set_tag(s, x, 1);
+ act_var_bump(s,x);
+ if (var_level(s, x) == sat_solver_dl(s))
cnt++;
else
- veci_push(learnt,q);
+ veci_push(learnt,clause_read_lit(h));
}
}else{
-
- if (clause_learnt(c))
- act_clause_bump(s,c);
-
+ clause* c = clause_read(s, h);
+// if (clause_learnt(c))
+// act_clause_bump(s,c);
lits = clause_begin(c);
- //printlits(lits,lits+clause_size(c)); printf("\n");
- for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
- lit q = lits[j];
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dl(s))
+ //printlits(lits,lits+clause_nlits(c)); printf("\n");
+ for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(c); j++){
+ int x = lit_var(lits[j]);
+ if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+ var_set_tag(s, x, 1);
+ act_var_bump(s,x);
+ if (var_level(s,x) == sat_solver_dl(s))
cnt++;
else
- veci_push(learnt,q);
+ veci_push(learnt,lits[j]);
}
}
}
- while (tags[lit_var(trail[ind--])] == l_Undef);
+ while ( !var_tag(s, lit_var(trail[ind--])) );
p = trail[ind+1];
- c = reasons[lit_var(p)];
+ h = s->reasons[lit_var(p)];
cnt--;
}while (cnt > 0);
@@ -735,13 +785,13 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
lits = veci_begin(learnt);
minl = 0;
for (i = 1; i < veci_size(learnt); i++){
- int lev = levels[lit_var(lits[i])];
+ int lev = var_level(s, lit_var(lits[i]));
minl |= 1 << (lev & 31);
}
// simplify (full)
for (i = j = 1; i < veci_size(learnt); i++){
- if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+ if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lit_var(lits[i]),minl))
lits[j++] = lits[i];
}
@@ -750,14 +800,11 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
s->stats.tot_literals += j;
// clear tags
- tagged = veci_begin(&s->tagged);
- for (i = 0; i < veci_size(&s->tagged); i++)
- tags[tagged[i]] = l_Undef;
- veci_resize(&s->tagged,0);
+ solver2_clear_tags(s,0);
#ifdef DEBUG
for (i = 0; i < s->size; i++)
- assert(tags[i] == l_Undef);
+ assert(!var_tag(s, i));
#endif
#ifdef VERBOSEDEBUG
@@ -766,12 +813,12 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
#endif
if (veci_size(learnt) > 1){
int max_i = 1;
- int max = levels[lit_var(lits[1])];
+ int max = var_level(s, lit_var(lits[1]));
lit tmp;
for (i = 2; i < veci_size(learnt); i++)
- if (levels[lit_var(lits[i])] > max){
- max = levels[lit_var(lits[i])];
+ if (var_level(s, lit_var(lits[i])) > max){
+ max = var_level(s, lit_var(lits[i]));
max_i = i;
}
@@ -781,28 +828,26 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
}
#ifdef VERBOSEDEBUG
{
- int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+ int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0;
printf(" } at level %d\n", lev);
}
#endif
}
-clause* sat_solver_propagate(sat_solver* s)
+int sat_solver_propagate(sat_solver* s)
{
- lbool* values = s->assigns;
- clause* confl = (clause*)0;
+ int hConfl = 0;
lit* lits;
lit false_lit;
- lbool sig;
//printf("sat_solver_propagate\n");
- while (confl == 0 && s->qtail - s->qhead > 0){
- lit p = s->trail[s->qhead++];
- vecp* ws = sat_solver_read_wlist(s,p);
- clause **begin = (clause**)vecp_begin(ws);
- clause **end = begin + vecp_size(ws);
- clause **i, **j;
+ while (hConfl == 0 && s->qtail - s->qhead > 0){
+ lit p = s->trail[s->qhead++];
+ veci* ws = sat_solver_read_wlist(s,p);
+ int* begin = veci_begin(ws);
+ int* end = begin + veci_size(ws);
+ int*i, *j;
s->stats.propagations++;
s->simpdb_props--;
@@ -812,24 +857,24 @@ clause* sat_solver_propagate(sat_solver* s)
if (clause_is_lit(*i)){
int Lit = clause_read_lit(*i);
- sig = !lit_sign(Lit); sig += sig - 1;
- if (values[lit_var(Lit)] == sig){
+ if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
*j++ = *i++;
continue;
}
*j++ = *i;
if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
- confl = s->binary;
- (clause_begin(confl))[1] = lit_neg(p);
- (clause_begin(confl))[0] = clause_read_lit(*i++);
+ hConfl = s->hBinary;
+ (clause_begin(s->binary))[1] = lit_neg(p);
+ (clause_begin(s->binary))[0] = clause_read_lit(*i++);
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
}else{
- lits = clause_begin(*i);
+ clause* c = clause_read(s,*i);
+ lits = clause_begin(c);
// Make sure the false literal is data[1]:
false_lit = lit_neg(p);
@@ -838,29 +883,26 @@ clause* sat_solver_propagate(sat_solver* s)
lits[1] = false_lit;
}
assert(lits[1] == false_lit);
- //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
// If 0th watch is true, then clause is already satisfied.
- sig = !lit_sign(lits[0]); sig += sig - 1;
- if (values[lit_var(lits[0])] == sig){
+ if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
*j++ = *i;
- }else{
+ else{
// Look for new watch:
- lit* stop = lits + clause_size(*i);
+ lit* stop = lits + clause_nlits(c);
lit* k;
for (k = lits + 2; k < stop; k++){
- lbool sig = lit_sign(*k); sig += sig - 1;
- if (values[lit_var(*k)] != sig){
+ if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
lits[1] = *k;
*k = false_lit;
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+ veci_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
goto next; }
}
*j++ = *i;
// Clause is unit under assignment:
if (!sat_solver_enqueue(s,lits[0], *i)){
- confl = *i++;
+ hConfl = *i++;
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
@@ -871,11 +913,11 @@ clause* sat_solver_propagate(sat_solver* s)
i++;
}
- s->stats.inspects += j - (clause**)vecp_begin(ws);
- vecp_resize(ws,j - (clause**)vecp_begin(ws));
+ s->stats.inspects += j - veci_begin(ws);
+ veci_resize(ws,j - veci_begin(ws));
}
- return confl;
+ return hConfl;
}
//=================================================================================================
@@ -883,12 +925,15 @@ clause* sat_solver_propagate(sat_solver* s)
sat_solver* sat_solver_new(void)
{
- sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
- memset( s, 0, sizeof(sat_solver) );
+ sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
+
+ Vec_RecAlloc_(&s->Mem);
+ s->hLearnts = -1;
+ s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+ s->binary = clause_read( s, s->hBinary );
+ s->binary->size_learnt = (2 << 1);
// initialize vectors
- vecp_new(&s->clauses);
- vecp_new(&s->learnts);
veci_new(&s->order);
veci_new(&s->trail_lim);
veci_new(&s->tagged);
@@ -901,15 +946,10 @@ sat_solver* sat_solver_new(void)
// initialize arrays
s->wlists = 0;
s->activity = 0;
- s->factors = 0;
- s->assigns = 0;
s->orderpos = 0;
s->reasons = 0;
- s->levels = 0;
- s->tags = 0;
s->trail = 0;
-
// initialize other vars
s->size = 0;
s->cap = 0;
@@ -929,8 +969,8 @@ sat_solver* sat_solver_new(void)
s->simpdb_props = 0;
s->random_seed = 91648253;
s->progress_estimate = 0;
- s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
- s->binary->size_learnt = (2 << 1);
+// s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+// s->binary->size_learnt = (2 << 1);
s->verbosity = 0;
s->stats.starts = 0;
@@ -943,12 +983,6 @@ sat_solver* sat_solver_new(void)
s->stats.learnts = 0;
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- s->pMem = NULL;
-#else
- s->pMem = Sat_MmStepStart( 10 );
-#endif
return s;
}
@@ -960,42 +994,46 @@ void sat_solver_setnvars(sat_solver* s,int n)
int old_cap = s->cap;
while (s->cap < n) s->cap = s->cap*2+1;
- s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2);
+ s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
+// s->vi = ABC_REALLOC(varinfo,s->vi, s->cap);
+ s->levels = ABC_REALLOC(int, s->levels, s->cap);
+ s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
+ s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
+ s->tags = ABC_REALLOC(char, s->tags, s->cap);
#ifdef USE_FLOAT_ACTIVITY
s->activity = ABC_REALLOC(double, s->activity, s->cap);
#else
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
#endif
+ if ( s->factors )
s->factors = ABC_REALLOC(double, s->factors, s->cap);
- s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap);
s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
- s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap);
- s->levels = ABC_REALLOC(int, s->levels, s->cap);
- s->tags = ABC_REALLOC(lbool, s->tags, s->cap);
+ s->reasons = ABC_REALLOC(int, s->reasons, s->cap);
s->trail = ABC_REALLOC(lit, s->trail, s->cap);
- s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
- memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
- }
+ memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
+ }
for (var = s->size; var < n; var++){
assert(!s->wlists[2*var].size);
assert(!s->wlists[2*var+1].size);
if ( s->wlists[2*var].ptr == NULL )
- vecp_new(&s->wlists[2*var]);
+ veci_new(&s->wlists[2*var]);
if ( s->wlists[2*var+1].ptr == NULL )
- vecp_new(&s->wlists[2*var+1]);
+ veci_new(&s->wlists[2*var+1]);
#ifdef USE_FLOAT_ACTIVITY
s->activity[var] = 0;
#else
s->activity[var] = (1<<10);
#endif
- s->factors [var] = 0;
- s->assigns [var] = l_Undef;
- s->orderpos [var] = veci_size(&s->order);
- s->reasons [var] = (clause*)0;
- s->levels [var] = 0;
- s->tags [var] = l_Undef;
- s->polarity [var] = 0;
+ if ( s->factors )
+ s->factors [var] = 0;
+// *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+ s->levels [var] = 0;
+ s->assigns [var] = varX;
+ s->polarity[var] = 0;
+ s->tags [var] = 0;
+ s->orderpos[var] = veci_size(&s->order);
+ s->reasons [var] = 0;
/* does not hold because variables enqueued at top level will not be reinserted in the heap
assert(veci_size(&s->order) == var);
@@ -1009,20 +1047,9 @@ void sat_solver_setnvars(sat_solver* s,int n)
void sat_solver_delete(sat_solver* s)
{
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- int i;
- for (i = 0; i < vecp_size(&s->clauses); i++)
- ABC_FREE(vecp_begin(&s->clauses)[i]);
- for (i = 0; i < vecp_size(&s->learnts); i++)
- ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
- Sat_MmStepStop( s->pMem, 0 );
-#endif
+ Vec_RecFree_( &s->Mem );
// delete vectors
- vecp_delete(&s->clauses);
- vecp_delete(&s->learnts);
veci_delete(&s->order);
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
@@ -1031,23 +1058,23 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->act_vars);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
- ABC_FREE(s->binary);
// delete arrays
- if (s->wlists != 0){
+ if (s->reasons != 0){
int i;
for (i = 0; i < s->cap*2; i++)
- vecp_delete(&s->wlists[i]);
+ veci_delete(&s->wlists[i]);
ABC_FREE(s->wlists );
+// ABC_FREE(s->vi );
+ ABC_FREE(s->levels );
+ ABC_FREE(s->assigns );
+ ABC_FREE(s->polarity );
+ ABC_FREE(s->tags );
ABC_FREE(s->activity );
ABC_FREE(s->factors );
- ABC_FREE(s->assigns );
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
- ABC_FREE(s->levels );
ABC_FREE(s->trail );
- ABC_FREE(s->tags );
- ABC_FREE(s->polarity );
}
sat_solver_store_free(s);
@@ -1057,16 +1084,13 @@ void sat_solver_delete(sat_solver* s)
void sat_solver_rollback( sat_solver* s )
{
int i;
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- for (i = 0; i < vecp_size(&s->clauses); i++)
- ABC_FREE(vecp_begin(&s->clauses)[i]);
- for (i = 0; i < vecp_size(&s->learnts); i++)
- ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
- Sat_MmStepRestart( s->pMem );
-#endif
- vecp_resize(&s->clauses, 0);
- vecp_resize(&s->learnts, 0);
+ Vec_RecRestart( &s->Mem );
+
+ s->hLearnts = -1;
+ s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+ s->binary = clause_read( s, s->hBinary );
+ s->binary->size_learnt = (2 << 1);
+
veci_resize(&s->trail_lim, 0);
veci_resize(&s->order, 0);
for ( i = 0; i < s->size*2; i++ )
@@ -1105,56 +1129,49 @@ void sat_solver_rollback( sat_solver* s )
s->stats.tot_literals = 0;
}
-
+/*
static void clause_remove(sat_solver* s, clause* c)
{
lit* lits = clause_begin(c);
assert(lit_neg(lits[0]) < s->size*2);
assert(lit_neg(lits[1]) < s->size*2);
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+ //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+ //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
assert(lits[0] < s->size*2);
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+ veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[1])));
+ veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->stats.learnts--;
- s->stats.learnts_literals -= clause_size(c);
+ s->stats.learnts_literals -= clause_nlits(c);
}else{
s->stats.clauses--;
- s->stats.clauses_literals -= clause_size(c);
+ s->stats.clauses_literals -= clause_nlits(c);
}
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- ABC_FREE(c);
-#else
- Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
}
static lbool clause_simplify(sat_solver* s, clause* c)
{
lit* lits = clause_begin(c);
- lbool* values = s->assigns;
int i;
assert(sat_solver_dl(s) == 0);
- for (i = 0; i < clause_size(c); i++){
+ for (i = 0; i < clause_nlits(c); i++){
lbool sig = !lit_sign(lits[i]); sig += sig - 1;
- if (values[lit_var(lits[i])] == sig)
+ if (s->assignss[lit_var(lits[i])] == sig)
return l_True;
}
return l_False;
}
+*/
int sat_solver_simplify(sat_solver* s)
{
- clause** reasons;
- int type;
-
+// clause** reasons;
+// int type;
assert(sat_solver_dl(s) == 0);
if (sat_solver_propagate(s) != 0)
@@ -1162,7 +1179,7 @@ int sat_solver_simplify(sat_solver* s)
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
-
+/*
reasons = s->reasons;
for (type = 0; type < 2; type++){
vecp* cs = type ? &s->learnts : &s->clauses;
@@ -1178,53 +1195,48 @@ int sat_solver_simplify(sat_solver* s)
}
vecp_resize(cs,j);
}
-
+*/
s->simpdb_assigns = s->qhead;
// (shouldn't depend on 'stats' really, but it will do for now)
s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-
return true;
}
+/*
static int clause_cmp (const void* x, const void* y) {
- return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
+ return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
void sat_solver_reducedb(sat_solver* s)
{
int i, j;
- double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
- clause** learnts = (clause**)vecp_begin(&s->learnts);
+ double extra_lim = s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity
+ clause** learnts = (clause**)veci_begin(&s->learnts);
clause** reasons = s->reasons;
- sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+ sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp);
- for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+ for (i = j = 0; i < veci_size(&s->learnts) / 2; i++){
+ if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
}
- for (; i < vecp_size(&s->learnts); i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+ for (; i < veci_size(&s->learnts); i++){
+ if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
}
-
- //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
- vecp_resize(&s->learnts,j);
+ veci_resize(&s->learnts,j);
}
+*/
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
- clause * c;
lit *i,*j;
int maxvar;
- lbool* values;
lit last;
+ assert( begin < end );
veci_resize( &s->temp_clause, 0 );
for ( i = begin; i < end; i++ )
@@ -1232,10 +1244,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
begin = veci_begin( &s->temp_clause );
end = begin + veci_size( &s->temp_clause );
- if (begin == end)
- return false;
-
- //printlits(begin,end); printf("\n");
// insertion sort
maxvar = lit_var(*begin);
for (i = begin + 1; i < end; i++){
@@ -1246,7 +1254,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
*j = l;
}
sat_solver_setnvars(s,maxvar+1);
-// sat_solver_setnvars(s, lit_var(*(end-1))+1 );
///////////////////////////////////
// add clause to internal storage
@@ -1257,17 +1264,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
}
///////////////////////////////////
- //printlits(begin,end); printf("\n");
- values = s->assigns;
-
// delete duplicates
last = lit_Undef;
for (i = j = begin; i < end; i++){
- //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
- lbool sig = !lit_sign(*i); sig += sig - 1;
- if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+ //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
+ if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
return true; // tautology
- else if (*i != last && values[lit_var(*i)] == l_Undef)
+ else if (*i != last && var_value(s, lit_var(*i)) == varX)
last = *j++ = *i;
}
// j = i;
@@ -1276,17 +1279,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
return false;
if (j - begin == 1) // unit clause
- return sat_solver_enqueue(s,*begin,(clause*)0);
+ return sat_solver_enqueue(s,*begin,0);
// create new clause
- c = clause_create_new(s,begin,j,0);
- if ( c )
- vecp_push(&s->clauses,c);
-
+ clause_create_new(s,begin,j,0);
s->stats.clauses++;
s->stats.clauses_literals += j - begin;
-
return true;
}
@@ -1313,7 +1312,6 @@ void luby_test()
static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
{
- int* levels = s->levels;
double var_decay = 0.95;
double clause_decay = 0.999;
double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
@@ -1343,8 +1341,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
act_var_bump_global(s, s->act_vars.ptr[i]);
for (;;){
- clause* confl = sat_solver_propagate(s);
- if (confl != 0){
+ int hConfl = sat_solver_propagate(s);
+ if (hConfl != 0){
// CONFLICT
int blevel;
@@ -1354,24 +1352,25 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
s->stats.conflicts++; conflictC++;
if (sat_solver_dl(s) == s->root_level){
#ifdef SAT_USE_ANALYZE_FINAL
- sat_solver_analyze_final(s, confl, 0);
+ sat_solver_analyze_final(s, hConfl, 0);
#endif
veci_delete(&learnt_clause);
return l_False;
}
veci_resize(&learnt_clause,0);
- sat_solver_analyze(s, confl, &learnt_clause);
- blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+ sat_solver_analyze(s, hConfl, &learnt_clause);
+ blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
blevel = s->root_level > blevel ? s->root_level : blevel;
sat_solver_canceluntil(s,blevel);
sat_solver_record(s,&learnt_clause);
#ifdef SAT_USE_ANALYZE_FINAL
// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
- if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+ if ( learnt_clause.size == 1 )
+ var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
#endif
act_var_decay(s);
- act_clause_decay(s);
+// act_clause_decay(s);
}else{
// NO CONFLICT
@@ -1385,7 +1384,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
return l_Undef; }
if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-// (s->nInsLimit && s->stats.inspects > s->nInsLimit) )
(s->nInsLimit && s->stats.propagations > s->nInsLimit) )
{
// Reached bound on number of conflicts:
@@ -1399,7 +1397,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
// Simplify the set of problem clauses:
sat_solver_simplify(s);
-// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+// if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
// sat_solver_reducedb(s);
@@ -1409,11 +1407,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
if (next == var_Undef){
// Model found:
- lbool* values = s->assigns;
int i;
veci_resize(&s->model, 0);
for (i = 0; i < s->size; i++)
- veci_push(&s->model,(int)values[i]);
+ veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
@@ -1428,7 +1425,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
return l_True;
}
- if ( s->polarity[next] ) // positive polarity
+ if ( var_polar(s, next) ) // positive polarity
sat_solver_assume(s,toLit(next));
else
sat_solver_assume(s,lit_neg(toLit(next)));
@@ -1444,7 +1441,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
ABC_INT64_T nof_conflicts;
ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3;
lbool status = l_Undef;
- lbool* values = s->assigns;
lit* i;
////////////////////////////////////////////////
@@ -1478,15 +1474,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
//printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){
- switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
- case 1: // l_True:
+// switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
+ switch (var_value(s, *i)) {
+ case var1: // l_True:
break;
- case 0: // l_Undef
+ case varX: // l_Undef
sat_solver_assume(s, *i);
- if (sat_solver_propagate(s) == NULL)
+ if (sat_solver_propagate(s) == 0)
break;
// fallthrough
- case -1: // l_False
+ case var0: // l_False
sat_solver_canceluntil(s, 0);
return l_False;
}
@@ -1535,21 +1532,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
lit p = *i;
assert(lit_var(p) < s->size);
veci_push(&s->trail_lim,s->qtail);
- if (!sat_solver_enqueue(s,p,(clause*)0))
+ if (!sat_solver_enqueue(s,p,0))
{
- clause * r = s->reasons[lit_var(p)];
- if (r != NULL)
+ int h = s->reasons[lit_var(p)];
+ if (h)
{
- clause* confl;
- if (clause_is_lit(r))
+ if (clause_is_lit(h))
{
- confl = s->binary;
- (clause_begin(confl))[1] = lit_neg(p);
- (clause_begin(confl))[0] = clause_read_lit(r);
+ (clause_begin(s->binary))[1] = lit_neg(p);
+ (clause_begin(s->binary))[0] = clause_read_lit(h);
+ h = s->hBinary;
}
- else
- confl = r;
- sat_solver_analyze_final(s, confl, 1);
+ sat_solver_analyze_final(s, h, 1);
veci_push(&s->conf_final, lit_neg(p));
}
else
@@ -1557,7 +1551,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
veci_resize(&s->conf_final,0);
veci_push(&s->conf_final, lit_neg(p));
// the two lines below are a bug fix by Siert Wieringa
- if (s->levels[lit_var(p)] > 0)
+ if (var_level(s, lit_var(p)) > 0)
veci_push(&s->conf_final, p);
}
sat_solver_canceluntil(s, 0);
@@ -1565,9 +1559,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
}
else
{
- clause* confl = sat_solver_propagate(s);
- if (confl != NULL){
- sat_solver_analyze_final(s, confl, 0);
+ int fConfl = sat_solver_propagate(s);
+ if (fConfl){
+ sat_solver_analyze_final(s, fConfl, 0);
assert(s->conf_final.size > 0);
sat_solver_canceluntil(s, 0);
return l_False; }
@@ -1586,12 +1580,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
}
while (status == l_Undef){
-// int nConfs = 0;
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
break;
-
if (s->verbosity >= 1)
{
printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
@@ -1606,31 +1598,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
fflush(stdout);
}
nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-//printf( "%d ", (int)nof_conflicts );
-// nConfs = s->stats.conflicts;
status = sat_solver_search(s, nof_conflicts, nof_learnts);
-// if ( status == l_True )
-// printf( "%d ", s->stats.conflicts - nConfs );
-
-// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
-//printf( "%d ", s->stats.conflicts );
// quit the loop if reached an external limit
if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
- {
-// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
break;
- }
-// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
- {
-// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
break;
- }
if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
break;
}
-//printf( "\n" );
if (s->verbosity >= 1)
printf("==============================================================================\n");
@@ -1655,7 +1632,7 @@ int sat_solver_nvars(sat_solver* s)
int sat_solver_nclauses(sat_solver* s)
{
- return vecp_size(&s->clauses);
+ return s->stats.clauses;
}
@@ -1710,57 +1687,6 @@ void * sat_solver_store_release( sat_solver * s )
return pTemp;
}
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
- int i, j, best_i;
- void* tmp;
-
- for (i = 0; i < size-1; i++){
- best_i = i;
- for (j = i+1; j < size; j++){
- if (comp(array[j], array[best_i]) < 0)
- best_i = j;
- }
- tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
- }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
- if (size <= 15)
- selectionsort(array, size, comp);
-
- else{
- void* pivot = array[irand(seed, size)];
- void* tmp;
- int i = -1;
- int j = size;
-
- for(;;){
- do i++; while(comp(array[i], pivot)<0);
- do j--; while(comp(pivot, array[j])<0);
-
- if (i >= j) break;
-
- tmp = array[i]; array[i] = array[j]; array[j] = tmp;
- }
-
- sortrnd(array , i , comp, seed);
- sortrnd(&array[i], size-i, comp, seed);
- }
-}
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-// int i;
- double seed = 91648253;
- sortrnd(array,size,comp,&seed);
-// for ( i = 1; i < size; i++ )
-// assert(comp(array[i-1], array[i])<0);
-}
ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 4c577b1e..a0e94bfb 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <assert.h>
#include "satVec.h"
-#include "satMem.h"
+#include "vecRec.h"
ABC_NAMESPACE_HEADER_START
@@ -54,6 +54,8 @@ 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);
+extern int sat_solver_get_var_value(sat_solver* s, int v);
+
extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
@@ -79,84 +81,87 @@ extern void * sat_solver_store_release( sat_solver * s );
struct clause_t;
typedef struct clause_t clause;
+struct varinfo_t;
+typedef struct varinfo_t varinfo;
+
struct sat_solver_t
{
- int size; // nof variables
- int cap; // size of varmaps
- int qhead; // Head index of queue.
- int qtail; // Tail index of queue.
+ int size; // nof variables
+ int cap; // size of varmaps
+ int qhead; // Head index of queue.
+ int qtail; // Tail index of queue.
// clauses
- vecp clauses; // List of problem constraints. (contains: clause*)
- vecp learnts; // List of learnt clauses. (contains: clause*)
+ Vec_Rec_t Mem;
+ int hLearnts; // the first learnt clause
+ int hBinary; // the special binary clause
+ clause * binary;
// activities
#ifdef USE_FLOAT_ACTIVITY
- double var_inc; // Amount to bump next variable with.
- double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
- float cla_inc; // Amount to bump next clause with.
- float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
- double* activity; // A heuristic measurement of the activity of a variable.
+ double var_inc; // Amount to bump next variable with.
+ double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
+ float cla_inc; // Amount to bump next clause with.
+ float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
+ double* activity; // A heuristic measurement of the activity of a variable.
#else
- int var_inc; // Amount to bump next variable with.
- int cla_inc; // Amount to bump next clause with.
- unsigned*activity; // A heuristic measurement of the activity of a variable.
+ int var_inc; // Amount to bump next variable with.
+ int cla_inc; // Amount to bump next clause with.
+ unsigned* activity; // A heuristic measurement of the activity of a variable.
#endif
- vecp* wlists; //
- lbool* assigns; // Current values of variables.
- int* orderpos; // Index in variable order.
- clause** reasons; //
- int* levels; //
- lit* trail;
- char* polarity;
-
- clause* binary; // A temporary binary clause
- lbool* tags; //
- veci tagged; // (contains: var)
- veci stack; // (contains: var)
-
- veci order; // Variable order. (heap) (contains: var)
- veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
- veci model; // If problem is solved, this vector contains the model (contains: lbool).
- veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
- // this vector represent the final conflict clause expressed in the assumptions.
-
- int root_level; // Level of first proper decision.
- int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
- int simpdb_props; // Number of propagations before next 'simplifyDB()'.
- double random_seed;
- double progress_estimate;
- int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
- stats_t stats;
-
- ABC_INT64_T nConfLimit; // external limit on the number of conflicts
- ABC_INT64_T nInsLimit; // external limit on the number of implications
- int nRuntimeLimit; // external limit on runtime
-
- veci act_vars; // variables whose activity has changed
- double* factors; // the activity factors
- int nRestarts; // the number of local restarts
- int nCalls; // the number of local restarts
- int nCalls2; // the number of local restarts
-
- Sat_MmStep_t * pMem;
-
- int fSkipSimplify; // set to one to skip simplification of the clause database
- int fNotUseRandom; // do not allow random decisions with a fixed probability
-
- int * pGlobalVars; // for experiments with global vars during interpolation
+ veci* wlists; //
+// varinfo * vi; // variable information
+ int* levels; //
+ char* assigns; // Current values of variables.
+ char* polarity; //
+ char* tags; //
+
+ int* orderpos; // Index in variable order.
+ int* reasons; //
+ lit* trail;
+ veci tagged; // (contains: var)
+ veci stack; // (contains: var)
+
+ veci order; // Variable order. (heap) (contains: var)
+ veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
+ veci model; // If problem is solved, this vector contains the model (contains: lbool).
+ veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
+ // this vector represent the final conflict clause expressed in the assumptions.
+
+ int root_level; // Level of first proper decision.
+ int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+ int simpdb_props; // Number of propagations before next 'simplifyDB()'.
+ double random_seed;
+ double progress_estimate;
+ int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+ stats_t stats;
+
+ ABC_INT64_T nConfLimit; // external limit on the number of conflicts
+ ABC_INT64_T nInsLimit; // external limit on the number of implications
+ int nRuntimeLimit; // external limit on runtime
+
+ veci act_vars; // variables whose activity has changed
+ double* factors; // the activity factors
+ int nRestarts; // the number of local restarts
+ int nCalls; // the number of local restarts
+ int nCalls2; // the number of local restarts
+
+ int fSkipSimplify; // set to one to skip simplification of the clause database
+ int fNotUseRandom; // do not allow random decisions with a fixed probability
+
+ int * pGlobalVars; // for experiments with global vars during interpolation
// clause store
- void * pStore;
- int fSolved;
+ void * pStore;
+ int fSolved;
// trace recording
- FILE * pFile;
- int nClauses;
- int nRoots;
+ FILE * pFile;
+ int nClauses;
+ int nRoots;
- veci temp_clause; // temporary storage for a CNF clause
+ veci temp_clause; // temporary storage for a CNF clause
};
static int sat_solver_var_value( sat_solver* s, int v )
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 5eb65132..0cda3295 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -65,14 +65,6 @@ static inline double drand(double* seed) {
static inline int irand(double* seed, int size) {
return (int)(drand(seed) * size); }
-static inline int sat_float2int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
-static inline float sat_int2float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
-
-//=================================================================================================
-// Predeclarations:
-
-static void solver2_sort(void** array, int size, int(*comp)(const void *, const void *));
-
//=================================================================================================
// Variable datatype + minor functions:
@@ -82,23 +74,27 @@ static const int varX = 3;
struct varinfo_t
{
- unsigned val : 2; // variable value
+// unsigned val : 2; // variable value
unsigned pol : 1; // last polarity
unsigned partA : 1; // partA variable
unsigned tag : 4; // conflict analysis tags
- unsigned lev : 24; // variable level
+// unsigned lev : 24; // variable level
};
int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; }
void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; }
-static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; }
+//static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; }
+static inline int var_level (sat_solver2* s, int v) { return s->levels[v]; }
+//static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; }
+static inline int var_value (sat_solver2* s, int v) { return s->assigns[v]; }
static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; }
-static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; }
-static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; }
+//static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; }
+static inline void var_set_level (sat_solver2* s, int v, int lev) { s->levels[v] = lev; }
+//static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; }
+static inline void var_set_value (sat_solver2* s, int v, int val) { s->assigns[v] = val; }
static inline void var_set_polar (sat_solver2* s, int v, int pol) { s->vi[v].pol = pol; }
-static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; }
// variable tags
static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; }
@@ -1268,6 +1264,8 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
s->vi = ABC_REALLOC(varinfo, s->vi, s->cap);
+ s->levels = ABC_REALLOC(int, s->levels, s->cap);
+ s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
s->trail = ABC_REALLOC(lit, s->trail, s->cap);
s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
s->reasons = ABC_REALLOC(cla, s->reasons, s->cap);
@@ -1288,7 +1286,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
veci_new(&s->wlists[2*var]);
if ( s->wlists[2*var+1].ptr == NULL )
veci_new(&s->wlists[2*var+1]);
- *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+ *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
+ s->levels [var] = 0;
+ s->assigns [var] = varX;
s->orderpos[var] = veci_size(&s->order);
s->reasons [var] = 0;
if ( s->fProofLogging )
@@ -1346,6 +1346,8 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->wlists[i]);
ABC_FREE(s->wlists );
ABC_FREE(s->vi );
+ ABC_FREE(s->levels );
+ ABC_FREE(s->assigns );
ABC_FREE(s->trail );
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 0c08ac1e..21dc3b21 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -126,6 +126,8 @@ struct sat_solver2_t
// internal state
varinfo * vi; // variable information
+ int* levels; //
+ char* assigns; //
lit* trail; // sequence of assignment and implications
int* orderpos; // Index in variable order.
cla* reasons; // reason clauses
diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c
new file mode 100644
index 00000000..4d851d0f
--- /dev/null
+++ b/src/sat/bsat/satSolver_old.c
@@ -0,0 +1,1766 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "satSolver.h"
+#include "satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+#define SAT_USE_ANALYZE_FINAL
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND "%-*d"
+#define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s)
+#define L_LIT "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+ int i;
+ for (i = 0; i < end - begin; i++)
+ printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+ int q;
+ *seed *= 1389796;
+ q = (int)(*seed / 2147483647);
+ *seed -= (double)q * 2147483647;
+ return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+ return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+ int size_learnt;
+ lit lits[0];
+};
+
+static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
+static inline lit* clause_begin (clause* c) { return c->lits; }
+static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
+static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline unsigned clause_activity2 (clause* c) { return *((unsigned*)&c->lits[c->size_learnt>>1]); }
+static inline void clause_setactivity (clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a; }
+static inline void clause_print (clause* c) {
+ int i;
+ printf( "{ " );
+ for ( i = 0; i < clause_size(c); i++ )
+ printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
+ printf( "}\n" );
+}
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
+static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); }
+static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
+static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver* s, int v) // updateorder
+{
+ int* orderpos = s->orderpos;
+ int* heap = veci_begin(&s->order);
+ int i = orderpos[v];
+ int x = heap[i];
+ int parent = (i - 1) / 2;
+
+ assert(s->orderpos[v] != -1);
+
+ while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
+ heap[i] = heap[parent];
+ orderpos[heap[i]] = i;
+ i = parent;
+ parent = (i - 1) / 2;
+ }
+ heap[i] = x;
+ orderpos[x] = i;
+}
+
+static inline void order_assigned(sat_solver* s, int v)
+{
+}
+
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
+{
+ int* orderpos = s->orderpos;
+ if (orderpos[v] == -1){
+ orderpos[v] = veci_size(&s->order);
+ veci_push(&s->order,v);
+ order_update(s,v);
+//printf( "+%d ", v );
+ }
+}
+
+static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
+{
+ int* heap;
+ int* orderpos;
+
+ lbool* values = s->assigns;
+
+ // Random decision:
+ if (drand(&s->random_seed) < random_var_freq){
+ int next = irand(&s->random_seed,s->size);
+ assert(next >= 0 && next < s->size);
+ if (values[next] == l_Undef)
+ return next;
+ }
+
+ // Activity based decision:
+
+ heap = veci_begin(&s->order);
+ orderpos = s->orderpos;
+
+
+ while (veci_size(&s->order) > 0){
+ int next = heap[0];
+ int size = veci_size(&s->order)-1;
+ int x = heap[size];
+
+ veci_resize(&s->order,size);
+
+ orderpos[next] = -1;
+
+ if (size > 0){
+
+ int i = 0;
+ int child = 1;
+
+
+ while (child < size){
+ if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
+ child++;
+
+ assert(child < size);
+
+ if (s->activity[x] >= s->activity[heap[child]])
+ break;
+
+ heap[i] = heap[child];
+ orderpos[heap[i]] = i;
+ i = child;
+ child = 2 * child + 1;
+ }
+ heap[i] = x;
+ orderpos[heap[i]] = i;
+ }
+
+//printf( "-%d ", next );
+ if (values[next] == l_Undef)
+ return next;
+ }
+
+ return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+#ifdef USE_FLOAT_ACTIVITY
+
+static inline void act_var_rescale(sat_solver* s) {
+ double* activity = s->activity;
+ int i;
+ for (i = 0; i < s->size; i++)
+ activity[i] *= 1e-100;
+ s->var_inc *= 1e-100;
+}
+static inline void act_clause_rescale(sat_solver* s) {
+ static int Total = 0;
+ clause** cs = (clause**)vecp_begin(&s->learnts);
+ int i, clk = clock();
+ for (i = 0; i < vecp_size(&s->learnts); i++){
+ float a = clause_activity(cs[i]);
+ clause_setactivity(cs[i], a * (float)1e-20);
+ }
+ s->cla_inc *= (float)1e-20;
+
+ Total += clock() - clk;
+ printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
+ Abc_PrintTime( 1, "Time", Total );
+}
+static inline void act_var_bump(sat_solver* s, int v) {
+ s->activity[v] += s->var_inc;
+ if (s->activity[v] > 1e100)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+static inline void act_var_bump_global(sat_solver* s, int v) {
+ s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
+ if (s->activity[v] > 1e100)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+ s->activity[v] += (s->var_inc * s->factors[v]);
+ if (s->activity[v] > 1e100)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+ float a = clause_activity(c) + s->cla_inc;
+ clause_setactivity(c,a);
+ if (a > 1e20) act_clause_rescale(s);
+}
+static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+
+#else
+
+static inline void act_var_rescale(sat_solver* s) {
+ unsigned* activity = s->activity;
+ int i;
+ for (i = 0; i < s->size; i++)
+ activity[i] >>= 19;
+ s->var_inc >>= 19;
+ s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
+}
+static inline void act_clause_rescale(sat_solver* s) {
+ static int Total = 0;
+ clause** cs = (clause**)vecp_begin(&s->learnts);
+ int i, clk = clock();
+ for (i = 0; i < vecp_size(&s->learnts); i++){
+ unsigned a = clause_activity2(cs[i]);
+ clause_setactivity2(cs[i], a >> 14);
+ }
+ s->cla_inc >>= 14;
+ s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
+
+// Total += clock() - clk;
+// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
+// Abc_PrintTime( 1, "Time", Total );
+}
+static inline void act_var_bump(sat_solver* s, int v) {
+ s->activity[v] += s->var_inc;
+ if (s->activity[v] & 0x80000000)
+ act_var_rescale(s);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+}
+static inline void act_var_bump_global(sat_solver* s, int v) {}
+static inline void act_var_bump_factor(sat_solver* s, int v) {}
+static inline void act_clause_bump(sat_solver* s, clause*c) {
+ unsigned a = clause_activity2(c) + s->cla_inc;
+ clause_setactivity2(c,a);
+ if (a & 0x80000000)
+ act_clause_rescale(s);
+}
+static inline void act_var_decay(sat_solver* s) { s->var_inc += (s->var_inc >> 4); }
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
+
+#endif
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+{
+ int size;
+ clause* c;
+ int i;
+
+ 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;
+ }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+ c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
+ c->size_learnt = (size << 1) | learnt;
+ assert(((ABC_PTRUINT_T)c & 1) == 0);
+
+ for (i = 0; i < size; i++)
+ c->lits[i] = begin[i];
+
+ if (learnt)
+ *((float*)&c->lits[size]) = 0.0;
+
+ assert(begin[0] >= 0);
+ assert(begin[0] < s->size*2);
+ assert(begin[1] >= 0);
+ assert(begin[1] < s->size*2);
+
+ assert(lit_neg(begin[0]) < s->size*2);
+ assert(lit_neg(begin[1]) < s->size*2);
+
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+ 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])));
+
+ return c;
+}
+
+
+//=================================================================================================
+// Minor (solver) functions:
+
+static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
+{
+ lbool* values = s->assigns;
+ int v = lit_var(l);
+ lbool val = values[v];
+ lbool sig;
+#ifdef VERBOSEDEBUG
+ printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+ sig = !lit_sign(l); sig += sig - 1;
+ if (val != l_Undef){
+ return val == sig;
+ }else{
+ int* levels = s->levels;
+ clause** reasons = s->reasons;
+ // New fact -- store it.
+#ifdef VERBOSEDEBUG
+ printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+ values [v] = sig;
+ levels [v] = sat_solver_dl(s);
+ reasons[v] = from;
+ s->trail[s->qtail++] = l;
+
+ order_assigned(s, v);
+ return true;
+ }
+}
+
+
+static inline int sat_solver_assume(sat_solver* s, lit l){
+ assert(s->qtail == s->qhead);
+ assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+ printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l));
+ printf( "act = %.20f\n", s->activity[lit_var(l)] );
+#endif
+ veci_push(&s->trail_lim,s->qtail);
+ return sat_solver_enqueue(s,l,(clause*)0);
+}
+
+
+static void sat_solver_canceluntil(sat_solver* s, int level) {
+ lit* trail;
+ lbool* values;
+ clause** reasons;
+ int bound;
+ int lastLev;
+ int c;
+
+ if (sat_solver_dl(s) <= level)
+ return;
+
+ trail = s->trail;
+ values = s->assigns;
+ reasons = s->reasons;
+ bound = (veci_begin(&s->trail_lim))[level];
+ lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
+
+ ////////////////////////////////////////
+ // added to cancel all assignments
+// if ( level == -1 )
+// bound = 0;
+ ////////////////////////////////////////
+
+ for (c = s->qtail-1; c >= bound; c--) {
+ int x = lit_var(trail[c]);
+ values [x] = l_Undef;
+ reasons[x] = (clause*)0;
+ if ( c < lastLev )
+ s->polarity[x] = !lit_sign(trail[c]);
+ }
+
+ for (c = s->qhead-1; c >= bound; c--)
+ order_unassigned(s,lit_var(trail[c]));
+
+ s->qhead = s->qtail = bound;
+ veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver_record(sat_solver* s, veci* cls)
+{
+ lit* begin = veci_begin(cls);
+ lit* end = begin + veci_size(cls);
+ clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
+ sat_solver_enqueue(s,*begin,c);
+
+ ///////////////////////////////////
+ // add clause to internal storage
+ if ( s->pStore )
+ {
+ int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
+ assert( RetValue );
+ }
+ ///////////////////////////////////
+
+ assert(veci_size(cls) > 0);
+
+ if (c != 0) {
+ vecp_push(&s->learnts,c);
+ act_clause_bump(s,c);
+ s->stats.learnts++;
+ s->stats.learnts_literals += veci_size(cls);
+ }
+}
+
+
+static double sat_solver_progress(sat_solver* s)
+{
+ lbool* values = s->assigns;
+ int* levels = s->levels;
+ int i;
+
+ double progress = 0;
+ double F = 1.0 / s->size;
+ for (i = 0; i < s->size; i++)
+ if (values[i] != l_Undef)
+ progress += pow(F, levels[i]);
+ return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+{
+ lbool* tags = s->tags;
+ clause** reasons = s->reasons;
+ int* levels = s->levels;
+ int top = veci_size(&s->tagged);
+
+ assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+ assert(reasons[lit_var(l)] != 0);
+ veci_resize(&s->stack,0);
+ veci_push(&s->stack,lit_var(l));
+
+ while (veci_size(&s->stack) > 0){
+ clause* c;
+ int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+ assert(v >= 0 && v < s->size);
+ veci_resize(&s->stack,veci_size(&s->stack)-1);
+ assert(reasons[v] != 0);
+ c = reasons[v];
+
+ if (clause_is_lit(c)){
+ int v = lit_var(clause_read_lit(c));
+ if (tags[v] == l_Undef && levels[v] != 0){
+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+ veci_push(&s->stack,v);
+ tags[v] = l_True;
+ veci_push(&s->tagged,v);
+ }else{
+ int* tagged = veci_begin(&s->tagged);
+ int j;
+ for (j = top; j < veci_size(&s->tagged); j++)
+ tags[tagged[j]] = l_Undef;
+ veci_resize(&s->tagged,top);
+ return false;
+ }
+ }
+ }else{
+ lit* lits = clause_begin(c);
+ int i, j;
+
+ for (i = 1; i < clause_size(c); i++){
+ int v = lit_var(lits[i]);
+ if (tags[v] == l_Undef && levels[v] != 0){
+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+ veci_push(&s->stack,lit_var(lits[i]));
+ tags[v] = l_True;
+ veci_push(&s->tagged,v);
+ }else{
+ int* tagged = veci_begin(&s->tagged);
+ for (j = top; j < veci_size(&s->tagged); j++)
+ tags[tagged[j]] = l_Undef;
+ veci_resize(&s->tagged,top);
+ return false;
+ }
+ }
+ }
+ }
+ }
+
+ return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| analyzeFinal : (p : Lit) -> [void]
+|
+| Description:
+| Specialized analysis procedure to express the final conflict in terms of assumptions.
+| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+| stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+/*
+void Solver::analyzeFinal(Clause* confl, bool skip_first)
+{
+ // -- NOTE! This code is relatively untested. Please report bugs!
+ conflict.clear();
+ if (root_level == 0) return;
+
+ vec<char>& seen = analyze_seen;
+ for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
+ Var x = var((*confl)[i]);
+ if (level[x] > 0)
+ seen[x] = 1;
+ }
+
+ int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
+ for (int i = start; i >= trail_lim[0]; i--){
+ Var x = var(trail[i]);
+ if (seen[x]){
+ GClause r = reason[x];
+ if (r == GClause_NULL){
+ assert(level[x] > 0);
+ conflict.push(~trail[i]);
+ }else{
+ if (r.isLit()){
+ Lit p = r.lit();
+ if (level[var(p)] > 0)
+ seen[var(p)] = 1;
+ }else{
+ Clause& c = *r.clause();
+ for (int j = 1; j < c.size(); j++)
+ if (level[var(c[j])] > 0)
+ seen[var(c[j])] = 1;
+ }
+ }
+ seen[x] = 0;
+ }
+ }
+}
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+
+static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
+{
+ int i, j, start;
+ veci_resize(&s->conf_final,0);
+ if ( s->root_level == 0 )
+ return;
+ assert( veci_size(&s->tagged) == 0 );
+// assert( s->tags[lit_var(p)] == l_Undef );
+// s->tags[lit_var(p)] = l_True;
+ for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
+ {
+ int x = lit_var(clause_begin(conf)[i]);
+ if (s->levels[x] > 0)
+ {
+ s->tags[x] = l_True;
+ veci_push(&s->tagged,x);
+ }
+ }
+
+ start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
+ for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
+ int x = lit_var(s->trail[i]);
+ if (s->tags[x] == l_True){
+ if (s->reasons[x] == NULL){
+ assert(s->levels[x] > 0);
+ veci_push(&s->conf_final,lit_neg(s->trail[i]));
+ }else{
+ clause* c = s->reasons[x];
+ if (clause_is_lit(c)){
+ lit q = clause_read_lit(c);
+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+ if (s->levels[lit_var(q)] > 0)
+ {
+ s->tags[lit_var(q)] = l_True;
+ veci_push(&s->tagged,lit_var(q));
+ }
+ }
+ else{
+ int* lits = clause_begin(c);
+ for (j = 1; j < clause_size(c); j++)
+ if (s->levels[lit_var(lits[j])] > 0)
+ {
+ s->tags[lit_var(lits[j])] = l_True;
+ veci_push(&s->tagged,lit_var(lits[j]));
+ }
+ }
+ }
+ }
+ }
+ for (i = 0; i < veci_size(&s->tagged); i++)
+ s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
+ veci_resize(&s->tagged,0);
+}
+
+#endif
+
+
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+{
+ lit* trail = s->trail;
+ lbool* tags = s->tags;
+ clause** reasons = s->reasons;
+ int* levels = s->levels;
+ int cnt = 0;
+ lit p = lit_Undef;
+ int ind = s->qtail-1;
+ lit* lits;
+ int i, j, minl;
+ int* tagged;
+
+ veci_push(learnt,lit_Undef);
+
+ do{
+ assert(c != 0);
+
+ if (clause_is_lit(c)){
+ lit q = clause_read_lit(c);
+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+ tags[lit_var(q)] = l_True;
+ veci_push(&s->tagged,lit_var(q));
+ act_var_bump(s,lit_var(q));
+ if (levels[lit_var(q)] == sat_solver_dl(s))
+ cnt++;
+ else
+ veci_push(learnt,q);
+ }
+ }else{
+
+ if (clause_learnt(c))
+ act_clause_bump(s,c);
+
+ lits = clause_begin(c);
+ //printlits(lits,lits+clause_size(c)); printf("\n");
+ for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+ lit q = lits[j];
+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+ tags[lit_var(q)] = l_True;
+ veci_push(&s->tagged,lit_var(q));
+ act_var_bump(s,lit_var(q));
+ if (levels[lit_var(q)] == sat_solver_dl(s))
+ cnt++;
+ else
+ veci_push(learnt,q);
+ }
+ }
+ }
+
+ while (tags[lit_var(trail[ind--])] == l_Undef);
+
+ p = trail[ind+1];
+ c = reasons[lit_var(p)];
+ cnt--;
+
+ }while (cnt > 0);
+
+ *veci_begin(learnt) = lit_neg(p);
+
+ lits = veci_begin(learnt);
+ minl = 0;
+ for (i = 1; i < veci_size(learnt); i++){
+ int lev = levels[lit_var(lits[i])];
+ minl |= 1 << (lev & 31);
+ }
+
+ // simplify (full)
+ for (i = j = 1; i < veci_size(learnt); i++){
+ if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+ lits[j++] = lits[i];
+ }
+
+ // update size of learnt + statistics
+ veci_resize(learnt,j);
+ s->stats.tot_literals += j;
+
+ // clear tags
+ tagged = veci_begin(&s->tagged);
+ for (i = 0; i < veci_size(&s->tagged); i++)
+ tags[tagged[i]] = l_Undef;
+ veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+ for (i = 0; i < s->size; i++)
+ assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+ printf(L_IND"Learnt {", L_ind);
+ for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+ if (veci_size(learnt) > 1){
+ int max_i = 1;
+ int max = levels[lit_var(lits[1])];
+ lit tmp;
+
+ for (i = 2; i < veci_size(learnt); i++)
+ if (levels[lit_var(lits[i])] > max){
+ max = levels[lit_var(lits[i])];
+ max_i = i;
+ }
+
+ tmp = lits[1];
+ lits[1] = lits[max_i];
+ lits[max_i] = tmp;
+ }
+#ifdef VERBOSEDEBUG
+ {
+ int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+ printf(" } at level %d\n", lev);
+ }
+#endif
+}
+
+
+clause* sat_solver_propagate(sat_solver* s)
+{
+ lbool* values = s->assigns;
+ clause* confl = (clause*)0;
+ lit* lits;
+ lit false_lit;
+ lbool sig;
+
+ //printf("sat_solver_propagate\n");
+ while (confl == 0 && s->qtail - s->qhead > 0){
+ lit p = s->trail[s->qhead++];
+ vecp* ws = sat_solver_read_wlist(s,p);
+ clause **begin = (clause**)vecp_begin(ws);
+ clause **end = begin + vecp_size(ws);
+ clause **i, **j;
+
+ s->stats.propagations++;
+ s->simpdb_props--;
+
+ //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+ for (i = j = begin; i < end; ){
+ if (clause_is_lit(*i)){
+
+ int Lit = clause_read_lit(*i);
+ sig = !lit_sign(Lit); sig += sig - 1;
+ if (values[lit_var(Lit)] == sig){
+ *j++ = *i++;
+ continue;
+ }
+
+ *j++ = *i;
+ if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+ confl = s->binary;
+ (clause_begin(confl))[1] = lit_neg(p);
+ (clause_begin(confl))[0] = clause_read_lit(*i++);
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ }
+ }else{
+
+ lits = clause_begin(*i);
+
+ // Make sure the false literal is data[1]:
+ false_lit = lit_neg(p);
+ if (lits[0] == false_lit){
+ lits[0] = lits[1];
+ lits[1] = false_lit;
+ }
+ assert(lits[1] == false_lit);
+ //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+ // If 0th watch is true, then clause is already satisfied.
+ sig = !lit_sign(lits[0]); sig += sig - 1;
+ if (values[lit_var(lits[0])] == sig){
+ *j++ = *i;
+ }else{
+ // Look for new watch:
+ lit* stop = lits + clause_size(*i);
+ lit* k;
+ for (k = lits + 2; k < stop; k++){
+ lbool sig = lit_sign(*k); sig += sig - 1;
+ if (values[lit_var(*k)] != sig){
+ lits[1] = *k;
+ *k = false_lit;
+ vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+ goto next; }
+ }
+
+ *j++ = *i;
+ // Clause is unit under assignment:
+ if (!sat_solver_enqueue(s,lits[0], *i)){
+ confl = *i++;
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ }
+ }
+ }
+ next:
+ i++;
+ }
+
+ s->stats.inspects += j - (clause**)vecp_begin(ws);
+ vecp_resize(ws,j - (clause**)vecp_begin(ws));
+ }
+
+ return confl;
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver* sat_solver_new(void)
+{
+ sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
+ memset( s, 0, sizeof(sat_solver) );
+
+ // initialize vectors
+ vecp_new(&s->clauses);
+ vecp_new(&s->learnts);
+ veci_new(&s->order);
+ veci_new(&s->trail_lim);
+ veci_new(&s->tagged);
+ veci_new(&s->stack);
+ veci_new(&s->model);
+ veci_new(&s->act_vars);
+ veci_new(&s->temp_clause);
+ veci_new(&s->conf_final);
+
+ // initialize arrays
+ s->wlists = 0;
+ s->activity = 0;
+ s->factors = 0;
+ s->assigns = 0;
+ s->orderpos = 0;
+ s->reasons = 0;
+ s->levels = 0;
+ s->tags = 0;
+ s->trail = 0;
+
+
+ // initialize other vars
+ s->size = 0;
+ s->cap = 0;
+ s->qhead = 0;
+ s->qtail = 0;
+#ifdef USE_FLOAT_ACTIVITY
+ s->var_inc = 1;
+ s->cla_inc = 1;
+ s->var_decay = (float)(1 / 0.95 );
+ s->cla_decay = (float)(1 / 0.999 );
+#else
+ s->var_inc = (1 << 5);
+ s->cla_inc = (1 << 11);
+#endif
+ s->root_level = 0;
+ s->simpdb_assigns = 0;
+ s->simpdb_props = 0;
+ s->random_seed = 91648253;
+ s->progress_estimate = 0;
+ s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+ s->binary->size_learnt = (2 << 1);
+ s->verbosity = 0;
+
+ s->stats.starts = 0;
+ s->stats.decisions = 0;
+ s->stats.propagations = 0;
+ s->stats.inspects = 0;
+ s->stats.conflicts = 0;
+ s->stats.clauses = 0;
+ s->stats.clauses_literals = 0;
+ s->stats.learnts = 0;
+ s->stats.learnts_literals = 0;
+ s->stats.tot_literals = 0;
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ s->pMem = NULL;
+#else
+ s->pMem = Sat_MmStepStart( 10 );
+#endif
+ return s;
+}
+
+void sat_solver_setnvars(sat_solver* s,int n)
+{
+ int var;
+
+ if (s->cap < n){
+ int old_cap = s->cap;
+ while (s->cap < n) s->cap = s->cap*2+1;
+
+ s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2);
+#ifdef USE_FLOAT_ACTIVITY
+ s->activity = ABC_REALLOC(double, s->activity, s->cap);
+#else
+ s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
+#endif
+ s->factors = ABC_REALLOC(double, s->factors, s->cap);
+ s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap);
+ s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
+ s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap);
+ s->levels = ABC_REALLOC(int, s->levels, s->cap);
+ s->tags = ABC_REALLOC(lbool, s->tags, s->cap);
+ s->trail = ABC_REALLOC(lit, s->trail, s->cap);
+ s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
+ memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
+ }
+
+ for (var = s->size; var < n; var++){
+ assert(!s->wlists[2*var].size);
+ assert(!s->wlists[2*var+1].size);
+ if ( s->wlists[2*var].ptr == NULL )
+ vecp_new(&s->wlists[2*var]);
+ if ( s->wlists[2*var+1].ptr == NULL )
+ vecp_new(&s->wlists[2*var+1]);
+#ifdef USE_FLOAT_ACTIVITY
+ s->activity[var] = 0;
+#else
+ s->activity[var] = (1<<10);
+#endif
+ s->factors [var] = 0;
+ s->assigns [var] = l_Undef;
+ s->orderpos [var] = veci_size(&s->order);
+ s->reasons [var] = (clause*)0;
+ s->levels [var] = 0;
+ s->tags [var] = l_Undef;
+ s->polarity [var] = 0;
+
+ /* does not hold because variables enqueued at top level will not be reinserted in the heap
+ assert(veci_size(&s->order) == var);
+ */
+ veci_push(&s->order,var);
+ order_update(s, var);
+ }
+
+ s->size = n > s->size ? n : s->size;
+}
+
+void sat_solver_delete(sat_solver* s)
+{
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ int i;
+ for (i = 0; i < vecp_size(&s->clauses); i++)
+ ABC_FREE(vecp_begin(&s->clauses)[i]);
+ for (i = 0; i < vecp_size(&s->learnts); i++)
+ ABC_FREE(vecp_begin(&s->learnts)[i]);
+#else
+ Sat_MmStepStop( s->pMem, 0 );
+#endif
+
+ // delete vectors
+ vecp_delete(&s->clauses);
+ vecp_delete(&s->learnts);
+ veci_delete(&s->order);
+ veci_delete(&s->trail_lim);
+ veci_delete(&s->tagged);
+ veci_delete(&s->stack);
+ veci_delete(&s->model);
+ veci_delete(&s->act_vars);
+ veci_delete(&s->temp_clause);
+ veci_delete(&s->conf_final);
+ ABC_FREE(s->binary);
+
+ // delete arrays
+ if (s->wlists != 0){
+ int i;
+ for (i = 0; i < s->cap*2; i++)
+ vecp_delete(&s->wlists[i]);
+ ABC_FREE(s->wlists );
+ ABC_FREE(s->activity );
+ ABC_FREE(s->factors );
+ ABC_FREE(s->assigns );
+ ABC_FREE(s->orderpos );
+ ABC_FREE(s->reasons );
+ ABC_FREE(s->levels );
+ ABC_FREE(s->trail );
+ ABC_FREE(s->tags );
+ ABC_FREE(s->polarity );
+ }
+
+ sat_solver_store_free(s);
+ ABC_FREE(s);
+}
+
+void sat_solver_rollback( sat_solver* s )
+{
+ int i;
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ for (i = 0; i < vecp_size(&s->clauses); i++)
+ ABC_FREE(vecp_begin(&s->clauses)[i]);
+ for (i = 0; i < vecp_size(&s->learnts); i++)
+ ABC_FREE(vecp_begin(&s->learnts)[i]);
+#else
+ Sat_MmStepRestart( s->pMem );
+#endif
+ vecp_resize(&s->clauses, 0);
+ vecp_resize(&s->learnts, 0);
+ veci_resize(&s->trail_lim, 0);
+ veci_resize(&s->order, 0);
+ for ( i = 0; i < s->size*2; i++ )
+ s->wlists[i].size = 0;
+
+ // initialize other vars
+ s->size = 0;
+// s->cap = 0;
+ s->qhead = 0;
+ s->qtail = 0;
+#ifdef USE_FLOAT_ACTIVITY
+ s->var_inc = 1;
+ s->cla_inc = 1;
+ s->var_decay = (float)(1 / 0.95 );
+ s->cla_decay = (float)(1 / 0.999 );
+#else
+ s->var_inc = (1 << 5);
+ s->cla_inc = (1 << 11);
+#endif
+ s->root_level = 0;
+ s->simpdb_assigns = 0;
+ s->simpdb_props = 0;
+ s->random_seed = 91648253;
+ s->progress_estimate = 0;
+ s->verbosity = 0;
+
+ s->stats.starts = 0;
+ s->stats.decisions = 0;
+ s->stats.propagations = 0;
+ s->stats.inspects = 0;
+ s->stats.conflicts = 0;
+ s->stats.clauses = 0;
+ s->stats.clauses_literals = 0;
+ s->stats.learnts = 0;
+ s->stats.learnts_literals = 0;
+ s->stats.tot_literals = 0;
+}
+
+
+static void clause_remove(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ assert(lit_neg(lits[0]) < s->size*2);
+ assert(lit_neg(lits[1]) < s->size*2);
+
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+ assert(lits[0] < s->size*2);
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+ if (clause_learnt(c)){
+ s->stats.learnts--;
+ s->stats.learnts_literals -= clause_size(c);
+ }else{
+ s->stats.clauses--;
+ s->stats.clauses_literals -= clause_size(c);
+ }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ ABC_FREE(c);
+#else
+ Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+}
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ lbool* values = s->assigns;
+ int i;
+
+ assert(sat_solver_dl(s) == 0);
+
+ for (i = 0; i < clause_size(c); i++){
+ lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+ if (values[lit_var(lits[i])] == sig)
+ return l_True;
+ }
+ return l_False;
+}
+
+int sat_solver_simplify(sat_solver* s)
+{
+ clause** reasons;
+ int type;
+
+ assert(sat_solver_dl(s) == 0);
+
+ if (sat_solver_propagate(s) != 0)
+ return false;
+
+ if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+ return true;
+
+ reasons = s->reasons;
+ for (type = 0; type < 2; type++){
+ vecp* cs = type ? &s->learnts : &s->clauses;
+ clause** cls = (clause**)vecp_begin(cs);
+
+ int i, j;
+ for (j = i = 0; i < vecp_size(cs); i++){
+ if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+ clause_simplify(s,cls[i]) == l_True)
+ clause_remove(s,cls[i]);
+ else
+ cls[j++] = cls[i];
+ }
+ vecp_resize(cs,j);
+ }
+
+ s->simpdb_assigns = s->qhead;
+ // (shouldn't depend on 'stats' really, but it will do for now)
+ s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+ return true;
+}
+
+
+static int clause_cmp (const void* x, const void* y) {
+ return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void sat_solver_reducedb(sat_solver* s)
+{
+ int i, j;
+ double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+ clause** learnts = (clause**)vecp_begin(&s->learnts);
+ clause** reasons = s->reasons;
+
+ sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+ for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+ for (; i < vecp_size(&s->learnts); i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+
+ //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+ vecp_resize(&s->learnts,j);
+}
+
+int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+{
+ clause * c;
+ lit *i,*j;
+ int maxvar;
+ lbool* values;
+ lit last;
+
+ veci_resize( &s->temp_clause, 0 );
+ for ( i = begin; i < end; i++ )
+ veci_push( &s->temp_clause, *i );
+ begin = veci_begin( &s->temp_clause );
+ end = begin + veci_size( &s->temp_clause );
+
+ if (begin == end)
+ return false;
+
+ //printlits(begin,end); printf("\n");
+ // insertion sort
+ maxvar = lit_var(*begin);
+ for (i = begin + 1; i < end; i++){
+ lit l = *i;
+ maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+ for (j = i; j > begin && *(j-1) > l; j--)
+ *j = *(j-1);
+ *j = l;
+ }
+ sat_solver_setnvars(s,maxvar+1);
+// sat_solver_setnvars(s, lit_var(*(end-1))+1 );
+
+ ///////////////////////////////////
+ // add clause to internal storage
+ if ( s->pStore )
+ {
+ int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
+ assert( RetValue );
+ }
+ ///////////////////////////////////
+
+ //printlits(begin,end); printf("\n");
+ values = s->assigns;
+
+ // delete duplicates
+ last = lit_Undef;
+ for (i = j = begin; i < end; i++){
+ //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+ lbool sig = !lit_sign(*i); sig += sig - 1;
+ if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+ return true; // tautology
+ else if (*i != last && values[lit_var(*i)] == l_Undef)
+ last = *j++ = *i;
+ }
+// j = i;
+
+ if (j == begin) // empty clause
+ return false;
+
+ if (j - begin == 1) // unit clause
+ return sat_solver_enqueue(s,*begin,(clause*)0);
+
+ // create new clause
+ c = clause_create_new(s,begin,j,0);
+ if ( c )
+ vecp_push(&s->clauses,c);
+
+
+ s->stats.clauses++;
+ s->stats.clauses_literals += j - begin;
+
+ return true;
+}
+
+
+double luby(double y, int x)
+{
+ int size, seq;
+ for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
+ while (size-1 != x){
+ size = (size-1) >> 1;
+ seq--;
+ x = x % size;
+ }
+ return pow(y, (double)seq);
+}
+
+void luby_test()
+{
+ int i;
+ for ( i = 0; i < 20; i++ )
+ printf( "%d ", (int)luby(2,i) );
+ printf( "\n" );
+}
+
+static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
+{
+ int* levels = s->levels;
+ double var_decay = 0.95;
+ double clause_decay = 0.999;
+ double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
+
+ ABC_INT64_T conflictC = 0;
+ veci learnt_clause;
+ int i;
+
+ assert(s->root_level == sat_solver_dl(s));
+
+ s->nRestarts++;
+ s->stats.starts++;
+// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new()
+// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new()
+ veci_resize(&s->model,0);
+ veci_new(&learnt_clause);
+
+ // use activity factors in every even restart
+ if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
+// if ( veci_size(&s->act_vars) > 0 )
+ for ( i = 0; i < s->act_vars.size; i++ )
+ act_var_bump_factor(s, s->act_vars.ptr[i]);
+
+ // use activity factors in every restart
+ if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
+ for ( i = 0; i < s->act_vars.size; i++ )
+ act_var_bump_global(s, s->act_vars.ptr[i]);
+
+ for (;;){
+ clause* confl = sat_solver_propagate(s);
+ if (confl != 0){
+ // CONFLICT
+ int blevel;
+
+#ifdef VERBOSEDEBUG
+ printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+ s->stats.conflicts++; conflictC++;
+ if (sat_solver_dl(s) == s->root_level){
+#ifdef SAT_USE_ANALYZE_FINAL
+ sat_solver_analyze_final(s, confl, 0);
+#endif
+ veci_delete(&learnt_clause);
+ return l_False;
+ }
+
+ veci_resize(&learnt_clause,0);
+ sat_solver_analyze(s, confl, &learnt_clause);
+ blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+ blevel = s->root_level > blevel ? s->root_level : blevel;
+ sat_solver_canceluntil(s,blevel);
+ sat_solver_record(s,&learnt_clause);
+#ifdef SAT_USE_ANALYZE_FINAL
+// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
+ if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+#endif
+ act_var_decay(s);
+ act_clause_decay(s);
+
+ }else{
+ // NO CONFLICT
+ int next;
+
+ if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+ // Reached bound on number of conflicts:
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef; }
+
+ if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
+// (s->nInsLimit && s->stats.inspects > s->nInsLimit) )
+ (s->nInsLimit && s->stats.propagations > s->nInsLimit) )
+ {
+ // Reached bound on number of conflicts:
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef;
+ }
+
+ if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
+ // Simplify the set of problem clauses:
+ sat_solver_simplify(s);
+
+// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+ // Reduce the set of learnt clauses:
+// sat_solver_reducedb(s);
+
+ // New variable decision:
+ s->stats.decisions++;
+ next = order_select(s,(float)random_var_freq);
+
+ if (next == var_Undef){
+ // Model found:
+ lbool* values = s->assigns;
+ int i;
+ veci_resize(&s->model, 0);
+ for (i = 0; i < s->size; i++)
+ veci_push(&s->model,(int)values[i]);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+
+ /*
+ veci apa; veci_new(&apa);
+ for (i = 0; i < s->size; i++)
+ veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+ printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+ veci_delete(&apa);
+ */
+
+ return l_True;
+ }
+
+ if ( s->polarity[next] ) // positive polarity
+ sat_solver_assume(s,toLit(next));
+ else
+ sat_solver_assume(s,lit_neg(toLit(next)));
+ }
+ }
+
+ return l_Undef; // cannot happen
+}
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+ int restart_iter = 0;
+ ABC_INT64_T nof_conflicts;
+ ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3;
+ lbool status = l_Undef;
+ lbool* values = s->assigns;
+ lit* i;
+
+ ////////////////////////////////////////////////
+ if ( s->fSolved )
+ {
+ if ( s->pStore )
+ {
+ int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
+ assert( RetValue );
+ }
+ return l_False;
+ }
+ ////////////////////////////////////////////////
+
+ // set the external limits
+ s->nCalls++;
+ s->nRestarts = 0;
+ s->nConfLimit = 0;
+ s->nInsLimit = 0;
+ if ( nConfLimit )
+ s->nConfLimit = s->stats.conflicts + nConfLimit;
+ if ( nInsLimit )
+// s->nInsLimit = s->stats.inspects + nInsLimit;
+ s->nInsLimit = s->stats.propagations + nInsLimit;
+ if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
+ s->nConfLimit = nConfLimitGlobal;
+ if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
+ s->nInsLimit = nInsLimitGlobal;
+
+#ifndef SAT_USE_ANALYZE_FINAL
+
+ //printf("solve: "); printlits(begin, end); printf("\n");
+ for (i = begin; i < end; i++){
+ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+ case 1: // l_True:
+ break;
+ case 0: // l_Undef
+ sat_solver_assume(s, *i);
+ if (sat_solver_propagate(s) == NULL)
+ break;
+ // fallthrough
+ case -1: // l_False
+ sat_solver_canceluntil(s, 0);
+ return l_False;
+ }
+ }
+ s->root_level = sat_solver_dl(s);
+
+#endif
+
+/*
+ // Perform assumptions:
+ root_level = assumps.size();
+ for (int i = 0; i < assumps.size(); i++){
+ Lit p = assumps[i];
+ assert(var(p) < nVars());
+ if (!sat_solver_assume(p)){
+ GClause r = reason[var(p)];
+ if (r != GClause_NULL){
+ Clause* confl;
+ if (r.isLit()){
+ confl = propagate_tmpbin;
+ (*confl)[1] = ~p;
+ (*confl)[0] = r.lit();
+ }else
+ confl = r.clause();
+ analyzeFinal(confl, true);
+ conflict.push(~p);
+ }else
+ conflict.clear(),
+ conflict.push(~p);
+ cancelUntil(0);
+ return false; }
+ Clause* confl = propagate();
+ if (confl != NULL){
+ analyzeFinal(confl), assert(conflict.size() > 0);
+ cancelUntil(0);
+ return false; }
+ }
+ assert(root_level == decisionLevel());
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+ // Perform assumptions:
+ s->root_level = end - begin;
+ for ( i = begin; i < end; i++ )
+ {
+ lit p = *i;
+ assert(lit_var(p) < s->size);
+ veci_push(&s->trail_lim,s->qtail);
+ if (!sat_solver_enqueue(s,p,(clause*)0))
+ {
+ clause * r = s->reasons[lit_var(p)];
+ if (r != NULL)
+ {
+ clause* confl;
+ if (clause_is_lit(r))
+ {
+ confl = s->binary;
+ (clause_begin(confl))[1] = lit_neg(p);
+ (clause_begin(confl))[0] = clause_read_lit(r);
+ }
+ else
+ confl = r;
+ sat_solver_analyze_final(s, confl, 1);
+ veci_push(&s->conf_final, lit_neg(p));
+ }
+ else
+ {
+ veci_resize(&s->conf_final,0);
+ veci_push(&s->conf_final, lit_neg(p));
+ // the two lines below are a bug fix by Siert Wieringa
+ if (s->levels[lit_var(p)] > 0)
+ veci_push(&s->conf_final, p);
+ }
+ sat_solver_canceluntil(s, 0);
+ return l_False;
+ }
+ else
+ {
+ clause* confl = sat_solver_propagate(s);
+ if (confl != NULL){
+ sat_solver_analyze_final(s, confl, 0);
+ assert(s->conf_final.size > 0);
+ sat_solver_canceluntil(s, 0);
+ return l_False; }
+ }
+ }
+ assert(s->root_level == sat_solver_dl(s));
+#endif
+
+ s->nCalls2++;
+
+ if (s->verbosity >= 1){
+ printf("==================================[MINISAT]===================================\n");
+ printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
+ printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
+ printf("==============================================================================\n");
+ }
+
+ while (status == l_Undef){
+// int nConfs = 0;
+ double Ratio = (s->stats.learnts == 0)? 0.0 :
+ s->stats.learnts_literals / (double)s->stats.learnts;
+ if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+ break;
+
+ if (s->verbosity >= 1)
+ {
+ printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
+ (double)s->stats.conflicts,
+ (double)s->stats.clauses,
+ (double)s->stats.clauses_literals,
+ (double)nof_learnts,
+ (double)s->stats.learnts,
+ (double)s->stats.learnts_literals,
+ Ratio,
+ s->progress_estimate*100);
+ fflush(stdout);
+ }
+ nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
+//printf( "%d ", (int)nof_conflicts );
+// nConfs = s->stats.conflicts;
+ status = sat_solver_search(s, nof_conflicts, nof_learnts);
+// if ( status == l_True )
+// printf( "%d ", s->stats.conflicts - nConfs );
+
+// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
+ nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
+//printf( "%d ", s->stats.conflicts );
+ // quit the loop if reached an external limit
+ if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+ {
+// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+ break;
+ }
+// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
+ if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
+ {
+// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+ break;
+ }
+ if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+ break;
+ }
+//printf( "\n" );
+ if (s->verbosity >= 1)
+ printf("==============================================================================\n");
+
+ sat_solver_canceluntil(s,0);
+
+ ////////////////////////////////////////////////
+ if ( status == l_False && s->pStore )
+ {
+ int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
+ assert( RetValue );
+ }
+ ////////////////////////////////////////////////
+ return status;
+}
+
+
+int sat_solver_nvars(sat_solver* s)
+{
+ return s->size;
+}
+
+
+int sat_solver_nclauses(sat_solver* s)
+{
+ return vecp_size(&s->clauses);
+}
+
+
+int sat_solver_nconflicts(sat_solver* s)
+{
+ return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Clause storage functions:
+
+void sat_solver_store_alloc( sat_solver * s )
+{
+ assert( s->pStore == NULL );
+ s->pStore = Sto_ManAlloc();
+}
+
+void sat_solver_store_write( sat_solver * s, char * pFileName )
+{
+ if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
+}
+
+void sat_solver_store_free( sat_solver * s )
+{
+ if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
+ s->pStore = NULL;
+}
+
+int sat_solver_store_change_last( sat_solver * s )
+{
+ if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
+ return -1;
+}
+
+void sat_solver_store_mark_roots( sat_solver * s )
+{
+ if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
+}
+
+void sat_solver_store_mark_clauses_a( sat_solver * s )
+{
+ if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
+}
+
+void * sat_solver_store_release( sat_solver * s )
+{
+ void * pTemp;
+ if ( s->pStore == NULL )
+ return NULL;
+ pTemp = s->pStore;
+ s->pStore = NULL;
+ return pTemp;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+ int i, j, best_i;
+ void* tmp;
+
+ for (i = 0; i < size-1; i++){
+ best_i = i;
+ for (j = i+1; j < size; j++){
+ if (comp(array[j], array[best_i]) < 0)
+ best_i = j;
+ }
+ tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+ }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+ if (size <= 15)
+ selectionsort(array, size, comp);
+
+ else{
+ void* pivot = array[irand(seed, size)];
+ void* tmp;
+ int i = -1;
+ int j = size;
+
+ for(;;){
+ do i++; while(comp(array[i], pivot)<0);
+ do j--; while(comp(pivot, array[j])<0);
+
+ if (i >= j) break;
+
+ tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+ }
+
+ sortrnd(array , i , comp, seed);
+ sortrnd(&array[i], size-i, comp, seed);
+ }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+// int i;
+ double seed = 91648253;
+ sortrnd(array,size,comp,&seed);
+// for ( i = 1; i < size; i++ )
+// assert(comp(array[i-1], array[i])<0);
+}
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satSolver_old.h b/src/sat/bsat/satSolver_old.h
new file mode 100644
index 00000000..4c577b1e
--- /dev/null
+++ b/src/sat/bsat/satSolver_old.h
@@ -0,0 +1,210 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver_h
+#define satSolver_h
+
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "satVec.h"
+#include "satMem.h"
+
+ABC_NAMESPACE_HEADER_START
+
+//#define USE_FLOAT_ACTIVITY
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
+
+extern sat_solver* sat_solver_new(void);
+extern void sat_solver_delete(sat_solver* s);
+
+extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern int sat_solver_simplify(sat_solver* s);
+extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern void sat_solver_rollback( sat_solver* s );
+
+extern int sat_solver_nvars(sat_solver* s);
+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);
+
+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 );
+extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar );
+
+// trace recording
+extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName );
+extern void Sat_SolverTraceStop( sat_solver * pSat );
+extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void sat_solver_store_alloc( sat_solver * s );
+extern void sat_solver_store_write( sat_solver * s, char * pFileName );
+extern void sat_solver_store_free( sat_solver * s );
+extern void sat_solver_store_mark_roots( sat_solver * s );
+extern void sat_solver_store_mark_clauses_a( sat_solver * s );
+extern void * sat_solver_store_release( sat_solver * s );
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver_t
+{
+ int size; // nof variables
+ int cap; // size of varmaps
+ int qhead; // Head index of queue.
+ int qtail; // Tail index of queue.
+
+ // clauses
+ vecp clauses; // List of problem constraints. (contains: clause*)
+ vecp learnts; // List of learnt clauses. (contains: clause*)
+
+ // activities
+#ifdef USE_FLOAT_ACTIVITY
+ double var_inc; // Amount to bump next variable with.
+ double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
+ float cla_inc; // Amount to bump next clause with.
+ float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
+ double* activity; // A heuristic measurement of the activity of a variable.
+#else
+ int var_inc; // Amount to bump next variable with.
+ int cla_inc; // Amount to bump next clause with.
+ unsigned*activity; // A heuristic measurement of the activity of a variable.
+#endif
+
+ vecp* wlists; //
+ lbool* assigns; // Current values of variables.
+ int* orderpos; // Index in variable order.
+ clause** reasons; //
+ int* levels; //
+ lit* trail;
+ char* polarity;
+
+ clause* binary; // A temporary binary clause
+ lbool* tags; //
+ veci tagged; // (contains: var)
+ veci stack; // (contains: var)
+
+ veci order; // Variable order. (heap) (contains: var)
+ veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
+ veci model; // If problem is solved, this vector contains the model (contains: lbool).
+ veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
+ // this vector represent the final conflict clause expressed in the assumptions.
+
+ int root_level; // Level of first proper decision.
+ int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+ int simpdb_props; // Number of propagations before next 'simplifyDB()'.
+ double random_seed;
+ double progress_estimate;
+ int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+ stats_t stats;
+
+ ABC_INT64_T nConfLimit; // external limit on the number of conflicts
+ ABC_INT64_T nInsLimit; // external limit on the number of implications
+ int nRuntimeLimit; // external limit on runtime
+
+ veci act_vars; // variables whose activity has changed
+ double* factors; // the activity factors
+ int nRestarts; // the number of local restarts
+ int nCalls; // the number of local restarts
+ int nCalls2; // the number of local restarts
+
+ Sat_MmStep_t * pMem;
+
+ int fSkipSimplify; // set to one to skip simplification of the clause database
+ int fNotUseRandom; // do not allow random decisions with a fixed probability
+
+ int * pGlobalVars; // for experiments with global vars during interpolation
+ // clause store
+ void * pStore;
+ int fSolved;
+
+ // trace recording
+ FILE * pFile;
+ int nClauses;
+ int nRoots;
+
+ veci temp_clause; // temporary storage for a CNF clause
+};
+
+static int sat_solver_var_value( sat_solver* s, int v )
+{
+ assert( s->model.ptr != NULL && v < s->size );
+ return (int)(s->model.ptr[v] == l_True);
+}
+static int sat_solver_var_literal( sat_solver* s, int v )
+{
+ assert( s->model.ptr != NULL && v < s->size );
+ return toLitCond( v, s->model.ptr[v] != l_True );
+}
+static void sat_solver_act_var_clear(sat_solver* s)
+{
+ int i;
+ for (i = 0; i < s->size; i++)
+ s->activity[i] = 0.0;
+ s->var_inc = 1.0;
+}
+static void sat_solver_compress(sat_solver* s)
+{
+ if ( s->qtail != s->qhead )
+ {
+ int RetValue = sat_solver_simplify(s);
+ assert( RetValue != 0 );
+ }
+}
+
+static int sat_solver_final(sat_solver* s, int ** ppArray)
+{
+ *ppArray = s->conf_final.ptr;
+ return s->conf_final.size;
+}
+
+static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
+{
+ int nRuntimeLimit = s->nRuntimeLimit;
+ s->nRuntimeLimit = Limit;
+ return nRuntimeLimit;
+}
+
+static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
+{
+ int fNotUseRandomOld = s->fNotUseRandom;
+ s->fNotUseRandom = fNotUseRandom;
+ return fNotUseRandomOld;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 17a9ba4a..5e809172 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -58,6 +58,7 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
***********************************************************************/
void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
{
+/*
FILE * pFile;
void ** pClauses;
int nClauses, i;
@@ -110,6 +111,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
fprintf( pFile, "\n" );
fclose( pFile );
+*/
}
/**Function*************************************************************
@@ -273,6 +275,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
***********************************************************************/
void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
{
+/*
clause * pClause;
lit Lit, * pLits;
int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
@@ -305,6 +308,7 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
for ( v = 0; v < nLits; v++ )
pLits[v] -= nLitsOld;
}
+*/
}
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
index d81cc631..fd0cc242 100644
--- a/src/sat/bsat/vecRec.h
+++ b/src/sat/bsat/vecRec.h
@@ -66,6 +66,9 @@ struct Vec_Rec_t_
for ( c = 1; c <= p->nChunks; c++ ) \
for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
+#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart ) \
+ for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 ) \
+ for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -97,6 +100,22 @@ static inline Vec_Rec_t * Vec_RecAlloc()
p->pChunks[1][0] = 0;
return p;
}
+static inline void Vec_RecAlloc_( Vec_Rec_t * p )
+{
+// Vec_Rec_t * p;
+// p = ABC_CALLOC( Vec_Rec_t, 1 );
+ memset( p, 0, sizeof(Vec_Rec_t) );
+ p->LogSize = 15; // chunk size = 2^15 ints = 128 Kb
+ p->Mask = (1 << p->LogSize) - 1;
+ p->hCurrent = (1 << 16);
+ p->nChunks = 1;
+ p->nChunksAlloc = 16;
+ p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc );
+ p->pChunks[0] = NULL;
+ p->pChunks[1] = ABC_ALLOC( int, (1 << 16) );
+ p->pChunks[1][0] = 0;
+// return p;
+}
/**Function*************************************************************
@@ -239,6 +258,14 @@ static inline void Vec_RecFree( Vec_Rec_t * p )
ABC_FREE( p->pChunks );
ABC_FREE( p );
}
+static inline void Vec_RecFree_( Vec_Rec_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nChunksAlloc; i++ )
+ ABC_FREE( p->pChunks[i] );
+ ABC_FREE( p->pChunks );
+// ABC_FREE( p );
+}
/**Function*************************************************************