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

6 files changed, 36 insertions, 42 deletions

diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c
index 8f7452e5..6ab8a92e 100644
--- a/src/sat/bmc/bmcBmc.c
+++ b/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 );
diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c
index 5c2df0d7..f9d65bbb 100644
--- a/src/sat/bmc/bmcBmc2.c
+++ b/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 );
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 26c93b72..f990a982 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/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 )
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c
index 1bfcd9d0..ea8ec2f6 100644
--- a/src/sat/bmc/bmcBmcS.c
+++ b/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 );  
diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c
index 6da70a1c..ee27496f 100644
--- a/src/sat/bmc/bmcMesh.c
+++ b/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 );
diff --git a/src/sat/bmc/bmcMesh2.c b/src/sat/bmc/bmcMesh2.c
index e6662d7c..1553e5bb 100644
--- a/src/sat/bmc/bmcMesh2.c
+++ b/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) )