SAT sweeping under constraints (bug fix).

5 files changed, 16 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 48f0c215..ed38806e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -891,7 +891,7 @@ extern int                 Gia_ManEquivCountLitsAll( Gia_Man_t * p );
 extern int                 Gia_ManEquivCountClasses( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
-extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
+extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose );
 extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 3067f956..d795856a 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -414,7 +414,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
@@ -445,7 +445,8 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
         return NULL;
     }
 */
-    Gia_ManSetPhase( p );
+    if ( !fSkipPhase )
+        Gia_ManSetPhase( p );
     if ( fDualOut )
         Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
@@ -637,7 +638,7 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
 {
     Gia_Man_t * pNew, * pFinal;
-    pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
+    pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
     if ( pNew == NULL )
         return NULL;
     if ( fMiterPairs )
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 994aedc1..4517bb7b 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -288,7 +288,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
     if ( p->pManTime == NULL )
     {
         Gia_ManFraigSweepPerform( p, pPars );
-        pNew = Gia_ManEquivReduce( p, 1, 0, 0 );
+        pNew = Gia_ManEquivReduce( p, 1, 0, 0, 0 );
         if ( pNew == NULL )
             return Gia_ManDup(p);
         return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d7e36cfa..ec8e9e76 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27365,7 +27365,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( fSynthesis )
     {
-        pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, fVerbose );
+        pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, 0, fVerbose );
         if ( pTemp )
         {
             pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
@@ -27612,7 +27612,7 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( fUseAll )
     {
-        pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, fVerbose );
+        pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, 0, fVerbose );
         pTemp = Gia_ManSeqStructSweep( pTemp2 = pTemp, 1, 1, 0 );
         Gia_ManStop( pTemp2 );
     }
@@ -31601,7 +31601,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Gia_Man_t * pTemp = NULL;
+    Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int fSwitch = 0;
 //    extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
@@ -31614,9 +31614,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //     extern void Unr_ManTest( Gia_Man_t * pGia );
 //    extern void Mig_ManTest( Gia_Man_t * pGia );
 //    extern int Gia_ManVerify( Gia_Man_t * pGia );
-//    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
 //    extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
 //    extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
+    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -31668,10 +31668,10 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Unr_ManTest( pAbc->pGia );
 //    Mig_ManTest( pAbc->pGia );
 //    Gia_ManVerifyWithBoxes( pAbc->pGia );
-//    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
-//    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
-//    Abc_FrameUpdateGia( pAbc, pTemp );
 //    Gia_ManCollectSeqTest( pAbc->pGia );
+//    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
+    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 43d0e250..1a57a47c 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -298,6 +298,7 @@ clk = clock();
         {
             p->nSatCallsUnsat++;
             pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
+            Gia_ObjSetProved( pAig, i );
         }
         else if ( status == l_True )
         {
@@ -329,9 +330,10 @@ clk = clock();
 p->timeSimSat += clock() - clk;
     }
 //    Gia_ManEquivPrintClasses( pAig, 1, 0 );
+//    Gia_ManPrint( pAig );
 
     // generate the resulting AIG
-    pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
+    pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
     if ( pResult == NULL )
     {
         printf( "There is no equivalences.\n" );