Integrating Satoko into pdr.

9 files changed, 68 insertions, 42 deletions

diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index 016830c3..e0f1641c 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -86,7 +86,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
         sat_solver_setnvars( pSat, iVarNew + 1 );
         if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
         {
-            int Lit = toLitCond( iVarNew, 1 );
+            int Lit = Abc_Var2Lit( iVarNew, 1 );
             int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
             assert( RetValue == 1 );
             (void) RetValue;
@@ -136,11 +136,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
             for ( i = iClaBeg; i < iClaEnd; i++ )
             {
                 Vec_IntClear( vLits );
-                Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+                Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
                 for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
                 {
-                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, 3 );
-                    Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, 3 );
+                    Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
                 }
                 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
                 assert( RetValue );
@@ -154,11 +154,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
             if ( 2 - !Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) == (Pol & ~PolPres) ) // taking opposite literal
             {
                 Vec_IntClear( vLits );
-                Vec_IntPush( vLits, toLitCond( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
+                Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
                 for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
                 {
-                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
-                    Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
+                    Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
                 }
                 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
                 assert( RetValue );
@@ -187,7 +187,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
         sat_solver_setnvars( pSat, iVarNew + 1 );
         if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
         {
-            int Lit = toLitCond( iVarNew, 1 );
+            int Lit = Abc_Var2Lit( iVarNew, 1 );
             int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
             assert( RetValue == 1 );
             (void) RetValue;
@@ -213,11 +213,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
     for ( i = iClaBeg; i < iClaEnd; i++ )
     {
         Vec_IntClear( vLits );
-        Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+        Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
         for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
         {
-            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, Pol );
-            Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, Pol );
+            Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
         }
         RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
         assert( RetValue );
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 60454752..7e5218d0 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -107,13 +107,13 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     assert( Vec_IntSize(vLits) < pCube->nLits );
     // if the cube overlaps with init, add any literal
     Vec_IntForEachEntry( vLits, Entry, i )
-        if ( lit_sign(Entry) == 0 ) // positive literal
+        if ( Abc_LitIsCompl(Entry) == 0 ) // positive literal
             break;
     if ( i == Vec_IntSize(vLits) ) // only negative literals
     {
         // add the first positive literal
         for ( i = 0; i < pCube->nLits; i++ )
-            if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
+            if ( Abc_LitIsCompl(pCube->Lits[i]) == 0 ) // positive literal
             {
                 Vec_IntPush( vLits, pCube->Lits[i] );
                 break;
@@ -524,6 +524,7 @@ static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_
 ***********************************************************************/
 int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
 {
+#if 0
     int fUseMinAss = 0;
     sat_solver * pSat = Pdr_ManFetchSolver( p, k );
     int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
@@ -661,6 +662,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
     *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
     assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
     Order = 0;
+#endif
     return 0;
 }
 
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 7bb3319d..186791b2 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -896,7 +896,7 @@ int IPdr_ManCheckCubeReduce( Pdr_Man_t * p, Vec_Ptr_t * vClauses, Pdr_Set_t * pC
 
     if ( pCube == NULL ) // solve the property
     {
-        Lit = toLit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
         assert( RetValue == 1 );
 
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 2a8ab023..639276db 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -28,11 +28,35 @@
 #include "aig/saig/saig.h"
 #include "misc/vec/vecWec.h"
 #include "sat/cnf/cnf.h"
-#include "sat/bsat/satSolver.h"
 #include "pdr.h" 
 #include "misc/hash/hashInt.h"
 #include "aig/gia/giaAig.h"
 
+//#define PDR_USE_SATOKO 1
+
+#ifndef PDR_USE_SATOKO
+    #include "sat/bsat/satSolver.h"
+#else
+    #include "sat/satoko/satoko.h"
+    #include "sat/satoko/solver.h"
+    #define l_Undef  0
+    #define l_True   1
+    #define l_False -1
+    #define sat_solver                       satoko_t
+    #define sat_solver_new                   satoko_create
+    #define sat_solver_delete                satoko_destroy
+    #define zsat_solver_new_seed(s)          satoko_create()
+    #define zsat_solver_restart_seed(s,a)    satoko_reset(s)
+    #define sat_solver_nvars                 solver_varnum
+    #define sat_solver_setnvars              satoko_setnvars
+    #define sat_solver_addclause(s,b,e)      satoko_add_clause(s,b,e-b)
+    #define sat_solver_final                 satoko_final_conflict
+    #define sat_solver_solve(s,b,e,c,x,y,z)  satoko_solve_assumptions_limit(s,b,e-b,(int)c)
+    #define sat_solver_var_value             solver_read_cex_varvalue
+    #define sat_solver_set_runtime_limit     solver_set_runtime_limit
+    #define sat_solver_compress(s)             
+#endif
+
 ABC_NAMESPACE_HEADER_START
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index cb51e51e..7686ec03 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -421,12 +421,12 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
         {
             Lit = pObl->pState->Lits[i];
-            if ( lit_sign(Lit) )
+            if ( Abc_LitIsCompl(Lit) )
                 continue;
-            if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
+            if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
                 continue;
-            assert( lit_var(Lit) < pCex->nPis );
-            Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+            assert( Abc_Lit2Var(Lit) < pCex->nPis );
+            Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
         }
     assert( f == nFrames );
     if ( !Saig_ManVerifyCex(p->pAig, pCex) )
@@ -470,9 +470,9 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
         {
             Lit = pObl->pState->Lits[i]; 
-            if ( lit_var(Lit) < nPis ) // PI literal
+            if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
                 continue;
-            Flop = lit_var(Lit) - nPis;
+            Flop = Abc_Lit2Var(Lit) - nPis;
             if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
                 continue;
             Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
@@ -502,13 +502,13 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
             for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
             {
                 Lit = pObl->pState->Lits[i];
-                if ( lit_sign(Lit) )
+                if ( Abc_LitIsCompl(Lit) )
                     continue;
-                if ( lit_var(Lit) < nPis ) // PI literal
-                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+                if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
+                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
                 else
                 {
-                    int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
+                    int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
                     assert( iPPI < pCex->nPis );
                     Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
                 }
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 3c1bbad0..b1a5b66c 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -120,11 +120,11 @@ Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
     Vec_IntClear( p->vLits );
     for ( i = 0; i < nArray; i++ )
     {
-        RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
+        RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
         if ( RegId == -1 )
             continue;
         assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
-        Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
+        Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
     }
     assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
     return p->vLits;
@@ -153,12 +153,12 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
         if ( pCube->Lits[i] == -1 )
             continue;
         if ( fNext )
-            pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
+            pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
         else
-            pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
-        iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
+            pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
+        iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
         iVarMax = Abc_MaxInt( iVarMax, iVar );
-        Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
+        Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
     }
 //    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
     p->tCnf += Abc_Clock() - clk;
@@ -192,7 +192,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
         // skip timedout outputs
         if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
             continue;
-        Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
+        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
     }
@@ -300,7 +300,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     if ( pCube == NULL ) // solve the property
     {
         clk = Abc_Clock();
-        Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
@@ -316,7 +316,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
             // add the cube in terms of current state variables
             vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
             // add activation literal
-            Lit = toLit( Pdr_ManFreeVar(p, k) );
+            Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
             // add activation literal
             Vec_IntPush( vLits, Lit );
             RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
@@ -325,7 +325,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
             // create assumptions
             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
             // add activation literal
-            Vec_IntPush( vLits, lit_neg(Lit) );
+            Vec_IntPush( vLits, Abc_LitNot(Lit) );
         }
         else
             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
@@ -376,7 +376,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     if ( fLitUsed )
     {
         int RetValue;
-        Lit = lit_neg(Lit);
+        Lit = Abc_LitNot(Lit);
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
         sat_solver_compress( pSat );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index acbf70f5..5bc0d3d6 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
     {
         if ( Saig_ObjIsPi(pAig, pObj) )
         {
-            Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
+            Lit = Abc_Var2Lit( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
             Vec_IntPush( vPiLits, Lit );
             continue;
         }
         assert( Saig_ObjIsLo(pAig, pObj) );
         if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
             continue;
-        Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
+        Lit = Abc_Var2Lit( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
         Vec_IntPush( vRes, Lit );
     }
     if ( Vec_IntSize(vRes) == 0 )
diff --git a/src/proof/pdr/pdrTsim3.c b/src/proof/pdr/pdrTsim3.c
index ebd1a702..3e24a356 100644
--- a/src/proof/pdr/pdrTsim3.c
+++ b/src/proof/pdr/pdrTsim3.c
@@ -233,7 +233,7 @@ Abc_Print( 1, " in frame %d.\n", k );
 
     // read solver
     pSat = Pdr_ManFetchSolver( p->pMan, k );
-    LitAux = toLit( Pdr_ManFreeVar(p->pMan, k) );
+    LitAux = Abc_Var2Lit( Pdr_ManFreeVar(p->pMan, k), 0 );
     // add the clause (complemented cube) in terms of next state variables
     if ( pCube == NULL ) // the target is the property output
     {
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 986697ac..b2eaa2c7 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -234,7 +234,7 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
     {
         if ( p->Lits[i] == -1 )
             continue;
-        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+        pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
     }
     if ( vFlopCounts )
     {
@@ -351,7 +351,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
     {
         if ( p->Lits[i] == -1 )
             continue;
-        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+        pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
     }
     if ( vFlopCounts )
     {
@@ -465,7 +465,7 @@ int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
         assert( pCube->Lits[i] != -1 );
         if ( i == iRemove )
             continue;
-        if ( lit_sign( pCube->Lits[i] ) == 0 )
+        if ( Abc_LitIsCompl( pCube->Lits[i] ) == 0 )
             return 0;
     }
     return 1;