summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satInterA.c8
-rw-r--r--src/sat/bsat/satSolver.c36
-rw-r--r--src/sat/bsat/satSolver.h1
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;