Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages

src/aig/gia/giaSatoko.c

@@ -21,7 +21,6 @@
 #include "gia.h"
 #include "sat/cnf/cnf.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -133,7 +132,7 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
     if ( pSat )
     {
         status = satoko_solve( pSat );
-        Cost = (unsigned)pSat->stats.n_conflicts;
+        Cost = satoko_stats(pSat)->n_conflicts;
         satoko_destroy( pSat );
     }
     else 

src/aig/gia/giaSupp.c

@@ -20,7 +20,6 @@
 
 #include "gia.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 
 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
@@ -389,7 +388,7 @@ Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia )
     p->vFanins   = Vec_PtrAlloc( 100 );
     p->vSatVars  = Vec_IntAlloc( 100 );
     p->iPattern  = 1;
-    p->pSat->opts.learnt_ratio = 0; // prevent garbage collection
+    satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection
     return p;
 }
 void Gia_Man2SuppStop( Gia_Man2Min_t * p )
@@ -725,7 +724,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p )
 //        assert( iTemp == -1 );
     Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 );
     Vec_IntClear( p->vSatVars );
-    assert( solver_varnum(p->pSat) == 0 );
+    assert( satoko_varnum(p->pSat) == 0 );
     iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 );
     iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 );
     satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) );
@@ -739,7 +738,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p )
         assert( Gia_Min2ManSimulate(p) == 1 );
         for ( n = 0; n < 2; n++ )
             Vec_IntForEachEntry( p->vCis[n], iTemp, i )
-                Gia_Min2SimSetInputBit( p, iTemp, var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == LIT_TRUE, p->iPattern );
+                Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern );
         //assert( Gia_Min2ManSimulate(p) == 0 );
         p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1;
         p->nSatSat++;

src/proof/cec/cecSat.c

@@ -21,7 +21,6 @@
 #include "aig/gia/gia.h"
 #include "misc/util/utilTruth.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 #include "cec.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -660,6 +659,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
 {
     Cec2_Man_t * p;
     Gia_Obj_t * pObj; int i;
+    satoko_opts_t Pars;
     //assert( Gia_ManRegNum(pAig) == 0 );
     p = ABC_CALLOC( Cec2_Man_t, 1 );
     memset( p, 0, sizeof(Cec2_Man_t) );
@@ -675,6 +675,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
     Gia_ManHashAlloc( p->pNew );
     Vec_IntFill( &p->pNew->vCopies, Gia_ManObjNum(p->pNew), -1 );
     // SAT solving
+    memset( &Pars, 0, sizeof(satoko_opts_t) );
     p->pSat         = satoko_create();
     p->vFrontier    = Vec_PtrAlloc( 1000 );
     p->vFanins      = Vec_PtrAlloc( 100 );
@@ -682,7 +683,8 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
     p->vSatVars     = Vec_IntAlloc( 100 );
     p->vObjSatPairs = Vec_IntAlloc( 100 );
     p->vCexTriples  = Vec_IntAlloc( 100 );
-    p->pSat->opts.conf_limit = pPars->nConfLimit;
+    Pars.conf_limit = pPars->nConfLimit;
+    satoko_configure(p->pSat, &Pars);
     // remember pointer to the solver in the AIG manager
     pAig->pData     = p->pSat;
     return p;
@@ -742,7 +744,7 @@ int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat )
         return pObj->fMark1;
     Gia_ObjSetTravIdCurrentId(p, iObj);
     if ( Gia_ObjIsCi(pObj) )
-        return pObj->fMark1 = var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == LIT_TRUE;
+        return pObj->fMark1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == SATOKO_LIT_TRUE;
     assert( Gia_ObjIsAnd(pObj) );
     Value0 = Cec2_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
     Value1 = Cec2_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
@@ -750,8 +752,8 @@ int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat )
 }
 void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat )
 {
-//    int val0 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == LIT_TRUE;
-//    int val1 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == LIT_TRUE;
+//    int val0 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == SATOKO_LIT_TRUE;
+//    int val1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == SATOKO_LIT_TRUE;
     int Value0, Value1;
     Gia_ManIncrementTravId( p );
     Value0 = Cec2_ManVerify_rec( p, iObj0, pSat );
@@ -805,7 +807,7 @@ int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase )
     if (iObj1 < iObj0) 
         iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
     assert( iObj0 < iObj1 );
-    assert( p->pPars->fUseCones || solver_varnum(p->pSat) == 0 );
+    assert( p->pPars->fUseCones || satoko_varnum(p->pSat) == 0 );
     if ( !iObj0 && Cec2_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
         Cec2_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), satoko_add_variable(p->pSat, 0) );
     iVar0 = Cec2_ObjGetCnfVar( p, iObj0 );
@@ -859,7 +861,7 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
         p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1;
         assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
         Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i )
-            Cec2_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE );
+            Cec2_ObjSimSetInputBit( p->pAig, IdAig, satoko_var_polarity(p->pSat, IdSat) == SATOKO_LIT_TRUE );
         p->timeSatSat += Abc_Clock() - clk;
         RetValue = 0;
     }
@@ -884,7 +886,7 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
     clk = Abc_Clock();
     satoko_rollback( p->pSat );
     p->timeExtra += Abc_Clock() - clk;
-    p->pSat->stats.n_conflicts = 0;
+    satoko_stats(p->pSat)->n_conflicts = 0;
     return RetValue;
 }
 void Cec2_ManPrintStats( Gia_Man_t * p, Cec2_Par_t * pPars, Cec2_Man_t * pMan )

src/proof/pdr/pdrInt.h

@@ -38,7 +38,6 @@
     #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
@@ -47,13 +46,13 @@
     #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_nvars                 satoko_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_var_value             satoko_read_cex_varvalue
+    #define sat_solver_set_runtime_limit     satoko_set_runtime_limit
     #define sat_solver_compress(s)             
 #endif
 

src/sat/bmc/bmcBmc.c

@@ -22,7 +22,6 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 #include "bmc.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -190,7 +189,7 @@ int * Sat2_SolverGetModel( satoko_t * p, int * pVars, int nVars )
     int i;
     pModel = ABC_CALLOC( int, nVars+1 );
     for ( i = 0; i < nVars; i++ )
-        pModel[i] = solver_read_cex_varvalue(p, pVars[i]);
+        pModel[i] = satoko_read_cex_varvalue(p, pVars[i]);
     return pModel;    
 }
  
@@ -320,8 +319,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                 printf( "Solved %2d outputs of frame %3d.  ", 
                     Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                 printf( "Conf =%8.0f. Imp =%11.0f. ", 
-                    (double)(pSat ? pSat->stats.conflicts    : solver_conflictnum(pSat2)), 
-                    (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2).n_propagations) );
+                    (double)(pSat ? pSat->stats.conflicts    : satoko_conflictnum(pSat2)), 
+                    (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2)->n_propagations) );
                 ABC_PRT( "T", Abc_Clock() - clkPart );
                 clkPart = Abc_Clock();
                 fflush( stdout );

src/sat/bmc/bmcBmc2.c

@@ -21,7 +21,6 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 #include "proof/ssw/ssw.h"
 #include "bmc.h"
 
@@ -690,7 +689,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
             iVarNum = Saig_BmcSatNum( p, pObjFrm );
             if ( iVarNum == 0 )
                 continue;
-            if ( p->pSat2 ? solver_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
+            if ( p->pSat2 ? satoko_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
                 Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
         }
     }
@@ -729,7 +728,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
     {
         if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
             continue;
-        if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll )
+        if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
             return l_Undef;
         VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
         Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
@@ -838,7 +837,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     if ( nTimeOut )
     {
         if ( p->pSat2 )
-            solver_set_runtime_limit( p->pSat2, nTimeToStop );
+            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
         else
             sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     }
@@ -867,7 +866,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         {
             printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
                 Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, 
-                p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2) );   
+                p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) );   
             printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
             printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
             printf( "\n" );
@@ -922,7 +921,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         {
             if ( p->iFrameLast >= p->nFramesMax )
                 printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-            else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll )
+            else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
                 printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
             else if ( nTimeOut && Abc_Clock() > nTimeToStop )
                 printf( "Reached timeout (%d seconds).\n", nTimeOut );

src/sat/bmc/bmcBmc3.c

@@ -22,7 +22,6 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/vec/vecWec.h"
 #include "bmc.h"
@@ -798,9 +797,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
             p->pSat ? p->pSat->nLearntDelta     : 0, 
             p->pSat ? p->pSat->nLearntRatio     : 0, 
             p->pSat ? p->pSat->nDBreduces       : 0, 
-            p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2), 
+            p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2), 
             nUsedVars, 
-            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2)) );
+            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2)) );
         Abc_Print( 1, "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  UniProps = %d.\n", 
             p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
     }
@@ -1382,7 +1381,7 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
             int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
             if ( p->pSat2 )
             {
-                if ( iLit != ~0 && solver_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
+                if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
                     Abc_InfoSetBit( pCex->pData, iBit + k );
             }
             else
@@ -1465,8 +1464,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     }
     else
     {
-        p->pSat2->RunId        = p->pPars->RunId;
-        p->pSat2->pFuncStop    = p->pPars->pFuncStop;
+        satoko_set_runid(p->pSat2, p->pPars->RunId);
+        satoko_set_stop_func(p->pSat2, p->pPars->pFuncStop);
     }
     if ( pPars->fSolveAll && p->vCexes == NULL )
         p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
@@ -1483,7 +1482,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     if ( nTimeToStop )
     {
         if ( p->pSat2 )
-            solver_set_runtime_limit( p->pSat2, nTimeToStop );
+            satoko_set_runtime_limit( p->pSat2, nTimeToStop );
         else
             sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     }
@@ -1614,7 +1613,7 @@ clkOther += Abc_Clock() - clk2;
                 assert( p->pTime4Outs[i] > 0 );
                 clkOne = Abc_Clock();
                 if ( p->pSat2 )
-                    solver_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
+                    satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
                 else
                     sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
             }
@@ -1673,8 +1672,8 @@ nTimeSat += clkSatRun;
                     {
                         Abc_Print( 1, "%4d %s : ", f,  fUnfinished ? "-" : "+" );
                         Abc_Print( 1, "Var =%8.0f. ",  (double)p->nSatVars );
-                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : solver_clausenum(p->pSat2)) );
-                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) );
+                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : satoko_clausenum(p->pSat2)) );
+                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
 //                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
                         Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
 //                        ABC_PRT( "Time", Abc_Clock() - clk );
@@ -1721,7 +1720,7 @@ nTimeSat += clkSatRun;
                 if ( nTimeToStop )
                 {
                     if ( p->pSat2 )
-                        solver_set_runtime_limit( p->pSat2, nTimeToStop );
+                        satoko_set_runtime_limit( p->pSat2, nTimeToStop );
                     else
                         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
                 }
@@ -1738,7 +1737,7 @@ nTimeSat += clkSatRun;
                     Lit = Saig_ManBmcCreateCnf( p, pObj, f );
                     if ( p->pSat2 )
                     {
-                        if ( solver_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
+                        if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                             continue;
                     }
                     else
@@ -1781,7 +1780,7 @@ nTimeUndec += clkSatRun;
         }
         if ( pPars->fVerbose ) 
         {
-            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > 1 )
+            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 1 )
             {
                 fFirst = 0;
 //                Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@@ -1789,8 +1788,8 @@ nTimeUndec += clkSatRun;
             Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
             Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
 //            Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
-            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : solver_clausenum(p->pSat2)) );
-            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) );
+            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : satoko_clausenum(p->pSat2)) );
+            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
 //            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
             Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
             if ( pPars->fSolveAll )

src/sat/bmc/bmcBmcS.c

@@ -21,7 +21,6 @@
 #include "bmc.h"
 #include "sat/cnf/cnf.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 
 
 //#define ABC_USE_EXT_SOLVERS 1
@@ -41,8 +40,8 @@
     #define bmc_sat_solver_addclause           satoko_add_clause
     #define bmc_sat_solver_addvar(s)           satoko_add_variable(s, 0)
     #define bmc_sat_solver_solve               satoko_solve_assumptions
-    #define bmc_sat_solver_read_cex_varvalue   solver_read_cex_varvalue
-    #define bmc_sat_solver_setstop             solver_set_stop
+    #define bmc_sat_solver_read_cex_varvalue   satoko_read_cex_varvalue
+    #define bmc_sat_solver_setstop             satoko_set_stop
 #endif
 
 
@@ -546,7 +545,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd )
     if ( pNew == NULL )
         return NULL;
     clk = Abc_Clock();
-    pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
+    pCnf = (Cnf_Dat_t *) Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
     pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
     pMap[0] = 0;
     Gia_ManForEachObj1( pNew, pObj, i )
@@ -584,10 +583,10 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
         return;
     Abc_Print( 1, "%4d %s : ", f,   fUnfinished ? "-" : "+" );
 #ifndef ABC_USE_EXT_SOLVERS
-    Abc_Print( 1, "Var =%8.0f.  ",  (double)solver_varnum(p->pSats[0]) ); 
-    Abc_Print( 1, "Cla =%9.0f.  ",  (double)solver_clausenum(p->pSats[0]) );  
-    Abc_Print( 1, "Learn =%9.0f.  ",(double)solver_learntnum(p->pSats[0]) );  
-    Abc_Print( 1, "Conf =%9.0f.  ", (double)solver_conflictnum(p->pSats[0]) );  
+    Abc_Print( 1, "Var =%8.0f.  ",  (double)satoko_varnum(p->pSats[0]) ); 
+    Abc_Print( 1, "Cla =%9.0f.  ",  (double)satoko_clausenum(p->pSats[0]) );  
+    Abc_Print( 1, "Learn =%9.0f.  ",(double)satoko_learntnum(p->pSats[0]) );  
+    Abc_Print( 1, "Conf =%9.0f.  ", (double)satoko_conflictnum(p->pSats[0]) );  
 #else
     Abc_Print( 1, "Var =%8.0f.  ",  (double)p->nSatVars ); 
     Abc_Print( 1, "Cla =%9.0f.  ",  (double)nClauses );  

src/sat/bmc/bmcMesh.c

@@ -20,7 +20,6 @@
 
 #include "bmc.h"
 #include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -53,9 +52,9 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][
 ***********************************************************************/
 static inline int Bmc_MeshVarValue( satoko_t * p, int v )
 {
-//    int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
-//    return value == LIT_TRUE;
-    return var_polarity(p, v) == LIT_TRUE;
+//    int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v);
+//    return value == SATOKO_LIT_TRUE;
+    return satoko_var_polarity(p, v) == SATOKO_LIT_TRUE;
 }
 
 /**Function*************************************************************
@@ -360,7 +359,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
         }
         printf( "Satisfying solution found. " );
 /*
-        iVar = solver_varnum(pSat);
+        iVar = satoko_varnum(pSat);
         for ( i = 0; i < iVar; i++ )
             if ( Bmc_MeshVarValue(pSat, i) )
                 printf( "%d ", i );

src/sat/bmc/bmcMesh2.c

@@ -20,7 +20,6 @@
 
 #include "bmc.h"
 //#include "sat/satoko/satoko.h"
-//#include "sat/satoko/solver.h"
 #include "sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -56,8 +55,8 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][
 ***********************************************************************/
 static inline int Bmc_MeshVarValue2( sat_solver * p, int v )
 {
-//    int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
-//    return value == LIT_TRUE;
+//    int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v);
+//    return value == SATOKO_LIT_TRUE;
     return sat_solver_var_value( p, v );
 }
 
@@ -370,7 +369,7 @@ void Bmc_MeshTest2( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
         }
         printf( "Satisfying solution found. " );
 /*
-//        iVar = solver_varnum(pSat);
+//        iVar = satoko_varnum(pSat);
         iVar = sat_solver_nvars(pSat);
         for ( i = 0; i < iVar; i++ )
             if ( Bmc_MeshVarValue2(pSat, i) )

src/sat/satoko/satoko.h

@@ -25,6 +25,12 @@ enum {
     SATOKO_UNSAT = -1
 };
 
+enum {
+    SATOKO_LIT_FALSE = 1,
+    SATOKO_LIT_TRUE = 0,
+    SATOKO_VAR_UNASSING = 3
+};
+
 struct solver_t_;
 typedef struct solver_t_ satoko_t;
 
@@ -120,7 +126,20 @@ extern int satoko_final_conflict(satoko_t *, int **);
  *   file will not be a DIMACS. (value 1 will use 0 as ID).
  */
 extern void satoko_write_dimacs(satoko_t *, char *, int, int);
-extern satoko_stats_t satoko_stats(satoko_t *);
+extern satoko_stats_t * satoko_stats(satoko_t *);
+extern satoko_opts_t * satoko_options(satoko_t *);
+
+extern int satoko_varnum(satoko_t *);
+extern int satoko_clausenum(satoko_t *);
+extern int satoko_learntnum(satoko_t *);
+extern int satoko_conflictnum(satoko_t *);
+extern void satoko_set_stop(satoko_t *, int *);
+extern void satoko_set_stop_func(satoko_t *s, int (*fnct)(int));
+extern void satoko_set_runid(satoko_t *, int);
+extern int satoko_read_cex_varvalue(satoko_t *, int);
+extern abctime satoko_set_runtime_limit(satoko_t *, abctime);
+extern char satoko_var_polarity(satoko_t *, unsigned);
+
 
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__satoko_h */

src/sat/satoko/solver.c

@@ -43,8 +43,8 @@ static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level
         unsigned *lits = &(c->data[0].lit);
 
         assert(var_reason(s, var) != UNDEF);
-        if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
-            assert(lit_value(s, lits[1]) == LIT_TRUE);
+        if (c->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
+            assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE);
             stk_swap(unsigned, lits[0], lits[1]);
         }
 
@@ -117,7 +117,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
     watch_list_foreach_bin(s->watches, w, neg_lit) {
         unsigned imp_lit = w->blocker;
         if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp &&
-            lit_value(s, imp_lit) == LIT_TRUE) {
+            lit_value(s, imp_lit) == SATOKO_LIT_TRUE) {
             counter++;
             vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1));
         }
@@ -186,7 +186,7 @@ static inline unsigned solver_decide(solver_t *s)
 {
     unsigned next_var = UNDEF;
 
-    while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) {
+    while (next_var == UNDEF || var_value(s, next_var) != SATOKO_VAR_UNASSING) {
         if (heap_size(s->var_order) == 0) {
             next_var = UNDEF;
             return UNDEF;
@@ -195,14 +195,14 @@ static inline unsigned solver_decide(solver_t *s)
         if (solver_has_marks(s) && !var_mark(s, next_var))
             next_var = UNDEF;
     }
-    return var2lit(next_var, var_polarity(s, next_var));
+    return var2lit(next_var, satoko_var_polarity(s, next_var));
 }
 
 static inline void solver_new_decision(solver_t *s, unsigned lit)
 {
     if (solver_has_marks(s) && !var_mark(s, lit2var(lit)))
         return;
-    assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
+    assert(var_value(s, lit2var(lit)) == SATOKO_VAR_UNASSING);
     vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
     solver_enqueue(s, lit, UNDEF);
 }
@@ -270,8 +270,8 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
         clause = clause_fetch(s, cref);
         lits = &(clause->data[0].lit);
 
-        if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
-            assert(lit_value(s, lits[1]) == LIT_TRUE);
+        if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
+            assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE);
             stk_swap(unsigned, lits[0], lits[1] );
         }
 
@@ -522,7 +522,7 @@ void solver_cancel_until(solver_t *s, unsigned level)
         unsigned var = lit2var(vec_uint_at(s->trail, i));
 
         vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var));
-        vec_char_assign(s->assigns, var, VAR_UNASSING);
+        vec_char_assign(s->assigns, var, SATOKO_VAR_UNASSING);
         vec_uint_assign(s->reasons, var, UNDEF);
         if (!heap_in_heap(s->var_order, var))
             heap_insert(s->var_order, var);
@@ -550,9 +550,9 @@ unsigned solver_propagate(solver_t *s)
         watch_list_foreach_bin(s->watches, i, p) {
             if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
                 continue;
-            if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
+            if (var_value(s, lit2var(i->blocker)) == SATOKO_VAR_UNASSING)
                 solver_enqueue(s, i->blocker, i->cref);
-            else if (lit_value(s, i->blocker) == LIT_FALSE)
+            else if (lit_value(s, i->blocker) == SATOKO_LIT_FALSE)
                 return i->cref;
         }
 
@@ -567,7 +567,7 @@ unsigned solver_propagate(solver_t *s)
                 *j++ = *i++;
                 continue;
             }
-            if (lit_value(s, i->blocker) == LIT_TRUE) {
+            if (lit_value(s, i->blocker) == SATOKO_LIT_TRUE) {
                 *j++ = *i++;
                 continue;
             }
@@ -585,13 +585,13 @@ unsigned solver_propagate(solver_t *s)
             w.blocker = lits[0];
 
             /* If 0th watch is true, then clause is already satisfied. */
-            if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE)
+            if (lits[0] != i->blocker && lit_value(s, lits[0]) == SATOKO_LIT_TRUE)
                 *j++ = w;
             else {
                 /* Look for new watch */
                 unsigned k;
                 for (k = 2; k < clause->size; k++) {
-                    if (lit_value(s, lits[k]) != LIT_FALSE) {
+                    if (lit_value(s, lits[k]) != SATOKO_LIT_FALSE) {
                         lits[1] = lits[k];
                         lits[k] = neg_lit;
                         watch_list_push(vec_wl_at(s->watches, lit_compl(lits[1])), w, 0);
@@ -602,7 +602,7 @@ unsigned solver_propagate(solver_t *s)
                 *j++ = w;
 
                 /* Clause becomes unit under this assignment */
-                if (lit_value(s, lits[0]) == LIT_FALSE) {
+                if (lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
                     conf_cref = i->cref;
                     s->i_qhead = vec_uint_size(s->trail);
                     i++;
@@ -665,9 +665,9 @@ char solver_search(solver_t *s)
             next_lit = UNDEF;
             while (solver_dlevel(s) < vec_uint_size(s->assumptions)) {
                 unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s));
-                if (lit_value(s, lit) == LIT_TRUE) {
+                if (lit_value(s, lit) == SATOKO_LIT_TRUE) {
                     vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
-                } else if (lit_value(s, lit) == LIT_FALSE) {
+                } else if (lit_value(s, lit) == SATOKO_LIT_FALSE) {
                     solver_analyze_final(s, lit_compl(lit));
                     return SATOKO_UNSAT;
                 } else {

src/sat/satoko/solver.h

@@ -30,11 +30,7 @@
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-enum {
-    LIT_FALSE = 1,
-    LIT_TRUE = 0,
-    VAR_UNASSING = 3
-};
+
 
 #define UNDEF 0xFFFFFFFF
 
@@ -145,11 +141,6 @@ static inline char var_value(solver_t *s, unsigned var)
     return vec_char_at(s->assigns, var);
 }
 
-static inline char var_polarity(solver_t *s, unsigned var)
-{
-    return vec_char_at(s->polarity, var);
-}
-
 static inline unsigned var_dlevel(solver_t *s, unsigned var)
 {
     return vec_uint_at(s->levels, var);
@@ -226,45 +217,15 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
     return SATOKO_OK;
 }
 
-static inline int solver_varnum(solver_t *s)
-{
-    return vec_char_size(s->assigns);
-}
-static inline int solver_clausenum(solver_t *s)
-{
-    return vec_uint_size(s->originals);
-}
-static inline int solver_learntnum(solver_t *s)
-{
-    return vec_uint_size(s->learnts);
-}
-static inline int solver_conflictnum(solver_t *s)
-{
-    return satoko_stats(s).n_conflicts;
-}
-
-static inline int solver_has_marks(solver_t *s)
+static inline int solver_has_marks(satoko_t *s)
 {
     return (int)(s->marks != NULL);
 }
-static inline int solver_stop(solver_t *s)
+
+static inline int solver_stop(satoko_t *s)
 {
     return s->pstop && *s->pstop;
 }
-static inline void solver_set_stop(solver_t *s, int * pstop)
-{
-    s->pstop = pstop;
-}
-static inline int solver_read_cex_varvalue(solver_t *s, int ivar)
-{
-    return var_polarity(s, ivar) == LIT_TRUE;
-}
-static abctime solver_set_runtime_limit(solver_t* s, abctime Limit)
-{
-    abctime nRuntimeLimit = s->nRuntimeLimit;
-    s->nRuntimeLimit = Limit;
-    return nRuntimeLimit;
-}
 
 //===------------------------------------------------------------------------===
 // Inline clause functions

src/sat/satoko/solver_api.c

@@ -27,7 +27,7 @@ static inline void solver_rebuild_order(solver_t *s)
     vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns));
 
     for (var = 0; var < vec_char_size(s->assigns); var++)
-        if (var_value(s, var) == VAR_UNASSING)
+        if (var_value(s, var) == SATOKO_VAR_UNASSING)
             vec_uint_push_back(vars, var);
     heap_build(s->var_order, vars);
     vec_uint_free(vars);
@@ -38,7 +38,7 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
     unsigned i;
     unsigned *lits = &(clause->data[0].lit);
     for (i = 0; i < clause->size; i++)
-        if (lit_value(s, lits[i]) == LIT_TRUE)
+        if (lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
             return SATOKO_OK;
     return SATOKO_ERR;
 }
@@ -226,7 +226,7 @@ int satoko_simplify(solver_t * s)
 void satoko_setnvars(solver_t *s, int nvars)
 {
     int i;
-    for (i = solver_varnum(s); i < nvars; i++)
+    for (i = satoko_varnum(s); i < nvars; i++)
         satoko_add_variable(s, 0);
 }
 
@@ -237,7 +237,7 @@ int satoko_add_variable(solver_t *s, char sign)
     vec_wl_push(s->watches);
     vec_act_push_back(s->activity, 0);
     vec_uint_push_back(s->levels, 0);
-    vec_char_push_back(s->assigns, VAR_UNASSING);
+    vec_char_push_back(s->assigns, SATOKO_VAR_UNASSING);
     vec_char_push_back(s->polarity, sign);
     vec_uint_push_back(s->reasons, UNDEF);
     vec_uint_push_back(s->stamps, 0);
@@ -258,15 +258,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
     qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare);
     max_var = lit2var(lits[size - 1]);
     while (max_var >= vec_act_size(s->activity))
-        satoko_add_variable(s, LIT_FALSE);
+        satoko_add_variable(s, SATOKO_LIT_FALSE);
 
     vec_uint_clear(s->temp_lits);
     j = 0;
     prev_lit = UNDEF;
     for (i = 0; i < (unsigned)size; i++) {
-        if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
+        if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
             return SATOKO_OK;
-        else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) {
+        else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == SATOKO_VAR_UNASSING) {
             prev_lit = lits[i];
             vec_uint_push_back(s->temp_lits, lits[i]);
         }
@@ -287,7 +287,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
 
 void satoko_assump_push(solver_t *s, int lit)
 {
-    assert(lit2var(lit) < solver_varnum(s));
+    assert(lit2var(lit) < satoko_varnum(s));
     // printf("[Satoko] Push assumption: %d\n", lit);
     vec_uint_push_back(s->assumptions, lit);
 }
@@ -337,8 +337,8 @@ int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
 {
     int i, status;
     // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions));
-    // printf("[Satoko]   + Variables: %d\n", solver_varnum(s));
-    // printf("[Satoko]   + Clauses: %d\n", solver_clausenum(s));
+    // printf("[Satoko]   + Variables: %d\n", satoko_varnum(s));
+    // printf("[Satoko]   + Clauses: %d\n", satoko_clausenum(s));
     // printf("[Satoko]   + Trail size: %d\n", vec_uint_size(s->trail));
     // printf("[Satoko]   + Queue head: %d\n", s->i_qhead);
     // solver_debug_check_trail(s);
@@ -365,9 +365,14 @@ int satoko_final_conflict(solver_t *s, int **out)
     return vec_uint_size(s->final_conflict);
 }
 
-satoko_stats_t satoko_stats(satoko_t *s)
+satoko_stats_t * satoko_stats(satoko_t *s)
 {
-    return s->stats;
+    return &s->stats;
+}
+
+satoko_opts_t * satoko_options(satoko_t *s)
+{
+    return &s->opts;
 }
 
 void satoko_bookmark(satoko_t *s)
@@ -493,7 +498,7 @@ void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
 {
     int i;
     if (!solver_has_marks(s))
-        s->marks = vec_char_init(solver_varnum(s), 0);
+        s->marks = vec_char_init(satoko_varnum(s), 0);
     for (i = 0; i < n_vars; i++) {
         var_set_mark(s, pvars[i]);
         vec_sdbl_assign(s->activity, pvars[i], 0);
@@ -532,11 +537,11 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
     }
     fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
     for (i = 0; i < vec_char_size(s->assigns); i++) {
-        if ( var_value(s, i) != VAR_UNASSING ) {
+        if ( var_value(s, i) != SATOKO_VAR_UNASSING ) {
             if (zero_var)
-                fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i) : i);
+                fprintf(file, "%d\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i) : i);
             else
-                fprintf(file, "%d 0\n", var_value(s, i) == LIT_FALSE ? -(int)(i + 1) : i + 1);
+                fprintf(file, "%d 0\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i + 1) : i + 1);
         }
     }
     array = vec_uint_data(s->originals);
@@ -552,5 +557,56 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
 
 }
 
+int satoko_varnum(satoko_t *s)
+{
+    return vec_char_size(s->assigns);
+}
+
+int satoko_clausenum(satoko_t *s)
+{
+    return vec_uint_size(s->originals);
+}
+
+int satoko_learntnum(satoko_t *s)
+{
+    return vec_uint_size(s->learnts);
+}
+
+int satoko_conflictnum(satoko_t *s)
+{
+    return satoko_stats(s)->n_conflicts;
+}
+
+void satoko_set_stop(satoko_t *s, int * pstop)
+{
+    s->pstop = pstop;
+}
+
+void satoko_set_stop_func(satoko_t *s, int (*fnct)(int))
+{
+    s->pFuncStop = fnct;
+}
+
+void satoko_set_runid(satoko_t *s, int id)
+{
+    s->RunId = id;
+}
+
+int satoko_read_cex_varvalue(satoko_t *s, int ivar)
+{
+    return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE;
+}
+
+abctime satoko_set_runtime_limit(satoko_t* s, abctime Limit)
+{
+    abctime nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
+
+char satoko_var_polarity(satoko_t *s, unsigned var)
+{
+    return vec_char_at(s->polarity, var);
+}
 
 ABC_NAMESPACE_IMPL_END