Version abc51225

4 files changed, 583 insertions, 14 deletions

diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 53ad88c2..167e7552 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), 
                             Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
+{
+    Abc_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Abc_AigMiter_rec( pMan, ppObjs,           nObjs/2 );
+    pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
+    return Abc_AigOr( pMan, pObj1, pObj2 );
+}
+ 
 /**Function*************************************************************
 
   Synopsis    [Implements the miter.]
@@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 ***********************************************************************/
 Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
 {
+    int i;
+    if ( vPairs->nSize == 0 )
+        return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) );
+    assert( vPairs->nSize % 2 == 0 );
+    // go through the cubes of the node's SOP
+    for ( i = 0; i < vPairs->nSize; i += 2 )
+        vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    vPairs->nSize = vPairs->nSize/2;
+    return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
+{
     Abc_Obj_t * pMiter, * pXor;
     int i;
     assert( vPairs->nSize % 2 == 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 71b76cf6..70cd2e6c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     } 
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
+        return 0;
+    }
+
+/*
     if ( !Abc_NtkIsLogic(pNtk) )
     {
         fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
@@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkUnmap(pNtk);
     if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkSopToBdd(pNtk);
-
-    RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
-    if ( RetValue == -1 )
-        printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
-    else if ( RetValue == 0 )
-        printf( "The miter is SATISFIABLE.\n" );
+*/
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
+        if ( RetValue == -1 )
+            printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+        else if ( RetValue == 0 )
+            printf( "The miter is SATISFIABLE.\n" );
+        else
+            printf( "The miter is UNSATISFIABLE.\n" );
+    }
     else
-        printf( "The miter is UNSATISFIABLE.\n" );
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
+        if ( RetValue == -1 )
+            printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+        else if ( RetValue == 0 )
+            printf( "The miter is SATISFIABLE.\n" );
+        else
+            printf( "The miter is UNSATISFIABLE.\n" );
+        Abc_NtkDelete( pTemp );
+    }
     return 0;
 
 usage:
     fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
-    fprintf( pErr, "\t         solves the miter\n" );
+    fprintf( pErr, "\t         solves the combinational miter\n" );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-//    Abc_NtkDeriveEsops( pNtk );
-//    Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
-    printf( "This command is currently not used.\n" );
+    Abc_NtkTestEsop( pNtk );
+//    Abc_NtkTestSop( pNtk );
+//    printf( "This command is currently not used.\n" );
 
 /*
     // run the command
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 4a65659c..8c8636c5 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -27,6 +27,10 @@
 static int  Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 static int  Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 
+static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
+
+static nMuxes;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -129,7 +133,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     Vec_Str_t * vCube;
     Vec_Int_t * vVars;
     char * pSop0, * pSop1;
-    int i;
+    int i, clk = clock();
 
     assert( Abc_NtkIsBddLogic(pNtk) );
 
@@ -159,6 +163,8 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     }
 //    Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
 
+    PRT( "Creating solver", clock() - clk );
+
     // delete
     Vec_StrFree( vCube );
     Vec_IntFree( vVars );
@@ -291,6 +297,495 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 }
 
 
+
+
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Attempts to solve the miter using an internal SAT solver.]
+
+  Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+{
+    solver * pSat;
+    lbool   status;
+    int RetValue, clk;
+
+    assert( Abc_NtkIsStrash(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) );
+
+    // load clauses into the solver
+    clk = clock();
+    pSat = Abc_NtkMiterSatCreate2( pNtk );
+    if ( pSat == NULL )
+        return 1;
+//    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 = 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 )
+    {
+        solver_delete( pSat );
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return 1;
+    }
+
+    // solve the miter
+    clk = clock();
+    if ( fVerbose )
+        pSat->verbosity = 1;
+    status = solver_solve( pSat, NULL, NULL, nSeconds );
+    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 solver time", clock() - clk );
+
+    // if the problem is SAT, get the counterexample
+    if ( status == l_True )
+    {
+        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+        pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
+        Vec_IntFree( vCiIds );
+    }
+    // free the solver
+    solver_delete( pSat );
+    return RetValue;
+}
+
+
+
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseTriv( 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 );
+    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 );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseAnd( 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 );
+
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+
+//    nVars = 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 ( !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 solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  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 VarF, VarI, VarT, VarE, fCompT, fCompE;
+//printf( "Adding mux %d.         %d\n", pNode->Id, (int)pSat->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 ( !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 ) )
+        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 ) )
+        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 ) )
+        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 ( !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 );
+}
+
+/**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    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
+    Vec_Ptr_t * vNodes, * vSuper;
+    Vec_Int_t * vVars;
+    int i, k, fUseMuxes = 1;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // start the data structures
+    vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the 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_NtkConst1(pNtk);
+    pNode->fMarkA = 1;
+    pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
+    Vec_PtrPush( vNodes, pNode );
+    Abc_NtkClauseTriv( pSat, pNode, vVars );
+
+    // collect the nodes that need clauses and top-level assignments
+    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
+        if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
+            return 0;
+    }
+
+    // add the clauses
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        assert( !Abc_ObjIsComplement(pNode) );
+        if ( !Abc_NodeIsAigAnd(pNode) )
+            continue;
+//printf( "%d ", pNode->Id );
+
+        // 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 ) )
+                return 0;
+        }
+        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 ) )
+                    return 0;
+            }
+            else
+            {
+                if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
+                    return 0;
+            }
+        }
+    }
+
+    // delete
+    Vec_IntFree( vVars );
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vSuper );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
+{
+    solver * pSat;
+    Abc_Obj_t * pNode;
+    int RetValue, i, clk = clock();
+
+    nMuxes = 0;
+
+    pSat = solver_new();
+    RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        pNode->fMarkA = 0;
+    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+    if ( RetValue == 0 )
+    {
+        solver_delete(pSat);
+        return NULL;
+    }
+    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+    PRT( "Creating solver", clock() - clk );
+    return pSat;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 070c871d..b30a6452 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
+    Params.fFuncRed = 0;
+    Params.nPatsRand = 0;
+    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
@@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
+    Params.fFuncRed = 0;
+    Params.nPatsRand = 0;
+    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );