diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-19 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-19 08:01:00 -0700 |
commit | de978ced7b754706efaf18ae588e18eb05624faf (patch) | |
tree | 0180f1b83fe9a3492a754a91e1aa152024affc54 /src/sat/bsat | |
parent | 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 (diff) | |
download | abc-de978ced7b754706efaf18ae588e18eb05624faf.tar.gz abc-de978ced7b754706efaf18ae588e18eb05624faf.tar.bz2 abc-de978ced7b754706efaf18ae588e18eb05624faf.zip |
Version abc80719
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/satInterA.c | 8 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 36 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 |
3 files changed, 32 insertions, 13 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 5837e68f..82f4e034 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -809,8 +809,12 @@ int Inta_ManProcessRoots( Inta_Man_t * p ) if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); +// printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 0179796c..12529ca7 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1061,7 +1061,8 @@ bool 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; + if (begin == end) + return false; //printlits(begin,end); printf("\n"); // insertion sort @@ -1076,6 +1077,16 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) sat_solver_setnvars(s,maxvar+1); // sat_solver_setnvars(s, lit_var(*(end-1))+1 ); + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, begin, end ); + assert( RetValue ); + } + /////////////////////////////////// + //printlits(begin,end); printf("\n"); values = s->assigns; @@ -1095,16 +1106,6 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) if (j == begin) // empty clause return false; - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, begin, j ); - assert( RetValue ); - } - /////////////////////////////////// - if (j - begin == 1) // unit clause return enqueue(s,*begin,(clause*)0); @@ -1164,6 +1165,19 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin lbool* values = s->assigns; lit* i; + //////////////////////////////////////////////// + if ( s->fSolved ) + { + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); + assert( RetValue ); + } + return l_False; + } + //////////////////////////////////////////////// + // set the external limits s->nCalls++; s->nRestarts = 0; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 9ffc2b75..86e7a966 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -182,6 +182,7 @@ struct sat_solver_t // clause store void * pStore; + int fSolved; // trace recording FILE * pFile; |