Adding interpolant computation sat_solver2.

7 files changed, 48 insertions, 12 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 2d3e7588..4b8a88eb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -689,7 +689,7 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
 extern ABC_DLL void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose );
-extern ABC_DLL int                Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+extern ABC_DLL int                Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor );
 /*=== abcNames.c ====================================================*/
 extern ABC_DLL char *             Abc_ObjName( Abc_Obj_t * pNode );
 extern ABC_DLL char *             Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b45fde8f..74525e26 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6560,18 +6560,22 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
     int fReverse = 0;
     int fComb = 0;
+    int fXor = 0;
     int c;
-    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor );
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rxh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'r':
             fReverse ^= 1;
             break;
+        case 'x':
+            fXor ^= 1;
+            break;
         case 'c':
             fComb ^= 1;
             break;
@@ -6612,7 +6616,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        if ( !Abc_NtkCombinePos( pNtk, 0 ) )
+        if ( !Abc_NtkCombinePos( pNtk, 0, fXor ) )
         {
             Abc_Print( -1, "ORing the POs has failed.\n" );
             return 1;
@@ -6626,9 +6630,10 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: orpos [-rh]\n" );
+    Abc_Print( -2, "usage: orpos [-rxh]\n" );
     Abc_Print( -2, "\t        creates single-output miter by ORing the POs of the current network\n" );
     Abc_Print( -2, "\t-r    : performs the reverse transform (OR decomposition) [default = %s]\n", fReverse? "yes": "no" );
+    Abc_Print( -2, "\t-x    : toggles combining the PO using XOR [default = %s]\n", fXor? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -6689,7 +6694,7 @@ int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkCombinePos( pNtk, 1 ) )
+    if ( !Abc_NtkCombinePos( pNtk, 1, 0 ) )
     {
         Abc_Print( -1, "ANDing the POs has failed.\n" );
         return 1;
@@ -22100,7 +22105,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         {
             Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk );
             Abc_Print( 0, "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) );
-            if ( !Abc_NtkCombinePos( pNtkNew, 0 ) )
+            if ( !Abc_NtkCombinePos( pNtkNew, 0, 0 ) )
             {
                 Abc_NtkDelete( pNtkNew );
                 Abc_Print( -1, "ORing outputs has failed.\n" );
@@ -32953,7 +32958,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Gia_Man_t * pTemp = NULL;
+    Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int nFrames = 3;
     int fSwitch = 0;
@@ -32973,6 +32978,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames );
 //    extern void Gia_ManMuxProfiling( Gia_Man_t * p );
 //    extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia );
+    extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
@@ -33044,6 +33050,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManMuxProfiling( pAbc->pGia );
 //    pTemp = Mig_ManTest( pAbc->pGia );
 //    Abc_FrameUpdateGia( pAbc, pTemp );
+    pTemp = Gia_ManInterTest( pAbc->pGia );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 8c5a4a83..747fe263 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1148,7 +1148,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
+int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor )
 {
     Abc_Obj_t * pNode, * pMiter;
     int i;
@@ -1165,6 +1165,8 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
     Abc_NtkForEachPo( pNtk, pNode, i )
         if ( fAnd )
             pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+        else if ( fXor )
+            pMiter = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
         else
             pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
     // remove the POs and their names
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 7d9973b1..25d1d113 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -362,7 +362,6 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
 ***********************************************************************/
 void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
-    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
     extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
     extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr );
 
@@ -416,7 +415,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
         // get this part of the miter
         Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
         pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
-        Abc_NtkCombinePos( pMiterPart, 0 );
+        Abc_NtkCombinePos( pMiterPart, 0, 0 );
         // check the miter for being constant
         RetValue = Abc_NtkMiterIsConstant( pMiterPart );
         if ( RetValue == 0 )
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;