Sweeper condition complement bug-fix and code for internal verification.

8 files changed, 60 insertions, 12 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 9e82939d..c3e0d033 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1007,7 +1007,8 @@ extern Gia_Man_t *         Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fVerbose );
+extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
+extern Gia_Man_t *         Gia_ManDupAnd( Gia_Man_t * p, int fCompl );
 extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 30f9140d..92076573 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1880,7 +1880,7 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fVerbose )
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -1951,7 +1951,12 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
                 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
                 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
             }
-            else
+            else if ( fImplic )
+            {
+                iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
+                Gia_ManAppendCo( pNew, iLit );
+            }
+            else 
             {
                 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
                 Gia_ManAppendCo( pNew, iLit );
@@ -1990,6 +1995,11 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
                 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
                 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
             }
+            else if ( fImplic )
+            {
+                iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
+                Gia_ManAppendCo( pNew, iLit );
+            }
             else
             {
                 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
@@ -2008,6 +2018,22 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the AND of all POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl )
+{
+    return NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms the circuit into a regular miter.]
 
   Description []
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 13443414..c5dba25b 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1882,7 +1882,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
         Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
         return 0;
     }
-    pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
+    pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
     if ( pMiter == NULL )
     {
         Gia_ManStop( pGia1 );
@@ -2021,7 +2021,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
         Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
         return 0;
     }
-    pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
+    pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
     if ( pMiter == NULL )
     {
         Gia_ManStop( pGia1 );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 4cad0bdc..838b9978 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -784,7 +784,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
     {
         iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
         Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
-        Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) );
+        Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
     }
     Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
     Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
@@ -969,6 +969,27 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
 
 /**Function*************************************************************
 
+  Synopsis    [Verification of the sweeper.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
+{
+    Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
+    Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 );
+
+    Gia_ManStop( pConstr );
+    Gia_ManStop( pMiter );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs conditional sweeping of the cone.]
 
   Description [Returns the result as a new GIA manager with as many inputs 
@@ -995,7 +1016,7 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords,
     pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
     pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
     Gia_ManSetPhase( pGiaOuts );
-    // if there is no conditions, define constant true constrain (constant 0 output)
+    // if there is no conditions, define constant true constraint (constant 0 output)
     if ( Gia_ManPoNum(pGiaCond) == 0 )
         Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
     // perform sweeping under constraints
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 16d09445..ea5ec003 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -554,7 +554,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
     pGia1 = Gia_ManDupCollapse( pGia,  pGia->pAigExtra,  NULL  );
     Vec_IntFreeP( &vBoxPres );
     // compute the miter
-    pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, fVerbose );
+    pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
     if ( pMiter )
     {
         Cec_ParCec_t ParsCec, * pPars = &ParsCec;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0681f28e..e37944cf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27966,7 +27966,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // compute the miter
-    pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, fVerbose );
+    pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, 0, fVerbose );
     Gia_ManStop( pSecond );
     Abc_FrameUpdateGia( pAbc, pAux );
     return 0;
@@ -29352,7 +29352,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // compute the miter
-    pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
+    pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, 0, pPars->fVerbose );
     if ( pMiter )
     {
         if ( fDumpMiter )
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 1d4c83b6..f3b1a3b0 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -301,7 +301,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
     int RetValue;
     Cec_ManCecSetDefaultParams( pPars );
     pPars->fVerbose = fVerbose;
-    pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, pPars->fVerbose );
+    pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, 0, pPars->fVerbose );
     if ( pMiter == NULL )
         return -1;
     RetValue = Cec_ManVerify( pMiter, pPars );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index e388db04..4376c336 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -206,7 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
 
     // create miter
     pTemp = Gia_ManDup( p );
-    pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
+    pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
     Gia_ManStop( pTemp );
     assert( Gia_ManPoNum(pMiter)  == 2 * Gia_ManPoNum(p) );
     assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );