Version abc80130

1 files changed, 72 insertions, 704 deletions

diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 58614584..4fb059e5 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 sat_solver.]
+  Synopsis    [Procedures to solve the miter using the internal SAT solver.]
 
   Author      [Alan Mishchenko]
   
@@ -19,167 +19,79 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "satSolver.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
-extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
-static nMuxes;
+static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Attempts to solve the miter using an internal SAT sat_solver.]
+  Synopsis    [Attempts to solve the miter using an internal SAT solver.]
 
-  Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+  Description [Returns 1 if the miter is SAT.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
+bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    sat_solver * pSat;
+    solver * pSat;
     lbool   status;
-    int RetValue, clk;
- 
-    if ( pNumConfs )
-        *pNumConfs = 0;
-    if ( pNumInspects )
-        *pNumInspects = 0;
+    int clk;
 
+    assert( Abc_NtkIsBddLogic(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
-//    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) );
+    if ( Abc_NtkPoNum(pNtk) > 1 )
+        fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" );
 
-    // load clauses into the sat_solver
+    // load clauses into the solver
     clk = clock();
-    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
-    if ( pSat == NULL )
-        return 1;
-//printf( "%d \n", pSat->clauses.size );
-//sat_solver_delete( pSat );
-//return 1;
-
-//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    pSat = Abc_NtkMiterSatCreate( pNtk );
+//    printf( "Created SAT problem with %d variable and %d clauses.   ", 
+//        solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
-    status = sat_solver_simplify(pSat);
-//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    status = solver_simplify(pSat);
+//    printf( "Simplified the problem to %d variables and %d clauses. ", 
+//        solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
-    if ( status == 0 )
+    if ( status == l_False )
     {
-        sat_solver_delete( pSat );
-//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return 1;
+        solver_delete( pSat );
+        printf( "The problem is UNSAT after simplification.\n" );
+        return 0;
     }
 
     // solve the miter
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    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" );
-        RetValue = -1;
-    }
-    else if ( status == l_True )
-    {
-//        printf( "The problem is SATISFIABLE.\n" );
-        RetValue = 0;
-    }
-    else if ( status == l_False )
-    {
-//        printf( "The problem is UNSATISFIABLE.\n" );
-        RetValue = 1;
-    }
-    else
-        assert( 0 );
-//    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 = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-        Vec_IntFree( vCiIds );
-    }
-    // free the sat_solver
-    if ( fVerbose )
-        Sat_SolverPrintStats( stdout, pSat );
-
-    if ( pNumConfs )
-        *pNumConfs = (int)pSat->stats.conflicts;
-    if ( pNumInspects )
-        *pNumInspects = (int)pSat->stats.inspects;
-
-sat_solver_store_write( pSat, "trace.cnf" );
-sat_solver_store_free( pSat );
-
-    sat_solver_delete( pSat );
-    return RetValue;
+    status = solver_solve( pSat, NULL, NULL );
+//    if ( fVerbose )
+//    {
+    printf( "The problem is %5s. ", (status == l_True)? "SAT" : "UNSAT" );
+    PRT( "SAT solver time", clock() - clk );
+//    }
+    // free the solver
+    solver_delete( pSat );
+    return status == l_True;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the array of CI IDs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vCiIds;
-    Abc_Obj_t * pObj;
-    int i;
-    vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        Vec_IntPush( vCiIds, (int)pObj->pCopy );
-    return vCiIds;
-}
-
-
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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->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 sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
+  Synopsis    [Sets up the SAT solver.]
 
   Description []
                
@@ -188,461 +100,43 @@ int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
 {
+    solver * pSat;
+    Extra_MmFlex_t * pMmFlex;
     Abc_Obj_t * pNode;
-    int i;
-//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 sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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->sat_solver_stats.clauses );
-
-    assert( !Abc_ObjIsComplement( pNode ) );
-    assert( Abc_ObjIsNode( pNode ) );
-
-//    nVars = sat_solver_nvars(pSat);
-    Var = (int)pNode->pCopy;
-//    Var = pNode->Id;
-
-//    assert( Var  < nVars ); 
-    for ( i = 0; i < vSuper->nSize; i++ )
-    {
-        // get the predecessor nodes
-        // get the complemented attributes of the nodes
-        fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
-        // determine the variable numbers
-        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
-//        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
-
-        // check that the variables are in the SAT manager
-//        assert( Var1 < nVars );
-
-        // suppose the AND-gate is A * B = C
-        // add !A => !C   or   A + !C
-    //  fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
-        vVars->nSize = 0;
-        Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
-        Vec_IntPush( vVars, toLitCond(Var,  1     ) );
-        if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-            return 0;
-    }
-
-    // add A & B => C   or   !A + !B + C
-//  fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
-    vVars->nSize = 0;
-    for ( i = 0; i < vSuper->nSize; i++ )
-    {
-        // get the predecessor nodes
-        // get the complemented attributes of the nodes
-        fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
-        // determine the variable numbers
-        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
-//        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
-        // add this variable to the array
-        Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
-    }
-    Vec_IntPush( vVars, toLitCond(Var, 0) );
-    return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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->sat_solver_stats.clauses );
-
-    assert( !Abc_ObjIsComplement( pNode ) );
-    assert( Abc_NodeIsMuxType( pNode ) );
-    // get the variable numbers
-    VarF = (int)pNode->pCopy;
-    VarI = (int)pNodeC->pCopy;
-    VarT = (int)Abc_ObjRegular(pNodeT)->pCopy;
-    VarE = (int)Abc_ObjRegular(pNodeE)->pCopy;
-//    VarF = (int)pNode->Id;
-//    VarI = (int)pNodeC->Id;
-//    VarT = (int)Abc_ObjRegular(pNodeT)->Id;
-//    VarE = (int)Abc_ObjRegular(pNodeE)->Id;
-
-    // get the complementation flags
-    fCompT = Abc_ObjIsComplement(pNodeT);
-    fCompE = Abc_ObjIsComplement(pNodeE);
-
-    // f = ITE(i, t, e)
-    // i' + t' + f
-    // i' + t  + f'
-    // i  + e' + f
-    // i  + e  + f'
-    // create four clauses
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarI,  1) );
-    Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    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 ( !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 ( !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 ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
- 
-    if ( VarT == VarE )
-    {
-//        assert( fCompT == !fCompE );
-        return 1;
-    }
-
-    // two additional clauses
-    // t' & e' -> f'       t  + e   + f'
-    // t  & e  -> f        t' + e'  + f 
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
-    Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    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 sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
-{
-    int RetValue1, RetValue2, i;
-    // check if the node is visited
-    if ( Abc_ObjRegular(pNode)->fMarkB )
-    {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pNode )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Abc_ObjNot(pNode) )
-                return -1;
-        assert( 0 );
-        return 0;
-    }
-    // if the new node is complemented or a PI, another gate begins
-    if ( !fFirst )
-    if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) )
-    {
-        Vec_PtrPush( vSuper, pNode );
-        Abc_ObjRegular(pNode)->fMarkB = 1;
-        return 0;
-    }
-    assert( !Abc_ObjIsComplement(pNode) );
-    assert( Abc_ObjIsNode(pNode) );
-    // go through the branches
-    RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux );
-    RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(pNode), vSuper, 0, fStopAtMux );
-    if ( RetValue1 == -1 || RetValue2 == -1 )
-        return -1;
-    // return 1 if at least one branch has a duplicate
-    return RetValue1 || RetValue2;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
-{
-    int RetValue, i;
-    assert( !Abc_ObjIsComplement(pNode) );
-    // collect the nodes in the implication supergate
-    Vec_PtrClear( vNodes );
-    RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
-    assert( vNodes->nSize > 1 );
-    // unmark the visited nodes
-    for ( i = 0; i < vNodes->nSize; i++ )
-        Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
-    // if we found the node and its complement in the same implication supergate, 
-    // return empty set of nodes (meaning that we should use constant-0 node)
-    if ( RetValue == -1 )
-        vNodes->nSize = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the factor of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
-{
-//  nLevelMax = ((nLevelMax)/2)*3;
-    assert( (int)pObj->Level <= nLevelMax );
-//    return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
-    return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
-//    return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets up the SAT sat_solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
-    Vec_Ptr_t * vNodes, * vSuper;
+    Vec_Str_t * vCube;
     Vec_Int_t * vVars;
-    int i, k, fUseMuxes = 1;
-    int clk1 = clock();
-//    int fOrderCiVarsFirst = 0;
-    int nLevelsMax = Abc_AigLevel(pNtk);
-    int RetValue = 0;
-
-    assert( Abc_NtkIsStrash(pNtk) );
+    char * pSop0, * pSop1;
+    int i;
 
-    // clean the CI node pointers
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = NULL;
+    assert( Abc_NtkIsBddLogic(pNtk) );
 
     // start the data structures
-    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
-
-    // add the clause for the constant node
-    pNode = Abc_AigConst1(pNtk);
-    pNode->fMarkA = 1;
-    pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
-    Vec_PtrPush( vNodes, pNode );
-    Abc_NtkClauseTriv( pSat, pNode, vVars );
-/*
-    // add the PI variables first
-    Abc_NtkForEachCi( pNtk, pNode, i )
-    {
-        pNode->fMarkA = 1;
-        pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
-        Vec_PtrPush( vNodes, pNode );
-    }
-*/
-    // collect the nodes that need clauses and top-level assignments
-    Vec_PtrClear( vSuper );
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        // get the fanin
-        pFanin = Abc_ObjFanin0(pNode);
-        // create the node's variable
-        if ( pFanin->fMarkA == 0 )
-        {
-            pFanin->fMarkA = 1;
-            pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
-            Vec_PtrPush( vNodes, pFanin );
-        }
-        // add the trivial clause
-        Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
-    }
-    if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
-        goto Quits;
-
-
-    // add the clauses
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        assert( !Abc_ObjIsComplement(pNode) );
-        if ( !Abc_AigNodeIsAnd(pNode) )
-            continue;
-//printf( "%d ", pNode->Id );
+    pSat    = solver_new();
+    pMmFlex = Extra_MmFlexStart();
+    vCube   = Vec_StrAlloc( 100 );
+    vVars   = Vec_IntAlloc( 100 );
 
-        // add the clauses
-        if ( fUseMuxes && Abc_NodeIsMuxType(pNode) )
-        {
-            nMuxes++;
-
-            pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
-            Vec_PtrClear( vSuper );
-            Vec_PtrPush( vSuper, pNodeC );
-            Vec_PtrPush( vSuper, pNodeT );
-            Vec_PtrPush( vSuper, pNodeE );
-            // add the fanin nodes to explore
-            Vec_PtrForEachEntry( vSuper, pFanin, k )
-            {
-                pFanin = Abc_ObjRegular(pFanin);
-                if ( pFanin->fMarkA == 0 )
-                {
-                    pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
-                    Vec_PtrPush( vNodes, pFanin );
-                }
-            }
-            // add the clauses
-            if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
-                goto Quits;
-        }
-        else
-        {
-            // get the supergate
-            Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper );
-            // add the fanin nodes to explore
-            Vec_PtrForEachEntry( vSuper, pFanin, k )
-            {
-                pFanin = Abc_ObjRegular(pFanin);
-                if ( pFanin->fMarkA == 0 )
-                {
-                    pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
-                    Vec_PtrPush( vNodes, pFanin );
-                }
-            }
-            // add the clauses
-            if ( vSuper->nSize == 0 )
-            {
-                if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
-//                if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
-                    goto Quits;
-            }
-            else
-            {
-                if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
-                    goto Quits;
-            }
-        }
-    }
-/*
-    // set preferred variables
-    if ( fOrderCiVarsFirst )
+    // add clauses for each internal nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        int * pPrefVars = ALLOC( int, Abc_NtkCiNum(pNtk) );
-        int nVars = 0;
-        Abc_NtkForEachCi( pNtk, pNode, i )
-        {
-            if ( pNode->fMarkA == 0 )
-                continue;
-            pPrefVars[nVars++] = (int)pNode->pCopy;
-        }
-        nVars = ABC_MIN( nVars, 10 );
-        ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
+        // derive SOPs for both phases of the node
+        Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
+        // add the clauses to the solver
+        Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
     }
-*/
-    RetValue = 1;
-Quits :
+    // add clauses for each PO
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+
     // delete
+    Vec_StrFree( vCube );
     Vec_IntFree( vVars );
-    Vec_PtrFree( vNodes );
-    Vec_PtrFree( vSuper );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets up the SAT sat_solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
-{
-    sat_solver * pSat;
-    Abc_Obj_t * pNode;
-    int RetValue, i, clk = clock();
-
-    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) );
-    if ( Abc_NtkIsBddLogic(pNtk) )
-        return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes);
-
-    nMuxes = 0;
-    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 );
-    if ( RetValue == 0 )
-    {
-        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 sat_solver", clock() - clk );
+    Extra_MmFlexStop( pMmFlex, 0 );
     return pSat;
 }
 
-
-
-
 /**Function*************************************************************
 
   Synopsis    [Adds clauses for the internal node.]
@@ -654,33 +148,14 @@ sat_solver_store_mark_roots( pSat );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
     int i, c, nFanins;
-    int RetValue;
     char * pCube;
 
     nFanins = Abc_ObjFaninNum( pNode );
     assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
-
-//    if ( nFanins == 0 )
-    if ( Cudd_Regular(pNode->pData) == Cudd_ReadOne(pNode->pNtk->pManFunc) )
-    {
-        vVars->nSize = 0;
-//        if ( Abc_SopIsConst1(pSop1) )
-        if ( !Cudd_IsComplement(pNode->pData) )
-            Vec_IntPush( vVars, toLit(pNode->Id) );
-        else
-            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" );
-            return 0;
-        }
-        return 1;
-    }
  
     // add clauses for the negative phase
     for ( c = 0; ; c++ )
@@ -696,15 +171,10 @@ int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t
             if ( pCube[i] == '0' )
                 Vec_IntPush( vVars, toLit(pFanin->Id) );
             else if ( pCube[i] == '1' )
-                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" );
-            return 0;
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
     }
 
     // add clauses for the positive phase
@@ -721,17 +191,11 @@ int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t
             if ( pCube[i] == '0' )
                 Vec_IntPush( vVars, toLit(pFanin->Id) );
             else if ( pCube[i] == '1' )
-                Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-        if ( !RetValue ) 
-        {
-            printf( "The CNF is trivially UNSAT.\n" );
-            return 0;
-        }
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
     }
-    return 1;
 }
 
 /**Function*************************************************************
@@ -745,10 +209,9 @@ int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
-    int RetValue;
 
     pFanin = Abc_ObjFanin0(pNode);
     if ( Abc_ObjFaninC0(pNode) )
@@ -756,126 +219,31 @@ int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVa
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-        if ( !RetValue ) 
-        {
-            printf( "The CNF is trivially UNSAT.\n" );
-            return 0;
-        }
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 
         vVars->nSize = 0;
-        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" );
-            return 0;
-        }
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
     }
     else
     {
         vVars->nSize = 0;
-        Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-        if ( !RetValue ) 
-        {
-            printf( "The CNF is trivially UNSAT.\n" );
-            return 0;
-        }
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, 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" );
-            return 0;
-        }
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
     }
 
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLit(pNode->Id) );
-    RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-    if ( !RetValue ) 
-    {
-        printf( "The CNF is trivially UNSAT.\n" );
-        return 0;
-    }
-    return 1;
+    solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Sets up the SAT sat_solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
-{
-    sat_solver * pSat;
-    Extra_MmFlex_t * pMmFlex;
-    Abc_Obj_t * pNode;
-    Vec_Str_t * vCube;
-    Vec_Int_t * vVars;
-    char * pSop0, * pSop1;
-    int i;
-
-    assert( Abc_NtkIsBddLogic(pNtk) );
-
-    // transfer the IDs to the copy field
-    Abc_NtkForEachPi( pNtk, pNode, i )
-        pNode->pCopy = (void *)pNode->Id;
-
-    // start the data structures
-    pSat    = sat_solver_new();
-sat_solver_store_alloc( pSat );
-    pMmFlex = Extra_MmFlexStart();
-    vCube   = Vec_StrAlloc( 100 );
-    vVars   = Vec_IntAlloc( 100 );
-
-    // 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 sat_solver
-        if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
-        {
-            sat_solver_delete( pSat );
-            pSat = NULL;
-            goto finish;
-        }
-    }
-    // add clauses for each PO
-    Abc_NtkForEachPo( pNtk, pNode, i )
-    {
-        if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) )
-        {
-            sat_solver_delete( pSat );
-            pSat = NULL;
-            goto finish;
-        }
-    }
-sat_solver_store_mark_roots( pSat );
-
-finish:
-    // delete
-    Vec_StrFree( vCube );
-    Vec_IntFree( vVars );
-    Extra_MmFlexStop( pMmFlex );
-    return pSat;
-}
-
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///