Version abc70123

8 files changed, 111 insertions, 237 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 849a888a..d843bca6 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -38,7 +38,6 @@ extern "C" {
 #include "cuddInt.h"
 #include "hop.h"
 #include "extra.h"
-#include "solver.h"
 #include "vec.h"
 #include "stmm.h"
 #include "nm.h"
@@ -118,6 +117,12 @@ typedef enum {
 #endif
 #endif
 
+#ifdef _WIN32
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
+#else
+typedef long long          sint64;
+#endif
+
 typedef struct Abc_Lib_t_       Abc_Lib_t;
 typedef struct Abc_Ntk_t_       Abc_Ntk_t;
 typedef struct Abc_Obj_t_       Abc_Obj_t;
@@ -725,8 +730,8 @@ extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, i
 /*=== abcRewrite.c ==========================================================*/
 extern int                Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
-extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes );
+extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
+extern void *             Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
@@ -761,8 +766,6 @@ extern bool               Abc_SopIsAndType( char * pSop );
 extern bool               Abc_SopIsOrType( char * pSop );
 extern int                Abc_SopIsExorType( char * pSop );
 extern bool               Abc_SopCheck( char * pSop, int nFanins );
-extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
-extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 extern char *             Abc_SopFromTruthBin( char * pTruth );
 extern char *             Abc_SopFromTruthHex( char * pTruth );
 /*=== abcStrash.c ==========================================================*/
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index ffef42c9..4e9a6548 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -799,77 +799,6 @@ bool Abc_SopCheck( char * pSop, int nFanins )
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Writes the CNF of the SOP into file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars )
-{
-    char * pChar;
-    int i;
-    // check the logic function of the node
-    for ( pChar = pClauses; *pChar; pChar++ )
-    {
-        // write the clause
-        for ( i = 0; i < vVars->nSize; i++, pChar++ )
-            if ( *pChar == '0' )
-                fprintf( pFile, "%d ", vVars->pArray[i] );
-            else if ( *pChar == '1' )
-                fprintf( pFile, "%d ", -vVars->pArray[i] );
-        fprintf( pFile, "0\n" );
-        // check that the remainig part is fine
-        assert( *pChar == ' ' );
-        pChar++;
-        assert( *pChar == '1' );
-        pChar++;
-        assert( *pChar == '\n' );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the clauses of for the CNF to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp )
-{
-    char * pChar;
-    int i, RetValue;
-    // check the logic function of the node
-    for ( pChar = pClauses; *pChar; pChar++ )
-    {
-        // add the clause
-        vTemp->nSize = 0;
-        for ( i = 0; i < vVars->nSize; i++, pChar++ )
-            if ( *pChar == '0' )
-                Vec_IntPush( vTemp, toLit(vVars->pArray[i]) );
-            else if ( *pChar == '1' )
-                Vec_IntPush( vTemp, neg(toLit(vVars->pArray[i])) );
-        // add the clause to the solver
-        RetValue = solver_addclause( pSat, vTemp->pArray, vTemp->pArray + vTemp->nSize );
-        assert( RetValue != 1 );
-        // check that the remainig part is fine
-        assert( *pChar == ' ' );
-        pChar++;
-        assert( *pChar == '1' );
-        pChar++;
-        assert( *pChar == '\n' );
-    }
-}
-
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f6c180da..a6552951 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9206,7 +9206,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
-    int fJFront;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
@@ -9217,12 +9216,11 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fJFront    = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvjh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9248,9 +9246,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
-        case 'j':
-            fJFront ^= 1;
-            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -9275,13 +9270,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     clk = clock();
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
     }
     else
     {
         assert( Abc_NtkIsLogic(pNtk) );
         Abc_NtkLogicToBdd( pNtk );
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
     }
 
     // verify that the pattern is correct
@@ -9316,12 +9311,11 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sat [-C num] [-I num] [-jvh]\n" );
+    fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
-    fprintf( pErr, "\t-j     : toggle the use of J-frontier [default = %s]\n", fJFront? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 610f5b5c..243067ce 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -491,7 +491,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     }
 
     // if SAT only, solve without iteration
-    RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL );
     if ( RetValue >= 0 )
         return RetValue;
 
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index d206ae6e..6d1ed161 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -79,7 +79,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
@@ -99,7 +99,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
         // try brute-force SAT
         clk = clock();
         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, 0, &nSatConfs, &nSatInspects );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
@@ -213,7 +213,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
         }
         clk = clock();
         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, 0, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index cf67db6d..96540269 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Procedures to solve the miter using the internal SAT solver.]
+  Synopsis    [Procedures to solve the miter using the internal SAT sat_solver.]
 
   Author      [Alan Mishchenko]
   
@@ -19,12 +19,13 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "satSolver.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
+static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
 extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
 static nMuxes;
 
@@ -34,7 +35,7 @@ static nMuxes;
 
 /**Function*************************************************************
 
-  Synopsis    [Attempts to solve the miter using an internal SAT solver.]
+  Synopsis    [Attempts to solve the miter using an internal SAT sat_solver.]
 
   Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
                
@@ -43,9 +44,9 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
 {
-    solver * pSat;
+    sat_solver * pSat;
     lbool   status;
     int RetValue, clk;
 
@@ -59,22 +60,22 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
 //    if ( Abc_NtkPoNum(pNtk) > 1 )
 //        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
-    // load clauses into the solver
+    // load clauses into the sat_solver
     clk = clock();
-    pSat = Abc_NtkMiterSatCreate( pNtk, fJFront, 0 );
+    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
     if ( pSat == NULL )
         return 1;
-//    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
-    status = solver_simplify(pSat);
-//    printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+    status = sat_solver_simplify(pSat);
+//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
     if ( status == 0 )
     {
-        solver_delete( pSat );
+        sat_solver_delete( pSat );
 //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
         return 1;
     }
@@ -83,7 +84,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit );
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
@@ -101,30 +102,30 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     }
     else
         assert( 0 );
-//    PRT( "SAT solver time", clock() - clk );
-//    printf( "The number of conflicts = %d.\n", (int)pSat->solver_stats.conflicts );
+//    PRT( "SAT sat_solver time", clock() - clk );
+//    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
 
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
     {
 //        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
         Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
-        pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
+        pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         Vec_IntFree( vCiIds );
     }
-    // free the solver
+    // free the sat_solver
     if ( fVerbose )
-        Asat_SatPrintStats( stdout, pSat );
+        Sat_SolverPrintStats( stdout, pSat );
 
     if ( pNumConfs )
-        *pNumConfs = (int)pSat->solver_stats.conflicts;
+        *pNumConfs = (int)pSat->stats.conflicts;
     if ( pNumInspects )
-        *pNumInspects = (int)pSat->solver_stats.inspects;
+        *pNumInspects = (int)pSat->stats.inspects;
 
-Sat_SolverTraceWrite( pSat, NULL, NULL, 0 );
-Sat_SolverTraceStop( pSat );
+sat_solver_store_write( pSat, "trace.cnf" );
+sat_solver_store_free( pSat );
 
-    solver_delete( pSat );
+    sat_solver_delete( pSat );
     return RetValue;
 }
 
@@ -163,13 +164,13 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
-//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
  
 /**Function*************************************************************
@@ -183,16 +184,16 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
+int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pNode;
     int i;
-//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
     Vec_PtrForEachEntry( vNodes, pNode, i )
         Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
  
 /**Function*************************************************************
@@ -206,15 +207,15 @@ int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
+int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
 {
     int fComp1, Var, Var1, i;
-//printf( "Adding AND %d.  (%d)    %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses );
+//printf( "Adding AND %d.  (%d)    %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->sat_solver_stats.clauses );
 
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
 
-//    nVars = solver_nvars(pSat);
+//    nVars = sat_solver_nvars(pSat);
     Var = (int)pNode->pCopy;
 //    Var = pNode->Id;
 
@@ -237,7 +238,7 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
         Vec_IntPush( vVars, toLitCond(Var,  1     ) );
-        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
             return 0;
     }
 
@@ -256,7 +257,7 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_
         Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
     }
     Vec_IntPush( vVars, toLitCond(Var, 0) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
  
 /**Function*************************************************************
@@ -270,10 +271,10 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars )
+int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars )
 {
     int VarF, VarI, VarT, VarE, fCompT, fCompE;
-//printf( "Adding mux %d.         %d\n", pNode->Id, (int)pSat->solver_stats.clauses );
+//printf( "Adding mux %d.         %d\n", pNode->Id, (int)pSat->sat_solver_stats.clauses );
 
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_NodeIsMuxType( pNode ) );
@@ -301,25 +302,25 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_
     Vec_IntPush( vVars, toLitCond(VarI,  1) );
     Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
     Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+    if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLitCond(VarI,  1) );
     Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
     Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+    if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLitCond(VarI,  0) );
     Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
     Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+    if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLitCond(VarI,  0) );
     Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
     Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+    if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
  
     if ( VarT == VarE )
@@ -335,13 +336,13 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_
     Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
     Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
     Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+    if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
     Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
     Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
 
 /**Function*************************************************************
@@ -442,7 +443,7 @@ int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets up the SAT solver.]
+  Synopsis    [Sets up the SAT sat_solver.]
 
   Description []
                
@@ -451,16 +452,14 @@ int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
+int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
     Vec_Ptr_t * vNodes, * vSuper;
-    Vec_Flt_t * vFactors;
-    Vec_Int_t * vVars, * vFanio;
-    Vec_Vec_t * vCircuit;
+    Vec_Int_t * vVars;
     int i, k, fUseMuxes = 1;
-    int clk1 = clock(), clk;
-    int fOrderCiVarsFirst = 0;
+    int clk1 = clock();
+//    int fOrderCiVarsFirst = 0;
     int nLevelsMax = Abc_AigLevel(pNtk);
     int RetValue = 0;
 
@@ -471,12 +470,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         pNode->pCopy = NULL;
 
     // start the data structures
-    vNodes  = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
+    vNodes  = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the sat_solver
     vSuper  = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
     vVars   = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
-    if ( fJFront )
-        vCircuit = Vec_VecAlloc( 1000 );
-//        vCircuit = Vec_VecStart( 184 );
 
     // add the clause for the constant node
     pNode = Abc_AigConst1(pNtk);
@@ -574,23 +570,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
                     goto Quits;
             }
         }
-        // add the variables to the J-frontier
-        if ( !fJFront )
-            continue;
-        // make sure that the fanin entries go first
-        assert( pNode->pCopy );
-        Vec_VecExpand( vCircuit, (int)pNode->pCopy );
-        vFanio = Vec_VecEntry( vCircuit, (int)pNode->pCopy );
-        Vec_PtrForEachEntryReverse( vSuper, pFanin, k )
-//        Vec_PtrForEachEntry( vSuper, pFanin, k )
-        {
-            pFanin = Abc_ObjRegular( pFanin );
-            assert( pFanin->pCopy && pFanin->pCopy != pNode->pCopy );
-            Vec_IntPushFirst( vFanio, (int)pFanin->pCopy );
-            Vec_VecPush( vCircuit, (int)pFanin->pCopy, pNode->pCopy );
-        }
     }
-
+/*
     // set preferred variables
     if ( fOrderCiVarsFirst )
     {
@@ -603,45 +584,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             pPrefVars[nVars++] = (int)pNode->pCopy;
         }
         nVars = ABC_MIN( nVars, 10 );
-        Asat_SolverSetPrefVars( pSat, pPrefVars, nVars );
-    }
-
-    // create the variable order
-    if ( fJFront )
-    {
-    clk = clock();
-        Asat_JManStart( pSat, vCircuit );
-        Vec_VecFree( vCircuit );
-    PRT( "Setup", clock() - clk );
-//        Asat_JManStop( pSat );
-//    PRT( "Total", clock() - clk1 );
+        ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
     }
-
-    Abc_NtkStartReverseLevels( pNtk );
-    vFactors = Vec_FltStart( solver_nvars(pSat) );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( pNode->fMarkA )
-            Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, Abc_NodeReadReverseLevel(pNode)) );
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        if ( pNode->fMarkA )
-            Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, nLevelsMax+1) );
-    // set the PI levels
-//    Abc_NtkForEachObj( pNtk, pNode, i )
-//        if ( pNode->fMarkA )
-//            printf( "(%d) %.3f   ", Abc_NodeReadReverseLevel(pNode), Vec_FltEntry(vFactors, (int)pNode->pCopy) );
-//    printf( "\n" );
-    Asat_SolverSetFactors( pSat, Vec_FltReleaseArray(vFactors) );
-    Vec_FltFree( vFactors );
-
-/*
-    // create factors
-    vLevels = Vec_IntStart( Vec_PtrSize(vNodes) );   // the reverse levels of the nodes
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        if ( pNode->fMarkA )
-            Vec_IntWriteEntry( vLevels, (int)pNode->pCopy, Abc_NtkNodeFactor(pNode, nLevelsMax) );
-    assert( Vec_PtrSize(vNodes) == Vec_IntSize(vLevels) );
-    Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
-    Vec_IntFree( vLevels );
 */
     RetValue = 1;
 Quits :
@@ -654,7 +598,7 @@ Quits :
 
 /**Function*************************************************************
 
-  Synopsis    [Sets up the SAT solver.]
+  Synopsis    [Sets up the SAT sat_solver.]
 
   Description []
                
@@ -663,9 +607,9 @@ Quits :
   SeeAlso     []
 
 ***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes )
+void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
 {
-    solver * pSat;
+    sat_solver * pSat;
     Abc_Obj_t * pNode;
     int RetValue, i, clk = clock();
 
@@ -674,18 +618,21 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes )
         return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes);
 
     nMuxes = 0;
-    pSat = solver_new();
-    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront );
+    pSat = sat_solver_new();
+sat_solver_store_alloc( pSat );
+    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
+sat_solver_store_mark_roots( pSat );
+
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->fMarkA = 0;
-//    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+//    ASat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
     if ( RetValue == 0 )
     {
-        solver_delete(pSat);
+        sat_solver_delete(pSat);
         return NULL;
     }
 //    printf( "Ands = %6d.  Muxes = %6d (%5.2f %%).  ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
-//    PRT( "Creating solver", clock() - clk );
+//    PRT( "Creating sat_solver", clock() - clk );
     return pSat;
 }
 
@@ -703,7 +650,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
     int i, c, nFanins;
@@ -721,8 +668,8 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p
         if ( !Cudd_IsComplement(pNode->pData) )
             Vec_IntPush( vVars, toLit(pNode->Id) );
         else
-            Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+            Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -745,10 +692,10 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p
             if ( pCube[i] == '0' )
                 Vec_IntPush( vVars, toLit(pFanin->Id) );
             else if ( pCube[i] == '1' )
-                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+                Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
         }
-        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -770,10 +717,10 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p
             if ( pCube[i] == '0' )
                 Vec_IntPush( vVars, toLit(pFanin->Id) );
             else if ( pCube[i] == '1' )
-                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+                Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -794,7 +741,7 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
     int RetValue;
@@ -805,7 +752,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -813,9 +760,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
         }
 
         vVars->nSize = 0;
-        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
-        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -825,9 +772,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
     else
     {
         vVars->nSize = 0;
-        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -836,8 +783,8 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
-        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
+        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
         if ( !RetValue ) 
         {
             printf( "The CNF is trivially UNSAT.\n" );
@@ -847,7 +794,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLit(pNode->Id) );
-    RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
     if ( !RetValue ) 
     {
         printf( "The CNF is trivially UNSAT.\n" );
@@ -858,7 +805,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets up the SAT solver.]
+  Synopsis    [Sets up the SAT sat_solver.]
 
   Description []
                
@@ -867,9 +814,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
-solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
+sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
 {
-    solver * pSat;
+    sat_solver * pSat;
     Extra_MmFlex_t * pMmFlex;
     Abc_Obj_t * pNode;
     Vec_Str_t * vCube;
@@ -884,22 +831,21 @@ solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
         pNode->pCopy = (void *)pNode->Id;
 
     // start the data structures
-    pSat    = solver_new();
+    pSat    = sat_solver_new();
+sat_solver_store_alloc( pSat );
     pMmFlex = Extra_MmFlexStart();
     vCube   = Vec_StrAlloc( 100 );
     vVars   = Vec_IntAlloc( 100 );
 
-Sat_SolverTraceStart( pSat, "trace.cnf" );
-
     // add clauses for each internal nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         // derive SOPs for both phases of the node
         Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 );
-        // add the clauses to the solver
+        // add the clauses to the sat_solver
         if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
         {
-            solver_delete( pSat );
+            sat_solver_delete( pSat );
             pSat = NULL;
             goto finish;
         }
@@ -909,11 +855,12 @@ Sat_SolverTraceStart( pSat, "trace.cnf" );
     {
         if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) )
         {
-            solver_delete( pSat );
+            sat_solver_delete( pSat );
             pSat = NULL;
             goto finish;
         }
     }
+sat_solver_store_mark_roots( pSat );
 
 finish:
     // delete
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index f3a069f4..c891772f 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -86,7 +86,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -268,7 +268,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index f12a1297..88695668 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "io.h"
+#include "satSolver.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -43,7 +44,7 @@ static Abc_Ntk_t * s_pNtk = NULL;
 ***********************************************************************/
 int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
 {
-    solver * pSat;
+    sat_solver * pSat;
     if ( Abc_NtkIsStrash(pNtk) )
         printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" );
     else
@@ -67,7 +68,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
     if ( Abc_NtkIsLogic(pNtk) )
         Abc_NtkLogicToBdd( pNtk );
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes );
+    pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
     if ( pSat == NULL )
     {
         fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
@@ -75,10 +76,10 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
     }        
     // write the clauses
     s_pNtk = pNtk;
-    Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
+    Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
     s_pNtk = NULL;
     // free the solver
-    solver_delete( pSat );
+    sat_solver_delete( pSat );
     return 1;
 }