summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/aig/aig.h4
-rw-r--r--src/sat/aig/fraigCore.c2
-rw-r--r--src/sat/aig/rwrTruth.c6
-rw-r--r--src/sat/asat/added.c24
-rw-r--r--src/sat/asat/asat60525.zipbin0 -> 25597 bytes
-rw-r--r--src/sat/asat/jfront.c4
-rw-r--r--src/sat/asat/solver.c201
-rw-r--r--src/sat/asat/solver.h26
-rw-r--r--src/sat/asat/solver_vec.h30
-rw-r--r--src/sat/csat/csat_apis.c95
-rw-r--r--src/sat/csat/csat_apis.h5
-rw-r--r--src/sat/fraig/fraig.h42
-rw-r--r--src/sat/fraig/fraigApi.c4
-rw-r--r--src/sat/fraig/fraigCanon.c4
-rw-r--r--src/sat/fraig/fraigInt.h3
-rw-r--r--src/sat/fraig/fraigMan.c12
-rw-r--r--src/sat/msat/msat.h1
-rw-r--r--src/sat/msat/msatInt.h6
-rw-r--r--src/sat/msat/msatSolverApi.c35
19 files changed, 340 insertions, 164 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 5d2547ea..a0d63ce9 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -64,9 +64,11 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
//typedef int bool;
+#ifndef __cplusplus
#ifndef bool
#define bool int
#endif
+#endif
typedef struct Aig_Param_t_ Aig_Param_t;
typedef struct Aig_Man_t_ Aig_Man_t;
@@ -215,7 +217,7 @@ struct Aig_SimInfo_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
+static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index 525d4a14..03781180 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
// solve the miter
clk = clock();
pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
- status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit );
+ status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
index 92a39f0a..cb8d03e0 100644
--- a/src/sat/aig/rwrTruth.c
+++ b/src/sat/aig/rwrTruth.c
@@ -167,7 +167,7 @@ void Aig_TruthCount( Aig_Truth_t * p )
***********************************************************************/
static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
{
- return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size));
+ return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size));
}
/**Function*************************************************************
@@ -183,7 +183,7 @@ static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
***********************************************************************/
static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
{
- p[Start/5] |= (Part << (Start%32));
+ p[Start/5] |= (Part << (Start&31));
}
/**Function*************************************************************
@@ -254,7 +254,7 @@ DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int n
}
if ( nVars == 5 )
{
- unsigned * pWord = pTruth + Shift/32;
+ unsigned * pWord = pTruth + (Shift>>5);
assert( Shift % 32 == 0 );
if ( *pWord == 0 )
return Cudd_ReadLogicZero(dd);
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
new file mode 100644
index 00000000..b8361af1
--- /dev/null
+++ b/src/sat/asat/asat60525.zip
Binary files differ
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
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 9184cab9..353f6c4c 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -39,8 +39,7 @@ struct ABC_ManagerStruct_t
Extra_MmFlex_t * pMmNames; // memory manager for signal names
// solving parameters
int mode; // 0 = resource-aware integration; 1 = brute-force SAT
- int nConfLimit; // time limit for pure SAT solving
- int nImpLimit; // time limit for pure SAT solving
+ Prove_Params_t Params; // integrated CEC parameters
// information about the target
int nog; // the numbers of gates in the target
Vec_Ptr_t * vNodes; // the gates in the target
@@ -87,9 +86,11 @@ ABC_Manager ABC_InitManager()
mng->pMmNames = Extra_MmFlexStart();
mng->vNodes = Vec_PtrAlloc( 100 );
mng->vValues = Vec_IntAlloc( 100 );
- mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT;
- mng->nImpLimit = ABC_DEFAULT_IMP_LIMIT;
mng->mode = 0; // set "resource-aware integration" as the default mode
+ // set default parameters for CEC
+ Prove_ParamsSetDefault( &mng->Params );
+ // set infinite resource limit for the final mitering
+ mng->Params.nMiteringLimitLast = ABC_INFINITY;
return mng;
}
@@ -334,7 +335,7 @@ int ABC_Check_Integrity( ABC_Manager mng )
continue;
if ( Abc_ObjFanoutNum(pObj) == 0 )
{
- printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
+// printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
return 0;
}
}
@@ -361,7 +362,7 @@ int ABC_Check_Integrity( ABC_Manager mng )
***********************************************************************/
void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
{
- printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
+// printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -377,7 +378,7 @@ void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
***********************************************************************/
void ABC_SetLearnLimit( ABC_Manager mng, int num )
{
- printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+// printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -393,7 +394,7 @@ void ABC_SetLearnLimit( ABC_Manager mng, int num )
***********************************************************************/
void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
{
- printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+// printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -409,7 +410,7 @@ void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
***********************************************************************/
void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
{
- mng->nConfLimit = num;
+ mng->Params.nMiteringLimitLast = num;
}
/**Function*************************************************************
@@ -425,7 +426,70 @@ void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
***********************************************************************/
void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num )
{
- mng->nImpLimit = num;
+// printf( "ABC_SetSolveImplicationLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num )
+{
+ mng->Params.nTotalBacktrackLimit = num;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num )
+{
+ mng->Params.nTotalInspectLimit = num;
+}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng )
+{
+ return mng->Params.nTotalBacktracksMade;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+uint64 ABC_GetTotalInspectsMade( ABC_Manager mng )
+{
+ return mng->Params.nTotalInspectsMade;
}
/**Function*************************************************************
@@ -539,7 +603,7 @@ void ABC_AnalyzeTargets( ABC_Manager mng )
***********************************************************************/
enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
{
- Prove_Params_t Params, * pParams = &Params;
+ Prove_Params_t * pParams = &mng->Params;
int RetValue, i;
// check if the target network is available
@@ -548,16 +612,9 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
// try to prove the miter using a number of techniques
if ( mng->mode )
- RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0, 0 );
+ RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
else
- {
- // set default parameters for CEC
- Prove_ParamsSetDefault( pParams );
- // set infinite resource limit for the final mitering
- pParams->nMiteringLimitLast = ABC_INFINITY;
- // call the checker
RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams );
- }
// analyze the result
mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index d2fa770e..b80eddbf 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -182,6 +182,11 @@ extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num
extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
extern void ABC_EnableDump(ABC_Manager mng, char* dump_file);
+extern void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num );
+extern void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num );
+extern uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng );
+extern uint64 ABC_GetTotalInspectsMade( ABC_Manager mng );
+
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index d6215465..84363efe 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -27,6 +27,8 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
+#include "solver.h"
+
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
@@ -49,8 +51,6 @@ struct Fraig_ParamsStruct_t_
int nPatsDyna; // the number of words of dynamic simulation info
int nBTLimit; // the max number of backtracks to perform
int nSeconds; // the timeout for the final proof
- int nConfLimit;
- int nImpLimit;
int fFuncRed; // performs only one level hashing
int fFeedBack; // enables solver feedback
int fDist1Pats; // enables distance-1 patterns
@@ -60,31 +60,39 @@ struct Fraig_ParamsStruct_t_
int fVerbose; // the verbosiness flag
int fVerboseP; // the verbosiness flag (for proof reporting)
int fInternal; // is set to 1 for internal fraig calls
+ int nConfLimit; // the limit on the number of conflicts
+ sint64 nInspLimit; // the limit on the number of inspections
};
struct Prove_ParamsStruct_t_
{
// general parameters
- int fUseFraiging; // enables fraiging
- int fUseRewriting; // enables rewriting
- int fUseBdds; // enables BDD construction when other methods fail
- int fVerbose; // prints verbose stats
+ int fUseFraiging; // enables fraiging
+ int fUseRewriting; // enables rewriting
+ int fUseBdds; // enables BDD construction when other methods fail
+ int fVerbose; // prints verbose stats
// iterations
- int nItersMax; // the number of iterations
+ int nItersMax; // the number of iterations
// mitering
- int nMiteringLimitStart; // starting mitering limit
- float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ int nMiteringLimitStart; // starting mitering limit
+ float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// rewriting
- int nRewritingLimitStart; // the number of rewriting iterations
- float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ int nRewritingLimitStart; // the number of rewriting iterations
+ float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// fraiging
- int nFraigingLimitStart; // starting backtrack(conflict) limit
- float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ int nFraigingLimitStart; // starting backtrack(conflict) limit
+ float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// last-gasp BDD construction
- int nBddSizeLimit; // the number of BDD nodes when construction is aborted
- int fBddReorder; // enables dynamic BDD variable reordering
+ int nBddSizeLimit; // the number of BDD nodes when construction is aborted
+ int fBddReorder; // enables dynamic BDD variable reordering
// last-gasp mitering
- int nMiteringLimitLast; // final mitering limit
+ int nMiteringLimitLast; // final mitering limit
+ // global SAT solver limits
+ sint64 nTotalBacktrackLimit; // global limit on the number of backtracks
+ sint64 nTotalInspectLimit; // global limit on the number of clause inspects
+ // global resources applied
+ sint64 nTotalBacktracksMade; // the total number of backtracks made
+ sint64 nTotalInspectsMade; // the total number of inspects made
};
////////////////////////////////////////////////////////////////////////
@@ -137,6 +145,8 @@ extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
extern int Fraig_ManReadSatFails( Fraig_Man_t * p );
+extern int Fraig_ManReadConflicts( Fraig_Man_t * p );
+extern int Fraig_ManReadInspects( Fraig_Man_t * p );
extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );
extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index b4bdbcab..79a7c224 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -66,6 +66,10 @@ int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) {
int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; }
// returns the number of times FRAIG package timed out
int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFailsReal; }
+// returns the number of conflicts in the SAT solver
+int Fraig_ManReadConflicts( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; }
+// returns the number of inspections in the SAT solver
+int Fraig_ManReadInspects( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadInspects(p->pSat) : 0; }
/**Function*************************************************************
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 4ebb9a9f..89bc924f 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -49,6 +49,7 @@
Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 )
{
Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
+ int fUseSatCheck;
// int RetValue;
// check for trivial cases
@@ -167,7 +168,8 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
// there is another node which looks the same according to simulation
// use SAT to resolve the ambiguity
- if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
+ fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit);
+ if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
{
// set the node to be equivalent with this node
// to prevent loops, only set if the old node is not in the TFI of the new node
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 8e016331..9c6e0d47 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -66,7 +66,7 @@
// the bit masks
#define FRAIG_MASK(n) ((~((unsigned)0)) >> (32-(n)))
#define FRAIG_FULL (~((unsigned)0))
-#define FRAIG_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0))
+#define FRAIG_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
// maximum/minimum operators
#define FRAIG_MIN(a,b) (((a) < (b))? (a) : (b))
@@ -152,6 +152,7 @@ struct Fraig_ManStruct_t_
int fTryProve; // tries to solve the final miter
int fVerbose; // the verbosiness flag
int fVerboseP; // the verbosiness flag
+ sint64 nInspLimit; // the inspection limit
int nTravIds; // the traversal counter
int nTravIds2; // the traversal counter
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 3268ac3a..ffb51a07 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -42,10 +42,12 @@ int timeAssign;
***********************************************************************/
void Prove_ParamsSetDefault( Prove_Params_t * pParams )
{
+ // clean the parameter structure
+ memset( pParams, 0, sizeof(Prove_Params_t) );
// general parameters
pParams->fUseFraiging = 1; // enables fraiging
pParams->fUseRewriting = 1; // enables rewriting
- pParams->fUseBdds = 1; // enables BDD construction when other methods fail
+ pParams->fUseBdds = 0; // enables BDD construction when other methods fail
pParams->fVerbose = 0; // prints verbose stats
// iterations
pParams->nItersMax = 6; // the number of iterations
@@ -63,6 +65,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
pParams->fBddReorder = 1; // enables dynamic BDD variable reordering
// last-gasp mitering
pParams->nMiteringLimitLast = 1000000; // final mitering limit
+ // global SAT solver limits
+ pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks
+ pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects
}
/**Function*************************************************************
@@ -92,6 +97,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbose flag for reporting the proof
pParams->fInternal = 0; // the flag indicates the internal run
+ pParams->nConfLimit = 0; // the limit on the number of conflicts
+ pParams->nInspLimit = 0; // the limit on the number of inspections
}
/**Function*************************************************************
@@ -121,6 +128,8 @@ void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbose flag for reporting the proof
pParams->fInternal = 0; // the flag indicates the internal run
+ pParams->nConfLimit = 0; // the limit on the number of conflicts
+ pParams->nInspLimit = 0; // the limit on the number of inspections
}
/**Function*************************************************************
@@ -176,6 +185,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice)
p->fVerbose = pParams->fVerbose; // disable verbose output
p->fVerboseP = pParams->fVerboseP; // disable verbose output
+ p->nInspLimit = pParams->nInspLimit; // the limit on the number of inspections
// start memory managers
p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 94416a5d..5f8603a7 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -97,6 +97,7 @@ extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int * Msat_SolverReadModelArray( Msat_Solver_t * p );
extern unsigned Msat_SolverReadTruth( Msat_Solver_t * p );
extern int Msat_SolverReadBackTracks( Msat_Solver_t * p );
+extern int Msat_SolverReadInspects( Msat_Solver_t * p );
extern void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
extern void Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
extern void Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 3dfe2109..03e7b873 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -56,10 +56,10 @@ typedef long long int64;
#define ALLOC(type, num) \
((type *) malloc(sizeof(type) * (num)))
#define REALLOC(type, obj, num) \
- (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
- ((type *) malloc(sizeof(type) * (num)))
+ ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+ ((type *) malloc(sizeof(type) * (num))))
#define FREE(obj) \
- ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+ ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
// By default, custom memory management is used
// which guarantees constant time allocation/deallocation
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 4a721487..e3d85774 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -41,26 +41,27 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
SeeAlso []
***********************************************************************/
-int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
-int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
-int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;}
+int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
+int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
+int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc; }
int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
-int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
-Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
+int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
+Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
-Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
-Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
-int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
-int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
-int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return p->nBackTracks; }
-Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
-int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
-int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
+Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
+int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
+int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
+int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; }
+int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; }
+Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
+int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
+int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; }
-void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
-void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
-void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
-void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
+void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
+void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
+void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
+void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-20 19:27:03 +0000