Version abc70123

1 files changed, 88 insertions, 141 deletions

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