Adding interpolant computation sat_solver2.

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;