Enabling circuit solver in &fraig.

6 files changed, 100 insertions, 13 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dff328eb..6ca352cd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28931,7 +28931,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ManFraSetDefaultParams( pPars );
     pPars->fSatSweeping = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29010,6 +29010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDualOut ^= 1;
             break;
+        case 'c':
+            pPars->fRunCSat ^= 1;
+            break;
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
@@ -29030,7 +29033,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
@@ -29041,6 +29044,7 @@ usage:
     Abc_Print( -2, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-d     : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 65d2e24e..2e69f7a4 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -107,6 +107,7 @@ struct Cec_ParFra_t_
     int              fDualOut;      // miter with separate outputs
     int              fColorDiff;    // miter with separate outputs
     int              fSatSweeping;  // enable SAT sweeping
+    int              fRunCSat;      // enable another solver
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the failed output
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c77b8fa1..71335e85 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -426,7 +426,10 @@ p->timeSim += Abc_Clock() - clk;
             break;
         }
 clk = Abc_Clock();
-        Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
+        if ( pPars->fRunCSat )
+            Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); 
+        else
+            Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
 p->timeSat += Abc_Clock() - clk;
         if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
         {
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index dd6dc618..ef1dd983 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -190,6 +190,7 @@ extern Cec_ManFra_t *       Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t *  p
 extern void                 Cec_ManFraStop( Cec_ManFra_t * p );
 /*=== cecPat.c ============================================================*/
 extern void                 Cec_ManPatSavePattern( Cec_ManPat_t *  pPat, Cec_ManSat_t *  p, Gia_Obj_t * pObj );
+extern void                 Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat );
 extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWords );
 extern Vec_Ptr_t *          Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
 /*=== cecSeq.c ============================================================*/
@@ -201,6 +202,7 @@ extern int                  Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void                 Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
 extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
 extern int                  Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c
index c175eaa7..91a0c941 100644
--- a/src/proof/cec/cecPat.c
+++ b/src/proof/cec/cecPat.c
@@ -360,20 +360,21 @@ void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t *  p, Gia_Obj_t *
 {
     Vec_Int_t * vPat;
     int nPatLits;
-    abctime clk, clkTotal = Abc_Clock();
+    abctime clkTotal = Abc_Clock();
+//    abctime clk;
     assert( Gia_ObjIsCo(pObj) );
     pMan->nPats++;
     pMan->nPatsAll++;
     // compute values in the cone of influence
-clk = Abc_Clock();
+//clk = Abc_Clock();
     Gia_ManIncrementTravId( p->pAig );
     nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
     assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
     pMan->nPatLits += nPatLits;
     pMan->nPatLitsAll += nPatLits;
-pMan->timeFind += Abc_Clock() - clk;
+//pMan->timeFind += Abc_Clock() - clk;
     // compute sensitizing path
-clk = Abc_Clock();
+//clk = Abc_Clock();
     Vec_IntClear( pMan->vPattern1 );
     Gia_ManIncrementTravId( p->pAig );
     Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
@@ -385,19 +386,26 @@ clk = Abc_Clock();
     vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
     pMan->nPatLitsMin += Vec_IntSize(vPat);
     pMan->nPatLitsMinAll += Vec_IntSize(vPat);
-pMan->timeShrink += Abc_Clock() - clk;
+//pMan->timeShrink += Abc_Clock() - clk;
     // verify pattern using ternary simulation
-clk = Abc_Clock();
-    Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
-pMan->timeVerify += Abc_Clock() - clk;
+//clk = Abc_Clock();
+//    Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
+//pMan->timeVerify += Abc_Clock() - clk;
     // sort pattern
-clk = Abc_Clock();
+//clk = Abc_Clock();
     Vec_IntSort( vPat, 0 );
-pMan->timeSort += Abc_Clock() - clk;
+//pMan->timeSort += Abc_Clock() - clk;
     // save pattern
     Cec_ManPatStore( pMan, vPat );
     pMan->timeTotal += Abc_Clock() - clkTotal;
 }
+void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat )
+{
+    // sort pattern
+    Vec_IntSort( vPat, 0 );
+    // save pattern
+    Cec_ManPatStore( pMan, vPat );
+}
 
 /**Function*************************************************************
 
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index c799d17d..e3db0b93 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -735,6 +735,75 @@ clk2 = Abc_Clock();
     Cec_ManSatStop( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of solving for the POs of the AIG.]
+
+  Description [Labels the nodes that have been proved (pObj->fMark1) 
+  and returns the set of satisfying assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat )
+{
+    int k, nSize;
+    Vec_IntClear( vPat );
+    // skip the output number
+    iStart++;
+    // get the number of items
+    nSize = Vec_IntEntry( vCexStore, iStart++ );
+    if ( nSize <= 0 )
+        return iStart;
+    // extract pattern
+    for ( k = 0; k < nSize; k++ )
+        Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
+    return iStart;
+}
+void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+{
+    Vec_Str_t * vStatus;
+    Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
+    Gia_Obj_t * pObj;
+    int i, status, iStart = 0;
+    assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
+    // reset the manager
+    if ( pPat )
+    {
+        pPat->iStart = Vec_StrSize(pPat->vStorage);
+        pPat->nPats = 0;
+        pPat->nPatLits = 0;
+        pPat->nPatLitsMin = 0;
+    } 
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        status = (int)Vec_StrEntry(vStatus, i);
+        pObj->fMark0 = (status == 0);
+        pObj->fMark1 = (status == 1);
+        if ( Vec_IntSize(vCexStore) > 0 && status != 1 )
+            iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat );
+        if ( status != 0 )
+            continue;
+        // save the pattern
+        if ( pPat && Vec_IntSize(vPat) > 0 )
+        {
+            abctime clk3 = Abc_Clock();
+            Cec_ManPatSavePatternCSat( pPat, vPat );
+            pPat->timeTotalSave += Abc_Clock() - clk3;
+        }
+        // quit if one of them is solved
+        if ( pPars->fCheckMiter )
+            break;
+    }
+    assert( iStart == Vec_IntSize(vCexStore) );
+    Vec_IntFree( vPat );
+    Vec_StrFree( vStatus );
+    Vec_IntFree( vCexStore );
+}
+
 
 
 /**Function*************************************************************