Experiments with SAT sweeping.

4 files changed, 15 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 55e14545..f9f2f2e0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12385,7 +12385,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cba_PrsReadBlifTest();
     }
 //    Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
-    Acb_DataReadTest();
+//    Acb_DataReadTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -32928,7 +32928,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, "WRILDCrmdcnwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcknwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -33010,6 +33010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fRunCSat ^= 1;
             break;
+        case 'k':
+            pPars->fUseCones ^= 1;
+            break;
         case 'n':
             fUseAlgo ^= 1;
             break;
@@ -33036,7 +33039,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcnwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcknwvh]\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 );
@@ -33048,6 +33051,7 @@ usage:
     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-k     : toggle using logic cones in the SAT solver [default = %s]\n", pPars->fUseCones? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggle using new implementation [default = %s]\n", fUseAlgo? "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" );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index e8b243d3..cb4ff27f 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -108,6 +108,7 @@ struct Cec_ParFra_t_
     int              fColorDiff;    // miter with separate outputs
     int              fSatSweeping;  // enable SAT sweeping
     int              fRunCSat;      // enable another solver
+    int              fUseCones;     // use cones
     int              fUseOrigIds;   // enable recording of original IDs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index ed5c4ab7..ccc5a8e6 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -138,6 +138,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->fDualOut       =       0;  // miter with separate outputs
     p->fColorDiff     =       0;  // miter with separate outputs
     p->fSatSweeping   =       0;  // enable SAT sweeping
+    p->fUseCones      =       0;  // use cones
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
     p->iOutFail       =      -1;  // the failed output
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index fc53d503..c32ed7f9 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -101,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p )
     p->nItersMax      =      10;    // max number of iterations
     p->nConfLimit     =    1000;    // conflict limit at a node
     p->fIsMiter       =       0;    // this is a miter
-    p->fUseCones      =       0;    // use logic cones
+    p->fUseCones      =       1;    // use logic cones
     p->fVeryVerbose   =       0;    // verbose stats
     p->fVerbose       =       0;    // verbose stats
 }  
@@ -968,7 +968,11 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
                 continue;
             }
             if ( Cec2_ManSweepNode(pMan, i) )
+            {
+                if ( Gia_ObjProved(p, i) )
+                    pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
                 continue;
+            }
             pObj->Value = ~0;
             Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) );
             fDisproved = 1;
@@ -1011,6 +1015,7 @@ Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 )
 //    pPars->nSimRounds = pPars0->nRounds;    // simulation rounds
 //    pPars->nItersMax  = pPars0->nItersMax;  // max number of iterations
     pPars->nConfLimit = pPars0->nBTLimit;   // conflict limit at a node
+    pPars->fUseCones  = pPars0->fUseCones;
     pPars->fVerbose   = pPars0->fVerbose;
 //    Gia_ManComputeGiaEquivs( p, 100000, 0 );
 //    Gia_ManEquivPrintClasses( p, 1, 0 );