Enabling new X-valued simulation in 'pdr'.

10 files changed, 424 insertions, 5 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f578fb77..d6b76966 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -5263,6 +5263,10 @@ SOURCE=.\src\proof\pdr\pdrTsim.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\pdr\pdrTsim2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\pdr\pdrUtil.c
 # End Source File
 # End Group
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7ff404b0..b8a0a301 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26008,7 +26008,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmsipdegoncvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmusipdegoncvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26123,6 +26123,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMonoCnf ^= 1;
             break;
+        case 'u':
+            pPars->fNewXSim ^= 1;
+            break;
         case 's':
             pPars->fShortest ^= 1;
             break;
@@ -26191,7 +26194,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmsipdegoncvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmusipdegoncvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26208,6 +26211,7 @@ usage:
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",              pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n",                    pPars->fMonoCnf? "yes": "no" );
+    Abc_Print( -2, "\t-u     : toggle updated X-valued simulation [default = %s]\n",                         pPars->fNewXSim? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle creating only shortest counter-examples [default = %s]\n",             pPars->fShortest? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle clause pushing from an intermediate timeframe [default = %s]\n",       pPars->fShiftStart? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle reusing proof-obligations in the last timeframe [default = %s]\n",     pPars->fReuseProofOblig? "yes": "no" );
diff --git a/src/proof/pdr/module.make b/src/proof/pdr/module.make
index 5bee83f8..2967aeb8 100644
--- a/src/proof/pdr/module.make
+++ b/src/proof/pdr/module.make
@@ -4,4 +4,5 @@ SRC +=    src/proof/pdr/pdrCnf.c \
     src/proof/pdr/pdrMan.c \
     src/proof/pdr/pdrSat.c \
     src/proof/pdr/pdrTsim.c \
+    src/proof/pdr/pdrTsim2.c \
     src/proof/pdr/pdrUtil.c 
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index b73a54df..9f9ef238 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -52,6 +52,7 @@ struct Pdr_Par_t_
     int nRandomSeed;      // value to seed the SAT solver with
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
+    int fNewXSim;         // updated X-valued simulation
     int fDumpInv;         // dump inductive invariant
     int fUseSupp;         // use support in the invariant
     int fShortest;        // forces bug traces to be shortest
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 71a61c81..38792ef8 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -63,6 +63,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fSkipDown      =       1;  // apply down in generalization
     pPars->fCtgs          =       0;  // handle CTGs in down
     pPars->fMonoCnf       =       0;  // monolythic CNF
+    pPars->fNewXSim       =       0;  // updated X-valued simulation
     pPars->fDumpInv       =       0;  // dump inductive invariant
     pPars->fUseSupp       =       1;  // using support variables in the invariant
     pPars->fShortest      =       0;  // forces bug traces to be shortest
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 9c1e9840..f47c08a9 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -42,6 +42,8 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Txs_Man_t_ Txs_Man_t;
+
 typedef struct Pdr_Set_t_ Pdr_Set_t;
 struct Pdr_Set_t_
 {
@@ -87,6 +89,8 @@ struct Pdr_Man_t_
     int *       pOrder;    // ordering of the lits
     Vec_Int_t * vActVars;  // the counter of activation variables
     int         iUseFrame; // the first used frame
+    // terminary simulation
+    Txs_Man_t * pTxs;      
     // internal use
     Vec_Int_t * vPrio;     // priority flops
     Vec_Int_t * vLits;     // array of literals
@@ -189,6 +193,10 @@ extern int             Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCu
 extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf );
 /*=== pdrTsim.c ==========================================================*/
 extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
+/*=== pdrTsim2.c ==========================================================*/
+extern Txs_Man_t *     Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
+extern void            Txs_ManStop( Txs_Man_t * );
+extern Pdr_Set_t *     Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube );
 /*=== pdrUtil.c ==========================================================*/
 extern Pdr_Set_t *     Pdr_SetAlloc( int nSize );
 extern Pdr_Set_t *     Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index b58c479b..eb12e341 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -70,6 +70,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vSuppLits= Vec_IntAlloc( 100 );  // support literals
     p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
     p->pCnfMan  = Cnf_ManStart();
+    // ternary simulation
+    p->pTxs     = Txs_ManStart( p, pAig, p->vPrio );
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
@@ -150,6 +152,8 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_WecFreeP( &p->vVLits );
     // CNF manager
     Cnf_ManStop( p->pCnfMan );
+    // terminary simulation
+    Txs_ManStop( p->pTxs );
     // internal use
     Vec_IntFreeP( &p->vPrio   );  // priority flops
     Vec_IntFree( p->vLits     );  // array of literals
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index eb94a826..49b0448a 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -377,7 +377,14 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         p->tSatSat += clk;
         p->nCallsS++;
         if ( ppPred )
-            *ppPred = Pdr_ManTernarySim( p, k, pCube );
+        {
+            abctime clk = Abc_Clock();
+            if ( p->pPars->fNewXSim )
+                *ppPred = Txs_ManTernarySim( p->pTxs, k, pCube );
+            else
+                *ppPred = Pdr_ManTernarySim( p, k, pCube );
+            p->tTsim += Abc_Clock() - clk;
+        }
         RetValue = 0;
     }
 
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 37f84667..43f2ddb0 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -364,7 +364,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
     Aig_Obj_t * pObj;
     int i, Entry, RetValue;
-    abctime clk = Abc_Clock();
+    //abctime clk = Abc_Clock();
 
     // collect CO objects
     Vec_IntClear( vCoObjs );
@@ -474,7 +474,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     // derive the set of resulting registers
     Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
     assert( Vec_IntSize(vRes) > 0 );
-    p->tTsim += Abc_Clock() - clk;
+    //p->tTsim += Abc_Clock() - clk;
     pRes = Pdr_SetCreate( vRes, vPiLits );
     //ZH: Disabled assertion because this invariant doesn't hold with down
     //because of the join operation which can bring in initial states
diff --git a/src/proof/pdr/pdrTsim2.c b/src/proof/pdr/pdrTsim2.c
new file mode 100644
index 00000000..82e9a56c
--- /dev/null
+++ b/src/proof/pdr/pdrTsim2.c
@@ -0,0 +1,389 @@
+/**CFile****************************************************************
+
+  FileName    [pdrTsim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Property driven reachability.]
+
+  Synopsis    [Improved ternary simulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 20, 2010.]
+
+  Revision    [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Txs_Man_t_
+{
+    Gia_Man_t * pGia;      // user's AIG
+    Vec_Int_t * vPrio;     // priority of each flop
+    Vec_Int_t * vCiObjs;   // cone leaves (CI obj IDs)
+    Vec_Int_t * vCoObjs;   // cone roots (CO obj IDs)
+    Vec_Int_t * vCiVals;   // cone leaf values (0/1 CI values)
+    Vec_Int_t * vCoVals;   // cone root values (0/1 CO values)
+    Vec_Int_t * vNodes;    // cone nodes (node obj IDs)
+    Vec_Int_t * vPiLits;   // resulting array of PI literals
+    Vec_Int_t * vFfLits;   // resulting array of flop literals
+    Pdr_Man_t * pMan;      // calling manager
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start and stop the ternary simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
+{
+    Txs_Man_t * p;
+//    Aig_Obj_t * pObj;
+//    int i;
+    assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
+    p = ABC_CALLOC( Txs_Man_t, 1 );
+    p->pGia    = Gia_ManFromAigSimple(pAig); // user's AIG
+//    Aig_ManForEachObj( pAig, pObj, i )
+//        assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
+    p->vPrio   = vPrio;                // priority of each flop
+    p->vCiObjs = Vec_IntAlloc( 100 );  // cone leaves (CI obj IDs)
+    p->vCoObjs = Vec_IntAlloc( 100 );  // cone roots (CO obj IDs)
+    p->vCiVals = Vec_IntAlloc( 100 );  // cone leaf values (0/1 CI values)
+    p->vCoVals = Vec_IntAlloc( 100 );  // cone root values (0/1 CO values)
+    p->vNodes  = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
+    p->vPiLits = Vec_IntAlloc( 100 );  // resulting array of PI literals
+    p->vFfLits = Vec_IntAlloc( 100 );  // resulting array of flop literals
+    p->pMan    = pMan;                 // calling manager
+    return p;
+}
+void Txs_ManStop( Txs_Man_t * p )
+{
+    Gia_ManStop( p->pGia );
+    Vec_IntFree( p->vCiObjs );
+    Vec_IntFree( p->vCoObjs );
+    Vec_IntFree( p->vCiVals );
+    Vec_IntFree( p->vCoVals );
+    Vec_IntFree( p->vNodes );
+    Vec_IntFree( p->vPiLits );
+    Vec_IntFree( p->vFfLits );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone and collects CIs and nodes.]
+
+  Description [For this procedure to work Value should not be ~0 
+  at the beginning.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Txs_ManCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+    if ( !~pObj->Value )
+        return;
+    pObj->Value = ~0;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vCiObjs, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
+    Txs_ManCollectCone_rec( p, Gia_ObjFanin1(pObj), vCiObjs, vNodes );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+void Txs_ManCollectCone( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+    Gia_Obj_t * pObj; int i;
+//    printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
+    Vec_IntClear( vCiObjs );
+    Vec_IntClear( vNodes );
+    Gia_ManConst0(p)->Value = ~0;
+    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+        Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate values and assign priority.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Txs_ManForwardPass( Gia_Man_t * p, 
+                         Vec_Int_t * vPrio, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, 
+                         Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
+{
+    Gia_Obj_t * pObj, * pFan0, * pFan1; int i;
+    pObj = Gia_ManConst0(p);
+    pObj->fMark0 = 0;
+    pObj->fMark1 = 0;
+    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+    {
+        pObj->fMark0 = Vec_IntEntry(vCiVals, i);
+        pObj->fMark1 = 0;
+        pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Vec_IntEntry(vPrio, Gia_ObjCioId(pObj)-Gia_ManPiNum(p));
+        assert( ~pObj->Value );
+    }
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+    {
+        pFan0 = Gia_ObjFanin0(pObj);
+        pFan1 = Gia_ObjFanin1(pObj);
+        pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj)) & (pFan1->fMark0 ^ Gia_ObjFaninC1(pObj));
+        pObj->fMark1 = 0;
+        if ( pObj->fMark0 )
+            pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
+        else if ( pFan0->fMark0 )
+            pObj->Value = pFan1->Value;
+        else if ( pFan1->fMark0 )
+            pObj->Value = pFan0->Value;
+        else // if ( pFan0->fMark0 == 0 && pFan1->fMark0 == 0 )
+            pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
+        assert( ~pObj->Value );
+    }
+    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+    {
+        pFan0 = Gia_ObjFanin0(pObj);
+        pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj));
+        pFan0->fMark1 = 1;
+        assert( (int)pObj->fMark0 == Vec_IntEntry(vCoVals, i) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate requirements and collect results.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Txs_ObjIsJust( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
+    Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
+    int value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+    int value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( pObj->fMark0 )
+        return pFan0->fMark1 && pFan1->fMark1;
+    assert( !pObj->fMark0 );
+    assert( !value0 || !value1 );
+    if ( value0 )
+        return pFan1->fMark1;
+    if ( value1 )
+        return pFan0->fMark1;
+    assert( !value0 && !value1 );
+    return pFan0->fMark1 || pFan1->fMark1 || Gia_ObjIsPi(p, pFan0) || Gia_ObjIsPi(p, pFan1);
+}
+void Txs_ManBackwardPass( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits )
+{
+    Gia_Obj_t * pObj, * pFan0, * pFan1; int i, value0, value1;
+    Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
+    {
+        if ( !pObj->fMark1 )
+            continue;
+        pFan0 = Gia_ObjFanin0(pObj);
+        pFan1 = Gia_ObjFanin1(pObj);
+        if ( pObj->fMark0 )
+        {
+            pFan0->fMark1 = 1;
+            pFan1->fMark1 = 1;
+            continue;
+        }
+        value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+        value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+        assert( !value0 || !value1 );
+        if ( value0 )
+            pFan1->fMark1 = 1;
+        else if ( value1 )
+            pFan0->fMark1 = 1;
+        else // if ( !value0 && !value1 )
+        {
+            if ( pFan0->fMark1 || pFan1->fMark1 )
+                continue;
+            if ( Gia_ObjIsPi(p, pFan0) )
+                pFan0->fMark1 = 1;
+            else if ( Gia_ObjIsPi(p, pFan1) )
+                pFan1->fMark1 = 1;
+            else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
+                pFan0->fMark1 = 1;
+            else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
+                pFan1->fMark1 = 1;
+            else
+            {
+                if ( pFan0->Value >= pFan1->Value )
+                    pFan0->fMark1 = 1;
+                else
+                    pFan1->fMark1 = 1;
+            }
+        }
+    }
+    Vec_IntClear( vPiLits );
+    Vec_IntClear( vFfLits );
+    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+    {
+        if ( !pObj->fMark1 )
+            continue;
+        if ( Gia_ObjIsPi(p, pObj) )
+            Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj),                 !pObj->fMark0) );
+        else
+            Vec_IntPush( vFfLits, Abc_Var2Lit(Gia_ObjCioId(pObj)-Gia_ManPiNum(p), !pObj->fMark0) );
+    }
+    assert( Vec_IntSize(vFfLits) > 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify the result.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Txs_ManVerify( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
+{
+    Gia_Obj_t * pObj;
+    int i, iLit;
+    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+        Gia_ObjTerSimSetX( pObj );
+    Vec_IntForEachEntry( vPiLits, iLit, i )
+    {
+        pObj = Gia_ManPi( p, Abc_Lit2Var(iLit) );
+        assert( Gia_ObjTerSimGetX(pObj) );
+        if ( Abc_LitIsCompl(iLit) )
+            Gia_ObjTerSimSet0( pObj );
+        else
+            Gia_ObjTerSimSet1( pObj );
+    }
+    Vec_IntForEachEntry( vFfLits, iLit, i )
+    {
+        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Abc_Lit2Var(iLit) );
+        assert( Gia_ObjTerSimGetX(pObj) );
+        if ( Abc_LitIsCompl(iLit) )
+            Gia_ObjTerSimSet0( pObj );
+        else
+            Gia_ObjTerSimSet1( pObj );
+    }
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+        Gia_ObjTerSimAnd( pObj );
+    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+    {
+        Gia_ObjTerSimCo( pObj );
+        if ( Vec_IntEntry(vCoVals, i) )
+            assert( Gia_ObjTerSimGet1(pObj) );
+        else
+            assert( Gia_ObjTerSimGet0(pObj) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinks values using ternary simulation.]
+
+  Description [The cube contains the set of flop index literals which,
+  when converted into a clause and applied to the combinational outputs, 
+  led to a satisfiable SAT run in frame k (values stored in the SAT solver).
+  If the cube is NULL, it is assumed that the first property output was
+  asserted and failed.
+  The resulting array is a set of flop index literals that asserts the COs.
+  Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+    Pdr_Set_t * pRes;
+    Gia_Obj_t * pObj;
+    // collect CO objects
+    Vec_IntClear( p->vCoObjs );
+    if ( pCube == NULL ) // the target is the property output
+    {
+        pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
+        Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
+    }
+    else // the target is the cube
+    {
+        int i;
+        for ( i = 0; i < pCube->nLits; i++ )
+        {
+            if ( pCube->Lits[i] == -1 )
+                continue;
+            pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
+            Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
+        }
+    }
+if ( 0 )
+{
+Abc_Print( 1, "Trying to justify cube " );
+if ( pCube )
+    Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
+else
+    Abc_Print( 1, "<prop=fail>" );
+Abc_Print( 1, " in frame %d.\n", k );
+}
+
+    // collect CI objects
+    Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
+    // collect values
+    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
+    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
+
+    // perform two passes
+    Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
+    Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
+    Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
+
+    // derive the final set
+    pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
+    //ZH: Disabled assertion because this invariant doesn't hold with down
+    //because of the join operation which can bring in initial states
+    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+    return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END