Improvements to quantification.

2 files changed, 80 insertions, 0 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 591dd419..9acbbe48 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -514,6 +514,7 @@ static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              {
 static inline int          Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj )  { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; }
 static inline int          Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; }
 
+static inline int          Gia_ManPoIsConst( Gia_Man_t * p, int iPoIndex )     { return Gia_ObjFaninId0p(p, Gia_ManPo(p, iPoIndex)) == 0;                   }
 static inline int          Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex )    { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
 static inline int          Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex )    { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
 
@@ -1237,6 +1238,8 @@ extern Gia_Man_t *         Gia_ManDupExist( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupUniv( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern Gia_Man_t *         Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds );
+extern int                 Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds );
 extern Gia_Man_t *         Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 96ddebd8..1d4f7a22 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1878,6 +1878,83 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates logic cone of the literal and inserts it back.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupConeSupp_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs )
+{
+    int iLit0, iLit1, iObj = Gia_ObjId( p, pObj );
+    int iLit = Gia_ObjCopyArray( p, iObj );
+    if ( iLit >= 0 )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin0(pObj), vObjs );
+    Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin1(pObj), vObjs );
+    iLit0 = Gia_ObjCopyArray( p, Gia_ObjFaninId0(pObj, iObj) );
+    iLit1 = Gia_ObjCopyArray( p, Gia_ObjFaninId1(pObj, iObj) );
+    iLit0 = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) );
+    iLit1 = Abc_LitNotCond( iLit1, Gia_ObjFaninC1(pObj) );
+    iLit  = Gia_ManAppendAnd( pNew, iLit0, iLit1 );
+    Gia_ObjSetCopyArray( p, iObj, iLit );
+    Vec_IntPush( vObjs, iObj );
+}
+Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds )
+{
+    Gia_Man_t * pNew; int i, iLit0;
+    Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+    Vec_Int_t * vObjs = Vec_IntAlloc( 1000 );
+    assert( Gia_ObjIsAnd(pRoot) );
+    if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
+        Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManForEachCiVec( vCiIds, p, pObj, i )
+        Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
+    Gia_ManDupConeSupp_rec( pNew, p, pRoot, vObjs );
+    iLit0 = Gia_ObjCopyArray( p, Abc_Lit2Var(iLit) );
+    iLit0 = Abc_LitNotCond( iLit0, Abc_LitIsCompl(iLit) );
+    Gia_ManAppendCo( pNew, iLit0 );
+    Gia_ManForEachCiVec( vCiIds, p, pObj, i )
+        Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 );
+    Gia_ManForEachObjVec( vObjs, p, pObj, i )
+        Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 );
+    Vec_IntFree( vObjs );
+    //assert( Vec_IntCountLarger(&p->vCopies, -1) == 0 );
+    return pNew;
+}
+void Gia_ManDupConeBack_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+//    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+int Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds )
+{
+    Gia_Obj_t * pObj, * pRoot; int i;
+    assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCiIds) );
+    Gia_ManFillValue(pNew);
+    Gia_ManConst0(pNew)->Value = 0;
+    Gia_ManForEachCi( pNew, pObj, i )
+        pObj->Value = Gia_Obj2Lit( p, Gia_ManCi(p, Vec_IntEntry(vCiIds, i)) );
+    pRoot = Gia_ManCo(pNew, 0);
+    Gia_ManDupConeBack_rec( p, pNew, Gia_ObjFanin0(pRoot) );
+    return Gia_ObjFanin0Copy(pRoot);
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
 
   Description []