diff options
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/module.make | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 17 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 11 |
3 files changed, 28 insertions, 1 deletions
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index e54dc891..4e85bece 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -6,6 +6,7 @@ SRC += src/sat/bsat/satMem.c \ src/sat/bsat/satProof.c \ src/sat/bsat/satSolver.c \ src/sat/bsat/satSolver2.c \ + src/sat/bsat/satSolver2i.c \ src/sat/bsat/satStore.c \ src/sat/bsat/satTrace.c \ src/sat/bsat/satTruth.c \ diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 84d59f62..96656b5b 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -169,6 +169,8 @@ static inline void proof_chain_start( sat_solver2* s, clause* c ) { if ( !s->fProofLogging ) return; + if ( s->pInt2 ) + s->tempInter = Int2_ManChainStart( s->pInt2, c ); if ( s->pPrf2 ) Prf_ManChainStart( s->pPrf2, c ); if ( s->pPrf1 ) @@ -186,6 +188,11 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { if ( !s->fProofLogging ) return; + if ( s->pInt2 ) + { + clause* c = cls ? cls : var_unit_clause( s, Var ); + s->tempInter = Int2_ManChainResolve( s->pInt2, c, s->tempInter, var_is_partA(s,Var) ); + } if ( s->pPrf2 ) { clause* c = cls ? cls : var_unit_clause( s, Var ); @@ -204,6 +211,12 @@ static inline int proof_chain_stop( sat_solver2* s ) { if ( !s->fProofLogging ) return 0; + if ( s->pInt2 ) + { + int h = s->tempInter; + s->tempInter = -1; + return h; + } if ( s->pPrf2 ) Prf_ManChainStop( s->pPrf2 ); if ( s->pPrf1 ) @@ -410,7 +423,7 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, assert( proof_id ); c->lbd = sat_clause_compute_lbd( s, c ); assert( clause_id(c) == veci_size(&s->act_clas) ); - if ( s->pPrf1 ) + if ( s->pPrf1 || s->pInt2 ) veci_push(&s->claProofs, proof_id); // veci_push(&s->act_clas, (1<<10)); veci_push(&s->act_clas, 0); @@ -1141,6 +1154,7 @@ sat_solver2* sat_solver2_new(void) // proof-logging veci_new(&s->claProofs); // s->pPrf1 = Vec_SetAlloc( 20 ); + s->tempInter = -1; // initialize clause pointers s->hLearntLast = -1; // the last learnt clause @@ -1244,6 +1258,7 @@ void sat_solver2_delete(sat_solver2* s) // veci_delete(&s->proofs); Vec_SetFree( s->pPrf1 ); Prf_ManStop( s->pPrf2 ); + Int2_ManStop( s->pInt2 ); // delete arrays if (s->vi != 0){ diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index d7d16d73..41dfc680 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -42,6 +42,7 @@ ABC_NAMESPACE_HEADER_START struct sat_solver2_t; typedef struct sat_solver2_t sat_solver2; +typedef struct Int2_Man_t_ Int2_Man_t; extern sat_solver2* sat_solver2_new(void); extern void sat_solver2_delete(sat_solver2* s); @@ -72,6 +73,14 @@ extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ); extern void Sat_ProofCheck( sat_solver2 * s ); +// interpolation APIs +extern Int2_Man_t * Int2_ManStart( sat_solver2 * pSat, int * pGloVars, int nGloVars ); +extern void Int2_ManStop( Int2_Man_t * p ); +extern int Int2_ManChainStart( Int2_Man_t * p, clause * c ); +extern int Int2_ManChainResolve( Int2_Man_t * p, clause * c, int iLit, int varA ); +extern void * Int2_ManReadInterpolant( sat_solver2 * s ); + + //================================================================================================= // Solver representation: @@ -156,6 +165,8 @@ struct sat_solver2_t int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) Prf_Man_t * pPrf2; // another proof manager double dPrfMemory; // memory used by the proof-logger + Int2_Man_t * pInt2; // interpolation manager + int tempInter; // temporary storage for the interpolant // statistics stats_t stats; |