From 37fd73cf9edb946e19b537ae94d8256f64db243e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 30 Mar 2014 14:10:12 -0700
Subject: Adding new code to verify invariant derived by 'pdr'.

---
 src/proof/pdr/pdrInv.c | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++
 src/proof/pdr/pdrMan.c |  2 +-
 src/sat/bmc/bmcBmc3.c  |  6 ++--
 3 files changed, 87 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 45bc3c35..1b97941d 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -218,6 +218,87 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+void Pdr_SetPrintOne( Pdr_Set_t * p )
+{
+    int i;
+    printf( "Clause: {" );
+    for ( i = 0; i < p->nLits; i++ )
+        printf( " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Aig_Man_t * Pdr_ManDupAigWithClauses( Aig_Man_t * p, Vec_Ptr_t * vCubes )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew, * pLit;
+    Pdr_Set_t * pCube;
+    int i, n;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachCi( p, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pNew );
+    // create outputs for each cube
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+//        Pdr_SetPrintOne( pCube );
+        pObjNew = Aig_ManConst1(pNew);
+        for ( n = 0; n < pCube->nLits; n++ )
+        {
+            assert( Abc_Lit2Var(pCube->Lits[n]) < Saig_ManRegNum(p) );
+            pLit = Aig_NotCond( Aig_ManCi(pNew, Saig_ManPiNum(p) + Abc_Lit2Var(pCube->Lits[n])), Abc_LitIsCompl(pCube->Lits[n]) );
+            pObjNew = Aig_And( pNew, pObjNew, pLit );
+        }
+        Aig_ObjCreateCo( pNew, pObjNew );
+    }
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the POs
+    Saig_ManForEachLi( p, pObj, i )
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
+    return pNew;
+}
+void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes )
+{
+    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+    Aig_Man_t * pNew = Pdr_ManDupAigWithClauses( p, vCubes );
+    Ioa_WriteAiger( pNew, "aig_with_clauses.aig", 0, 0 );
+    Aig_ManStop( pNew );
+    printf( "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" );
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -249,6 +330,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+//    Pdr_ManDumpAig( p->pAig, vCubes );
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index ec20b8a9..9a73b697 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -54,7 +54,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
     p->vActVars = Vec_IntAlloc( 256 );
     if ( !p->pPars->fMonoCnf )
-        p->vVLits   = Vec_WecStart( Abc_MaxInt(1, Aig_ManLevels(pAig)) );
+        p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
     // internal use
     p->vPrio    = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) );  // priority flops
     p->vLits    = Vec_IntAlloc( 100 );  // array of literals
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 3a84e496..3a27d54c 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1663,11 +1663,13 @@ nTimeSat += clkSatRun;
                     if ( !pPars->fNotVerbose )
                         Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                             nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
-                    // set the output number
-                    pCexNew0->iPo = k;
                     // report to the bridge
                     if ( p->pPars->fUseBridge )
+                    {
+                        // set the output number
+                        pCexNew0->iPo = k;
                         Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
+                    }
                     // remember solved output
                     Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
                 }
-- 
cgit v1.2.3