Adding solver type in &sat.

6 files changed, 582 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index feabe0bb..13f8caea 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36123,10 +36123,21 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fNewSolver = 0, fCSat = 0, f0Proved = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JCSNanmtcxzvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'J':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->SolverType = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->SolverType < 0 )
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -36222,8 +36233,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxzvh]\n" );
+    Abc_Print( -2, "usage: &sat [-JCSN <num>] [-anmctxzvh]\n" );
     Abc_Print( -2, "\t         performs SAT solving for the combinational outputs\n" );
+    Abc_Print( -2, "\t-J num : the SAT solver type [default = %d]\n", pPars->SolverType );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
     Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 791955e4..1bc037c4 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -43,6 +43,7 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Cec_ParSat_t_ Cec_ParSat_t;
 struct Cec_ParSat_t_
 {
+    int              SolverType;    // SAT solver type
     int              nBTLimit;      // conflict limit at a node
     int              nSatVarMax;    // the max number of SAT variables
     int              nCallsRecycle; // calls to perform before recycling SAT solver
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 4e8e5497..f94bd27f 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -45,6 +45,7 @@ ABC_NAMESPACE_IMPL_START
 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSat_t) );
+    p->SolverType     =      -1;  // SAT solver type
     p->nBTLimit       =     100;  // conflict limit at a node
     p->nSatVarMax     =    2000;  // the max number of SAT variables
     p->nCallsRecycle  =     200;  // calls to perform before recycling SAT solver
@@ -237,7 +238,10 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Pro
     Gia_Man_t * pNew;
     Cec_ManPat_t * pPat;
     pPat = Cec_ManPatStart();
-    Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved );
+    if ( pPars->SolverType == -1 )
+        Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved );
+    else
+        CecG_ManSatSolve( pPat, pAig, pPars, f0Proved );
 //    pNew = Gia_ManDupDfsSkip( pAig );
     pNew = Gia_ManCleanup( pAig );
     Cec_ManPatStop( pPat );
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index 80663db9..f78e5f25 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "sat/bsat/satSolver.h"
+#include "sat/glucose2/AbcGlucose2.h"
 #include "misc/bar/bar.h"
 #include "aig/gia/gia.h"
 #include "cec.h"
@@ -80,7 +81,8 @@ struct Cec_ManSat_t_
     Gia_Man_t *      pAig;           // the AIG whose outputs are considered
     Vec_Int_t *      vStatus;        // status for each output
     // SAT solving
-    sat_solver *     pSat;           // recyclable SAT solver
+    sat_solver *     pSat;           // recyclable SAT solver (MiniSAT)
+    bmcg2_sat_solver*pSat2;          // recyclable SAT solver (Glucose)
     int              nSatVars;       // the counter of SAT variables
     int *            pSatVars;       // mapping of each node into its SAT var
     Vec_Ptr_t *      vUsedNodes;     // nodes whose SAT vars are assigned
@@ -212,6 +214,8 @@ extern int                  Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * p
 extern int                  Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
 extern void                 Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
 extern Vec_Int_t *          Cec_ManSatReadCex( Cec_ManSat_t * p );
+/*=== cecSolveG.c ============================================================*/
+extern void                 CecG_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved );
 /*=== ceFraeep.c ============================================================*/
 extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
 extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/proof/cec/cecSolveG.c b/src/proof/cec/cecSolveG.c
new file mode 100644
index 00000000..c86fc2d9
--- /dev/null
+++ b/src/proof/cec/cecSolveG.c
@@ -0,0 +1,556 @@
+/**CFile****************************************************************
+
+  FileName    [cecSolve.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinational equivalence checking.]
+
+  Synopsis    [Performs one round of SAT solving.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSolve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  CecG_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj )             { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; }
+static inline void CecG_ObjSetSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj, int Num ) { p->pSatVars[Gia_ObjId(p->pAig,pObj)] = Num;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value of the SAT variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CecG_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj )             
+{ 
+    return sat_solver_var_value( p->pSat, CecG_ObjSatNum(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_AddClausesMux( Cec_ManSat_t * p, Gia_Obj_t * pNode )
+{
+    Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+    assert( !Gia_IsComplement( pNode ) );
+    assert( Gia_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the variable numbers
+    VarF = CecG_ObjSatNum(p,pNode);
+    VarI = CecG_ObjSatNum(p,pNodeI);
+    VarT = CecG_ObjSatNum(p,Gia_Regular(pNodeT));
+    VarE = CecG_ObjSatNum(p,Gia_Regular(pNodeE));
+    // get the complementation flags
+    fCompT = Gia_IsComplement(pNodeT);
+    fCompE = Gia_IsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 1^fCompT);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 0^fCompT);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = toLitCond(VarT, 0^fCompT);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarT, 1^fCompT);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+    Gia_Obj_t * pFanin;
+    int * pLits, nLits, RetValue, i;
+    assert( !Gia_IsComplement(pNode) );
+    assert( Gia_ObjIsAnd( pNode ) );
+    // create storage for literals
+    nLits = Vec_PtrSize(vSuper) + 1;
+    pLits = ABC_ALLOC( int, nLits );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(CecG_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
+        pLits[1] = toLitCond(CecG_ObjSatNum(p,pNode), 1);
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Gia_Regular(pFanin)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNode->fPhase )                pLits[1] = lit_neg( pLits[1] );
+        }
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
+    {
+        pLits[i] = toLitCond(CecG_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Gia_Regular(pFanin)->fPhase )  pLits[i] = lit_neg( pLits[i] );
+        }
+    }
+    pLits[nLits-1] = toLitCond(CecG_ObjSatNum(p,pNode), 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNode->fPhase )  pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+    assert( RetValue );
+    ABC_FREE( pLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || 
+         (!fFirst && Gia_ObjValue(pObj) > 1) || 
+         (fUseMuxes && Gia_ObjIsMuxType(pObj)) )
+    {
+        Vec_PtrPushUnique( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    CecG_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    CecG_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
+{
+    assert( !Gia_IsComplement(pObj) );
+    assert( !Gia_ObjIsCi(pObj) );
+    Vec_PtrClear( vSuper );
+    CecG_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_ObjAddToFrontier( Cec_ManSat_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Gia_IsComplement(pObj) );
+    if ( CecG_ObjSatNum(p,pObj) )
+        return;
+    assert( CecG_ObjSatNum(p,pObj) == 0 );
+    if ( Gia_ObjIsConst0(pObj) )
+        return;
+    Vec_PtrPush( p->vUsedNodes, pObj );
+    CecG_ObjSetSatNum( p, pObj, p->nSatVars++ );
+    if ( Gia_ObjIsAnd(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{ 
+    Vec_Ptr_t * vFrontier;
+    Gia_Obj_t * pNode, * pFanin;
+    int i, k, fUseMuxes = 1;
+    // quit if CNF is ready
+    if ( CecG_ObjSatNum(p,pObj) )
+        return;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_PtrPush( p->vUsedNodes, pObj );
+        CecG_ObjSetSatNum( p, pObj, p->nSatVars++ );
+        sat_solver_setnvars( p->pSat, p->nSatVars );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    CecG_ObjAddToFrontier( p, pObj, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( CecG_ObjSatNum(p,pNode) );
+        if ( fUseMuxes && Gia_ObjIsMuxType(pNode) )
+        {
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
+            Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
+                CecG_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+            CecG_AddClausesMux( p, pNode );
+        }
+        else
+        {
+            CecG_CollectSuper( pNode, fUseMuxes, p->vFanins );
+            Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
+                CecG_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+            CecG_AddClausesSuper( p, pNode, p->vFanins );
+        }
+        assert( Vec_PtrSize(p->vFanins) > 1 );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CecG_ManSatSolverRecycle( Cec_ManSat_t * p )
+{
+    int Lit;
+    if ( p->pSat )
+    {
+        Gia_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i )
+            CecG_ObjSetSatNum( p, pObj, 0 );
+        Vec_PtrClear( p->vUsedNodes );
+//        memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
+        sat_solver_delete( p->pSat );
+    }
+    p->pSat = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 1000 );
+    p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
+    // var 0 is not used
+    // var 1 is reserved for const0 node - add the clause
+    p->nSatVars = 1;
+//    p->nSatVars = 0;
+    Lit = toLitCond( p->nSatVars, 1 );
+//    if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012)
+//        Lit = lit_neg( Lit );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    CecG_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ );
+
+    p->nRecycles++;
+    p->nCallsSince = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CecG_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pObjR = Gia_Regular(pObj);
+    int nBTLimit = p->pPars->nBTLimit;
+    int Lit, RetValue, status, nConflicts;
+    abctime clk = Abc_Clock();
+
+    if ( pObj == Gia_ManConst0(p->pAig) )
+        return 1;
+    if ( pObj == Gia_ManConst1(p->pAig) )
+    {
+        assert( 0 );
+        return 0;
+    }
+
+    p->nCallsSince++;  // experiment with this!!!
+    p->nSatTotal++;
+    
+    // check if SAT solver needs recycling
+    if ( p->pSat == NULL || 
+        (p->pPars->nSatVarMax && 
+         p->nSatVars > p->pPars->nSatVarMax && 
+         p->nCallsSince > p->pPars->nCallsRecycle) )
+        CecG_ManSatSolverRecycle( p );
+
+    // if the nodes do not have SAT variables, allocate them
+    CecG_CnfNodeAddToSolver( p, pObjR );
+
+    // propage unit clauses
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    Lit = toLitCond( CecG_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pObjR->fPhase )  Lit = lit_neg( Lit );
+    }
+    nConflicts = p->pSat->stats.conflicts;
+
+    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_False )
+    {
+p->timeSatUnsat += Abc_Clock() - clk;
+        Lit = lit_neg( Lit );
+        RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+        assert( RetValue );
+        p->nSatUnsat++;
+        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;       
+//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return 1;
+    }
+    else if ( RetValue == l_True )
+    {
+p->timeSatSat += Abc_Clock() - clk;
+        p->nSatSat++;
+        p->nConfSat += p->pSat->stats.conflicts - nConflicts;
+//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return 0;
+    }
+    else // if ( RetValue == l_Undef )
+    {
+p->timeSatUndec += Abc_Clock() - clk;
+        p->nSatUndec++;
+        p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
+//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return -1;
+    }
+}
+
+void CecG_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Cec_ManSat_t * p;
+    Gia_Obj_t * pObj;
+    int i, status;
+    abctime clk = Abc_Clock(), clk2;
+    Vec_PtrFreeP( &pAig->vSeqModelVec );
+    // reset the manager
+    if ( pPat )
+    {
+        pPat->iStart = Vec_StrSize(pPat->vStorage);
+        pPat->nPats = 0;
+        pPat->nPatLits = 0;
+        pPat->nPatLitsMin = 0;
+    } 
+    Gia_ManSetPhase( pAig );
+    Gia_ManLevelNum( pAig );
+    Gia_ManIncrementTravId( pAig );
+    p = Cec_ManSatCreate( pAig, pPars );
+    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            status = !Gia_ObjFaninC0(pObj);
+            pObj->fMark0 = (status == 0);
+            pObj->fMark1 = (status == 1);
+            continue;
+        }
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
+clk2 = Abc_Clock();
+        status = CecG_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
+        pObj->fMark0 = (status == 0);
+        pObj->fMark1 = (status == 1);
+
+        if ( f0Proved && status == 1 )
+            Gia_ManPatchCoDriver( pAig, i, 0 );
+/*
+        if ( status == -1 )
+        {
+            Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
+            Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0, 0 );
+            Gia_ManStop( pTemp );
+            Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
+        }
+*/
+        if ( status != 0 )
+            continue;
+        // save the pattern
+        if ( pPat )
+        {
+            abctime clk3 = Abc_Clock();
+            Cec_ManPatSavePattern( pPat, p, pObj );
+            pPat->timeTotalSave += Abc_Clock() - clk3;
+        }
+        // quit if one of them is solved
+        if ( pPars->fCheckMiter )
+            break;
+    }
+    p->timeTotal = Abc_Clock() - clk;
+    Bar_ProgressStop( pProgress );
+    if ( pPars->fVerbose )
+        Cec_ManSatPrintStats( p );
+    Cec_ManSatStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make
index fa33ef82..b61bebfa 100644
--- a/src/proof/cec/module.make
+++ b/src/proof/cec/module.make
@@ -11,6 +11,7 @@ SRC +=    src/proof/cec/cecCec.c \
     src/proof/cec/cecSatG2.c \
     src/proof/cec/cecSeq.c \
     src/proof/cec/cecSolve.c \
+    src/proof/cec/cecSolveG.c \
     src/proof/cec/cecSplit.c \
     src/proof/cec/cecSynth.c \
     src/proof/cec/cecSweep.c