diff options
Diffstat (limited to 'src/sat/asat')
| -rw-r--r-- | src/sat/asat/added.c | 24 | ||||
| -rw-r--r-- | src/sat/asat/asat60525.zip | bin | 0 -> 25597 bytes | |||
| -rw-r--r-- | src/sat/asat/jfront.c | 4 | ||||
| -rw-r--r-- | src/sat/asat/solver.c | 201 | ||||
| -rw-r--r-- | src/sat/asat/solver.h | 26 | ||||
| -rw-r--r-- | src/sat/asat/solver_vec.h | 30 |
6 files changed, 184 insertions, 101 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index e1b1bb2a..832bc0cf 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -158,7 +158,7 @@ int * solver_get_model( solver * p, int * pVars, int nVars ) for ( i = 0; i < nVars; i++ ) { assert( pVars[i] >= 0 && pVars[i] < p->size ); - pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True); + pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True); } return pModel; } @@ -188,6 +188,28 @@ void Asat_SatPrintStats( FILE * pFile, solver * p ) (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) ); } +/**Function************************************************************* + + Synopsis [Sets the preferred variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) +{ + int i; + assert( s->pPrefVars == NULL ); + for ( i = 0; i < nPrefVars; i++ ) + assert( pPrefVars[i] < s->size ); + s->pPrefVars = pPrefVars; + s->nPrefVars = nPrefVars; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/asat60525.zip b/src/sat/asat/asat60525.zip Binary files differnew file mode 100644 index 00000000..b8361af1 --- /dev/null +++ b/src/sat/asat/asat60525.zip diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c index 1def6a37..8e673cc9 100644 --- a/src/sat/asat/jfront.c +++ b/src/sat/asat/jfront.c @@ -95,7 +95,7 @@ static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ); // iterator through the adjacent variables #define Asat_JVarForEachFanio( p, pVar, pFan, i ) \ - for ( i = 0; (i < pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ ) + for ( i = 0; (i < (int)pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ ) extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); @@ -223,7 +223,7 @@ int Asat_JManCheck( Asat_JMan_t * p ) // assert( i != pVar->nFans ); // if ( i == pVar->nFans ) // return 0; - if ( i == pVar->nFans ) + if ( i == (int)pVar->nFans ) Counter++; } if ( Counter > 0 ) diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 6d76d890..548abd1d 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "solver.h" -//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT +#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT //================================================================================================= // Simple (var/literal) helpers: @@ -96,14 +96,14 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ //================================================================================================= // Encode literals in clause pointers: -clause* clause_from_lit (lit l) { return (clause*)(l + l + 1); } -bool clause_is_lit (clause* c) { return ((unsigned int)c & 1); } -lit clause_read_lit (clause* c) { return (lit)((unsigned int)c >> 1); } +clause* clause_from_lit (lit l) { return (clause*)(((unsigned long)l) + ((unsigned long)l) + 1); } +bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } +lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } //================================================================================================= // Simple helpers: -static inline int solver_dlevel(solver* s) { return vec_size(&s->trail_lim); } +static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); } static inline vec* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; } static inline void vec_remove(vec* v, void* e) { @@ -124,7 +124,7 @@ static inline void order_update(solver* s, int v) // updateorder // int clk = clock(); int* orderpos = s->orderpos; double* activity = s->activity; - int* heap = (int*)vec_begin(&s->order); + int* heap = veci_begin(&s->order); int i = orderpos[v]; int x = heap[i]; int parent = (i - 1) / 2; @@ -151,8 +151,8 @@ static inline void order_unassigned(solver* s, int v) // undoorder // int clk = clock(); int* orderpos = s->orderpos; if (orderpos[v] == -1){ - orderpos[v] = vec_size(&s->order); - vec_push(&s->order,(void*)v); + orderpos[v] = veci_size(&s->order); + veci_push(&s->order,v); order_update(s,v); } // s->timeUpdate += clock() - clk; @@ -161,12 +161,23 @@ static inline void order_unassigned(solver* s, int v) // undoorder static int order_select(solver* s, float random_var_freq) // selectvar { // int clk = clock(); + static int Counter = 0; int* heap; double* activity; int* orderpos; lbool* values = s->assigns; + // The first decisions + if ( s->pPrefVars && s->nPrefDecNum < s->nPrefVars ) + { + int i; + s->nPrefDecNum++; + for ( i = 0; i < s->nPrefVars; i++ ) + if ( values[s->pPrefVars[i]] == l_Undef ) + return s->pPrefVars[i]; + } + // Random decision: if (drand(&s->random_seed) < random_var_freq){ int next = irand(&s->random_seed,s->size); @@ -177,17 +188,17 @@ static int order_select(solver* s, float random_var_freq) // selectvar // Activity based decision: - heap = (int*)vec_begin(&s->order); + heap = veci_begin(&s->order); activity = s->activity; orderpos = s->orderpos; - while (vec_size(&s->order) > 0){ + while (veci_size(&s->order) > 0){ int next = heap[0]; - int size = vec_size(&s->order)-1; + int size = veci_size(&s->order)-1; int x = heap[size]; - vec_resize(&s->order,size); + veci_resize(&s->order,size); orderpos[next] = -1; @@ -300,7 +311,10 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) assert(((unsigned int)c & 1) == 0); for (i = 0; i < size; i++) + { + assert(begin[i] >= 0); c->lits[i] = begin[i]; + } if (learnt) *((float*)&c->lits[size]) = 0.0; @@ -328,11 +342,11 @@ static void clause_remove(solver* s, clause* c) lit* lits = clause_begin(c); assert(neg(lits[0]) < s->size*2); assert(neg(lits[1]) < s->size*2); + assert(lits[0] < s->size*2); //vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)c); //vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)c); - assert(lits[0] < s->size*2); vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); @@ -399,8 +413,8 @@ static void solver_setnvars(solver* s,int n) s->levels [var] = 0; s->tags [var] = l_Undef; - assert(vec_size(&s->order) == var); - vec_push(&s->order,(void*)var); + assert(veci_size(&s->order) == var); + veci_push(&s->order,var); order_update(s,var); } @@ -413,20 +427,19 @@ static inline bool enqueue(solver* s, lit l, clause* from) lbool* values = s->assigns; int v = lit_var(l); lbool val = values[v]; + lbool sig = !lit_sign(l); sig += sig - 1; #ifdef VERBOSEDEBUG printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); #endif - - lbool sig = !lit_sign(l); sig += sig - 1; if (val != l_Undef){ return val == sig; }else{ // New fact -- store it. + int* levels = s->levels; + clause** reasons = s->reasons; #ifdef VERBOSEDEBUG printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); #endif - int* levels = s->levels; - clause** reasons = s->reasons; values [v] = sig; levels [v] = solver_dlevel(s); @@ -448,7 +461,7 @@ static inline void assume(solver* s, lit l){ #ifdef VERBOSEDEBUG printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); #endif - vec_push(&s->trail_lim,(void*)s->qtail); + veci_push(&s->trail_lim,s->qtail); enqueue(s,l,(clause*)0); } @@ -466,7 +479,7 @@ static inline void solver_canceluntil(solver* s, int level) { trail = s->trail; values = s->assigns; reasons = s->reasons; - bound = ((int*)vec_begin(&s->trail_lim))[level]; + bound = veci_begin(&s->trail_lim)[level]; for (c = s->qtail-1; c >= bound; c--) { int x = lit_var(trail[c]); @@ -482,23 +495,23 @@ static inline void solver_canceluntil(solver* s, int level) { order_unassigned( s, lit_var(trail[c]) ); s->qhead = s->qtail = bound; - vec_resize(&s->trail_lim,level); + veci_resize(&s->trail_lim,level); } -static void solver_record(solver* s, vec* cls) +static void solver_record(solver* s, veci* cls) { - lit* begin = (lit*)vec_begin(cls); - lit* end = begin + vec_size(cls); - clause* c = (vec_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; + lit* begin = veci_begin(cls); + lit* end = begin + veci_size(cls); + clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; enqueue(s,*begin,c); - assert(vec_size(cls) > 0); + assert(veci_size(cls) > 0); if (c != 0) { vec_push(&s->learnts,(void*)c); act_clause_bump(s,c); s->solver_stats.learnts++; - s->solver_stats.learnts_literals += vec_size(cls); + s->solver_stats.learnts_literals += veci_size(cls); } } @@ -525,18 +538,18 @@ static bool solver_lit_removable(solver* s, lit l, int minl) lbool* tags = s->tags; clause** reasons = s->reasons; int* levels = s->levels; - int top = vec_size(&s->tagged); + int top = veci_size(&s->tagged); assert(lit_var(l) >= 0 && lit_var(l) < s->size); assert(reasons[lit_var(l)] != 0); - vec_resize(&s->stack,0); - vec_push(&s->stack,(void*)lit_var(l)); + veci_resize(&s->stack,0); + veci_push(&s->stack,lit_var(l)); - while (vec_size(&s->stack) > 0){ + while (veci_size(&s->stack) > 0){ clause* c; - int v = (int)vec_begin(&s->stack)[vec_size(&s->stack)-1]; + int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; assert(v >= 0 && v < s->size); - vec_resize(&s->stack,vec_size(&s->stack)-1); + veci_resize(&s->stack,veci_size(&s->stack)-1); assert(reasons[v] != 0); c = reasons[v]; @@ -544,15 +557,15 @@ static bool solver_lit_removable(solver* s, lit l, int minl) 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)){ - vec_push(&s->stack,(void*)v); + veci_push(&s->stack,v); tags[v] = l_True; - vec_push(&s->tagged,(void*)v); + veci_push(&s->tagged,v); }else{ - int* tagged = (int*)vec_begin(&s->tagged); + int* tagged = veci_begin(&s->tagged); int j; - for (j = top; j < vec_size(&s->tagged); j++) + for (j = top; j < veci_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; - vec_resize(&s->tagged,top); + veci_resize(&s->tagged,top); return 0; } } @@ -565,14 +578,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl) if (tags[v] == l_Undef && levels[v] != 0){ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - vec_push(&s->stack,(void*)lit_var(lits[i])); + veci_push(&s->stack,lit_var(lits[i])); tags[v] = l_True; - vec_push(&s->tagged,(void*)v); + veci_push(&s->tagged,v); }else{ - int* tagged = (int*)vec_begin(&s->tagged); - for (j = top; j < vec_size(&s->tagged); j++) + int* tagged = veci_begin(&s->tagged); + for (j = top; j < veci_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; - vec_resize(&s->tagged,top); + veci_resize(&s->tagged,top); return 0; } } @@ -583,7 +596,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl) return 1; } -static void solver_analyze(solver* s, clause* c, vec* learnt) +static void solver_analyze(solver* s, clause* c, veci* learnt) { lit* trail = s->trail; lbool* tags = s->tags; @@ -596,7 +609,7 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) int i, j, minl; int* tagged; - vec_push(learnt,(void*)lit_Undef); + veci_push(learnt,lit_Undef); do{ assert(c != 0); @@ -606,12 +619,12 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) 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; - vec_push(&s->tagged,(void*)lit_var(q)); + veci_push(&s->tagged,lit_var(q)); act_var_bump(s,lit_var(q)); if (levels[lit_var(q)] == solver_dlevel(s)) cnt++; else - vec_push(learnt,(void*)q); + veci_push(learnt,q); } }else{ @@ -625,12 +638,12 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) 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; - vec_push(&s->tagged,(void*)lit_var(q)); + veci_push(&s->tagged,lit_var(q)); act_var_bump(s,lit_var(q)); if (levels[lit_var(q)] == solver_dlevel(s)) cnt++; else - vec_push(learnt,(void*)q); + veci_push(learnt,q); } } } @@ -643,31 +656,34 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) }while (cnt > 0); - *(lit*)vec_begin(learnt) = neg(p); +// *veci_begin(learnt) = neg(p); + + lits = veci_begin(learnt); + lits[0] = neg(p); - lits = (lit*)vec_begin(learnt); minl = 0; - for (i = 1; i < vec_size(learnt); i++){ + 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 < vec_size(learnt); i++){ + for (i = j = 1; i < veci_size(learnt); i++){ if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl)) lits[j++] = lits[i]; } +// j = veci_size(learnt); // update size of learnt + statistics - s->solver_stats.max_literals += vec_size(learnt); - vec_resize(learnt,j); + s->solver_stats.max_literals += veci_size(learnt); + veci_resize(learnt,j); s->solver_stats.tot_literals += j; // clear tags - tagged = (int*)vec_begin(&s->tagged); - for (i = 0; i < vec_size(&s->tagged); i++) + tagged = veci_begin(&s->tagged); + for (i = 0; i < veci_size(&s->tagged); i++) tags[tagged[i]] = l_Undef; - vec_resize(&s->tagged,0); + veci_resize(&s->tagged,0); #ifdef DEBUG for (i = 0; i < s->size; i++) @@ -676,14 +692,14 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) #ifdef VERBOSEDEBUG printf(L_IND"Learnt {", L_ind); - for (i = 0; i < vec_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); + for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); #endif - if (vec_size(learnt) > 1){ + if (veci_size(learnt) > 1){ int max_i = 1; int max = levels[lit_var(lits[1])]; lit tmp; - for (i = 2; i < vec_size(learnt); i++) + for (i = 2; i < veci_size(learnt); i++) if (levels[lit_var(lits[i])] > max){ max = levels[lit_var(lits[i])]; max_i = i; @@ -695,7 +711,7 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) } #ifdef VERBOSEDEBUG { - int lev = vec_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; + int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; printf(" } at level %d\n", lev); } #endif @@ -824,15 +840,15 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) double random_var_freq = 0.0;//0.02; int conflictC = 0; - vec learnt_clause; + veci learnt_clause; assert(s->root_level == solver_dlevel(s)); s->solver_stats.starts++; s->var_decay = (float)(1 / var_decay ); s->cla_decay = (float)(1 / clause_decay); - vec_resize(&s->model,0); - vec_new(&learnt_clause); + veci_resize(&s->model,0); + veci_new(&learnt_clause); for (;;){ clause* confl = solver_propagate(s); @@ -845,13 +861,13 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) #endif s->solver_stats.conflicts++; conflictC++; if (solver_dlevel(s) == s->root_level){ - vec_delete(&learnt_clause); + veci_delete(&learnt_clause); return l_False; } - vec_resize(&learnt_clause,0); + veci_resize(&learnt_clause,0); solver_analyze(s, confl, &learnt_clause); - blevel = vec_size(&learnt_clause) > 1 ? levels[lit_var(((lit*)vec_begin(&learnt_clause))[1])] : s->root_level; + blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; solver_canceluntil(s,blevel); solver_record(s,&learnt_clause); act_var_decay(s); @@ -866,17 +882,17 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) // Reached bound on number of conflicts: s->progress_estimate = solver_progress(s); solver_canceluntil(s,s->root_level); - vec_delete(&learnt_clause); + veci_delete(&learnt_clause); return l_Undef; } - if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit || - s->nImpLimit && s->solver_stats.propagations > s->nImpLimit ) + if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit || + s->nInsLimit && s->solver_stats.inspects > s->nInsLimit ) { // Reached bound on number of conflicts: s->progress_estimate = solver_progress(s); solver_canceluntil(s,s->root_level); - vec_delete(&learnt_clause); + veci_delete(&learnt_clause); return l_Undef; } @@ -899,9 +915,9 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) // Model found: lbool* values = s->assigns; int i; - for (i = 0; i < s->size; i++) vec_push(&s->model,(void*)((int)values[i])); + for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]); solver_canceluntil(s,s->root_level); - vec_delete(&learnt_clause); + veci_delete(&learnt_clause); return l_True; } @@ -922,11 +938,11 @@ solver* solver_new(void) // initialize vectors vec_new(&s->clauses); vec_new(&s->learnts); - vec_new(&s->order); - vec_new(&s->trail_lim); - vec_new(&s->tagged); - vec_new(&s->stack); - vec_new(&s->model); + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); + veci_new(&s->stack); + veci_new(&s->model); // initialize arrays s->wlists = 0; @@ -975,6 +991,8 @@ solver* solver_new(void) s->pMem = Asat_MmStepStart( 10 ); #endif s->pJMan = NULL; + s->pPrefVars = NULL; + s->nPrefVars = 0; s->timeTotal = clock(); s->timeSelect = 0; s->timeUpdate = 0; @@ -998,11 +1016,11 @@ void solver_delete(solver* s) // delete vectors vec_delete(&s->clauses); vec_delete(&s->learnts); - vec_delete(&s->order); - vec_delete(&s->trail_lim); - vec_delete(&s->tagged); - vec_delete(&s->stack); - vec_delete(&s->model); + veci_delete(&s->order); + veci_delete(&s->trail_lim); + veci_delete(&s->tagged); + veci_delete(&s->stack); + veci_delete(&s->model); free(s->binary); // delete arrays @@ -1022,7 +1040,8 @@ void solver_delete(solver* s) free(s->tags ); } - if ( s->pJMan ) Asat_JManStop( s ); + if ( s->pJMan ) Asat_JManStop( s ); + if ( s->pPrefVars ) free( s->pPrefVars ); free(s); } @@ -1117,9 +1136,10 @@ bool solver_simplify(solver* s) } -bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit ) +bool solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit ) { double nof_conflicts = 100; +// double nof_conflicts = 1000000; double nof_learnts = solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; @@ -1127,7 +1147,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit // set the external limits s->nConfLimit = nConfLimit; // external limit on the number of conflicts - s->nImpLimit = nImpLimit; // external limit on the number of implications + s->nInsLimit = nInsLimit; // external limit on the number of implications for (i = begin; i < end; i++) @@ -1160,6 +1180,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit s->progress_estimate*100); fflush(stdout); } + s->nPrefDecNum = 0; status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); nof_conflicts *= 1.5; nof_learnts *= 1.1; @@ -1170,9 +1191,9 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit // printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); break; } - if ( s->nImpLimit && s->solver_stats.propagations > s->nImpLimit ) + if ( s->nInsLimit && s->solver_stats.inspects > s->nInsLimit ) { -// printf( "Reached the limit on the number of implications (%d).\n", s->nImpLimit ); +// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); break; } } diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 3684d259..05e9dafa 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -37,9 +37,11 @@ extern "C" { // Simple types: //typedef int bool; +#ifndef __cplusplus #ifndef bool #define bool int #endif +#endif typedef int lit; typedef char lbool; @@ -74,17 +76,19 @@ extern void solver_delete(solver* s); extern bool solver_addclause(solver* s, lit* begin, lit* end); extern bool solver_simplify(solver* s); -extern int solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit ); +extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit ); extern int * solver_get_model( solver * p, int * pVars, int nVars ); extern int solver_nvars(solver* s); extern int solver_nclauses(solver* s); + // additional procedures extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars); extern void Asat_SatPrintStats( FILE * pFile, solver * p ); +extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); // J-frontier support extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); @@ -131,12 +135,12 @@ struct solver_t clause* binary; // A temporary binary clause lbool* tags; // - vec tagged; // (contains: var) - vec stack; // (contains: var) + veci tagged; // (contains: var) + veci stack; // (contains: var) - vec order; // Variable order. (heap) (contains: var) - vec trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - vec model; // If problem is solved, this vector contains the model (contains: lbool). + 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). int root_level; // Level of first proper decision. int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. @@ -145,8 +149,8 @@ struct solver_t double progress_estimate; int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - int nConfLimit; // external limit on the number of conflicts - int nImpLimit; // external limit on the number of implications + sint64 nConfLimit; // external limit on the number of conflicts + sint64 nInsLimit; // external limit on the number of implications // the memory manager Asat_MmStep_t * pMem; @@ -154,6 +158,12 @@ struct solver_t // J-frontier Asat_JMan_t * pJMan; + // for making decisions on some variables first + int nPrefDecNum; + int * pPrefVars; + int nPrefVars; + + // solver statistics stats solver_stats; int timeTotal; int timeSelect; diff --git a/src/sat/asat/solver_vec.h b/src/sat/asat/solver_vec.h index fae313d0..1ae30b0a 100644 --- a/src/sat/asat/solver_vec.h +++ b/src/sat/asat/solver_vec.h @@ -24,6 +24,35 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <stdlib.h> +// vector of 32-bit intergers (added for 64-bit portability) +struct veci_t { + int size; + int cap; + int* ptr; +}; +typedef struct veci_t veci; + +static inline void veci_new (veci* v) { + v->size = 0; + v->cap = 4; + v->ptr = (int*)malloc(sizeof(int)*v->cap); +} + +static inline void veci_delete (veci* v) { free(v->ptr); } +static inline int* veci_begin (veci* v) { return v->ptr; } +static inline int veci_size (veci* v) { return v->size; } +static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! +static inline void veci_push (veci* v, int e) +{ + if (v->size == v->cap) { + int newsize = v->cap * 2+1; + v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); + v->cap = newsize; } + v->ptr[v->size++] = e; +} + + +// vector of 32- or 64-bit pointers struct vec_t { int size; int cap; @@ -50,4 +79,5 @@ static inline void vec_push (vec* v, void* e) v->ptr[v->size++] = e; } + #endif |