Adding switch 'scorr -f' to dump inductive invariant as an AIG.

3 files changed, 18 insertions, 9 deletions

diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index cd65fc67..9bd83964 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -70,6 +70,7 @@ struct Ssw_Pars_t_
     int              fVerbose;      // verbose stats
     int              fFlopVerbose;  // verbose printout of redundant flops
     int              fEquivDump;    // enables dumping equivalences
+    int              fEquivDump2;   // enables dumping equivalences
     int              fStopWhenGone; // stop when PO output is not a candidate constant
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index 5ef6e71e..58c01b21 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fLocalSim      =       0;  // local simulation
     p->fVerbose       =       0;  // verbose stats
     p->fEquivDump     =       0;  // enables dumping equivalences
+    p->fEquivDump2    =       0;  // enables dumping equivalences
 
     // latch correspondence
     p->fLatchCorrOpt  =       0;  // performs optimized register correspondence
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index 77cb24de..2687e9c1 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -220,9 +220,14 @@ p->timeMarkCones += Abc_Clock() - clk;
     {
         pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
         Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
+        if ( p->pPars->fEquivDump2 && vPairs )
+        {
+            Vec_IntPush( vPairs, pObjRepr->Id );
+            Vec_IntPush( vPairs, pObj->Id );
+        }
         return 0;
     }
-    if ( vPairs )
+    if ( p->pPars->fEquivDump && vPairs )
     {
         Vec_IntPush( vPairs, pObjRepr->Id );
         Vec_IntPush( vPairs, pObj->Id );
@@ -334,7 +339,7 @@ p->timeBmc += Abc_Clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
+void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num, int fAddOuts )
 {
     FILE * pFile;
     char pBuffer[16];
@@ -347,7 +352,7 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
         return;
     }
     fclose( pFile );
-    pNew = Saig_ManCreateEquivMiter( p, vPairs );
+    pNew = Saig_ManCreateEquivMiter( p, vPairs, fAddOuts );
     Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
     Aig_ManStop( pNew );
     Abc_Print( 1, "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
@@ -372,7 +377,7 @@ int Ssw_ManSweep( Ssw_Man_t * p )
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
     int nConstrPairs, i, f;
     abctime clk;
-    Vec_Int_t * vDisproved;
+    Vec_Int_t * vObjPairs;
 
     // perform speculative reduction
 clk = Abc_Clock();
@@ -407,18 +412,18 @@ p->timeReduce += Abc_Clock() - clk;
     Ssw_ClassesClearRefined( p->ppClasses );
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
-    vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL;
+    vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )
-            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs );
         else if ( Aig_ObjIsNode(pObj) )
         {
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
-            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs );
         }
     }
     if ( p->pPars->fVerbose )
@@ -427,8 +432,10 @@ p->timeReduce += Abc_Clock() - clk;
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
     if ( p->pPars->fEquivDump )
-        Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ );
-    Vec_IntFreeP( &vDisproved );
+        Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, Counter++, 1 );
+    if ( p->pPars->fEquivDump2 && !p->fRefined )
+        Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, 0, 0 );
+    Vec_IntFreeP( &vObjPairs );
     return p->fRefined;
 }