Improvements to ternary simulation.

5 files changed, 375 insertions, 8 deletions

diff --git a/src/proof/pdr/module.make b/src/proof/pdr/module.make
index 1dee93aa..badff981 100644
--- a/src/proof/pdr/module.make
+++ b/src/proof/pdr/module.make
@@ -6,4 +6,5 @@ SRC +=    src/proof/pdr/pdrCnf.c \
     src/proof/pdr/pdrSat.c \
     src/proof/pdr/pdrTsim.c \
     src/proof/pdr/pdrTsim2.c \
+    src/proof/pdr/pdrTsim3.c \
     src/proof/pdr/pdrUtil.c
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index e5b04339..2a8ab023 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -43,7 +43,8 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Txs_Man_t_ Txs_Man_t;
+typedef struct Txs_Man_t_  Txs_Man_t;
+typedef struct Txs3_Man_t_ Txs3_Man_t;
 
 typedef struct Pdr_Set_t_ Pdr_Set_t;
 struct Pdr_Set_t_
@@ -99,7 +100,7 @@ struct Pdr_Man_t_
     int         nCexes;
     int         nCexesTotal;
     // terminary simulation
-    Txs_Man_t * pTxs;      
+    Txs3_Man_t * pTxs3;      
     // internal use
     Vec_Int_t * vPrio;     // priority flops
     Vec_Int_t * vLits;     // array of literals
@@ -206,6 +207,10 @@ extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCub
 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 );
+/*=== pdrTsim3.c ==========================================================*/
+extern Txs3_Man_t *    Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
+extern void            Txs3_ManStop( Txs3_Man_t * );
+extern Pdr_Set_t *     Txs3_ManTernarySim( Txs3_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 a076223b..cb51e51e 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -265,8 +265,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
         p->vPrio = vPrioInit;
     else if ( pPars->fFlopPrio )
         p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
-    else if ( p->pPars->fNewXSim )
-        p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
+//    else if ( p->pPars->fNewXSim )
+//        p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
     else 
         p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
     p->vLits    = Vec_IntAlloc( 100 );  // array of literals
@@ -281,7 +281,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vRes     = Vec_IntAlloc( 100 );  // final result
     p->pCnfMan  = Cnf_ManStart();
     // ternary simulation
-    p->pTxs     = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL;
+    p->pTxs3    = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
@@ -369,7 +369,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFreeP( &p->vMapPpi2Ff );
     // terminary simulation
     if ( p->pPars->fNewXSim )
-        Txs_ManStop( p->pTxs );
+        Txs3_ManStop( p->pTxs3 );
     // 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 ab582d9e..3c1bbad0 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -147,7 +147,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
     int i, iVar, iVarMax = 0;
     abctime clk = Abc_Clock();
     Vec_IntClear( p->vLits );
-    assert( !(fNext && fCompl) );
+//    assert( !(fNext && fCompl) );
     for ( i = 0; i < pCube->nLits; i++ )
     {
         if ( pCube->Lits[i] == -1 )
@@ -362,7 +362,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         {
             abctime clk = Abc_Clock();
             if ( p->pPars->fNewXSim )
-                *ppPred = Txs_ManTernarySim( p->pTxs, k, pCube );
+                *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
             else
                 *ppPred = Pdr_ManTernarySim( p, k, pCube );
             p->tTsim += Abc_Clock() - clk;
diff --git a/src/proof/pdr/pdrTsim3.c b/src/proof/pdr/pdrTsim3.c
new file mode 100644
index 00000000..c0822322
--- /dev/null
+++ b/src/proof/pdr/pdrTsim3.c
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [pdrTsim3.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: pdrTsim3.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 Txs3_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 * vFosPre;   // cone leaves (CI obj IDs)
+    Vec_Int_t * vFosAbs;   // 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 * vTemp;     // 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
+    int         nPiLits;   // the number of PI literals
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start and stop the ternary simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
+{
+    Txs3_Man_t * p;
+//    Aig_Obj_t * pObj;
+//    int i;
+    assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
+    p = ABC_CALLOC( Txs3_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->vFosPre = Vec_IntAlloc( 100 );  // present flop outputs
+    p->vFosAbs = Vec_IntAlloc( 100 );  // absracted flop outputs
+    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->vTemp   = 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 Txs3_ManStop( Txs3_Man_t * p )
+{
+    Gia_ManStop( p->pGia );
+    Vec_IntFree( p->vCiObjs );
+    Vec_IntFree( p->vFosPre );
+    Vec_IntFree( p->vFosAbs );
+    Vec_IntFree( p->vCoObjs );
+    Vec_IntFree( p->vCiVals );
+    Vec_IntFree( p->vCoVals );
+    Vec_IntFree( p->vNodes );
+    Vec_IntFree( p->vTemp );
+    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 Txs3_ManCollectCone_rec( Txs3_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( !~pObj->Value )
+        return;
+    pObj->Value = ~0;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        int Entry;
+        if ( Gia_ObjIsPi(p->pGia, pObj) )
+        {
+            Vec_IntPush( p->vCiObjs, Gia_ObjId(p->pGia, pObj) );
+            return;
+        }
+        Entry = Gia_ObjCioId(pObj) - Gia_ManPiNum(p->pGia);
+        if ( Vec_IntEntry(p->vPrio, Entry) ) // present flop
+            Vec_IntPush( p->vFosPre, Gia_ObjId(p->pGia, pObj) );
+        else // asbstracted flop
+            Vec_IntPush( p->vFosAbs, Gia_ObjId(p->pGia, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
+    Txs3_ManCollectCone_rec( p, Gia_ObjFanin1(pObj) );
+    Vec_IntPush( p->vNodes, Gia_ObjId(p->pGia, pObj) );
+}
+void Txs3_ManCollectCone( Txs3_Man_t * p, int fVerbose )
+{
+    Gia_Obj_t * pObj; int i, Entry;
+//    printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
+    Vec_IntClear( p->vCiObjs );
+    Vec_IntClear( p->vFosPre );
+    Vec_IntClear( p->vFosAbs );
+    Vec_IntClear( p->vNodes );
+    Gia_ManConst0(p->pGia)->Value = ~0;
+    Gia_ManForEachObjVec( p->vCoObjs, p->pGia, pObj, i )
+        Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
+if ( fVerbose )
+printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_IntSize(p->vFosAbs) );
+    p->nPiLits = Vec_IntSize(p->vCiObjs);
+    // sort primary inputs
+    Vec_IntSelectSort( Vec_IntArray(p->vCiObjs), Vec_IntSize(p->vCiObjs) );
+    // sort and add present flop variables
+    Vec_IntSelectSortReverse( Vec_IntArray(p->vFosPre), Vec_IntSize(p->vFosPre) );
+    Vec_IntForEachEntry( p->vFosPre, Entry, i )
+        Vec_IntPush( p->vCiObjs, Entry );
+    // sort and add absent flop variables
+    Vec_IntSelectSortReverse( Vec_IntArray(p->vFosAbs), Vec_IntSize(p->vFosAbs) );
+    Vec_IntForEachEntry( p->vFosAbs, Entry, i )
+        Vec_IntPush( p->vCiObjs, Entry );
+    // cleanup
+    Gia_ManForEachObjVec( p->vCiObjs, p->pGia, pObj, i )
+        pObj->Value = 0;
+    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+        pObj->Value = 0;
+}
+
+/**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 * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+    int fTryNew = 1;
+    int fUseLit = 1;
+    int fVerbose = 0;
+    sat_solver * pSat;
+    Pdr_Set_t * pRes;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vVar2Ids, * vLits;
+    int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits, nLits;
+//    if ( k == 0 )
+//        fVerbose = 1;
+    // 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
+    Txs3_ManCollectCone( p, fVerbose );
+    // collect values
+    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
+    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
+
+    // read solver
+    pSat = Pdr_ManFetchSolver( p->pMan, k );
+    LitAux = toLit( Pdr_ManFreeVar(p->pMan, k) );
+    // add the clause (complemented cube) in terms of next state variables
+    if ( pCube == NULL ) // the target is the property output
+    {
+        vLits = p->pMan->vLits;
+        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p->pMan, k, 2, Aig_ManCo(p->pMan->pAig, p->pMan->iOutCur)), 1 ); // neg literal (property holds)
+        Vec_IntFill( vLits, 1, Lit );
+    }
+    else
+        vLits = Pdr_ManCubeToLits( p->pMan, k, pCube, 1, 1 );
+    // add activation literal
+    Vec_IntPush( vLits, LitAux );
+    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+    assert( RetValue == 1 );
+    sat_solver_compress( pSat );
+
+    // collect assumptions 
+    Vec_IntClear( p->vTemp );
+    Vec_IntPush( p->vTemp, Abc_LitNot(LitAux) );
+    // iterate through the values of the CI variables
+    Vec_IntForEachEntryTwo( p->vCiObjs, p->vCiVals, Var, Value, i )
+    {
+        Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Var );
+//        iVar = Pdr_ObjSatVar( p->pMan, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
+        int iVar = Pdr_ObjSatVar( p->pMan, k, 3, pObj ); assert( iVar >= 0 );
+        assert( Aig_ObjIsCi(pObj) );
+        Vec_IntPush( p->vTemp, Abc_Var2Lit(iVar, !Value) );
+    }
+    if ( fVerbose )
+    {
+        printf( "Clause with %d lits on lev %d\n", pCube ? pCube->nLits : 0, k );
+        Vec_IntPrint( p->vTemp );
+    }
+
+/*
+    // solve with assumptions
+//printf( "%d -> ", Vec_IntSize(p->vTemp) );
+{
+abctime clk = Abc_Clock();
+// assume all except flops
+    Vec_IntForEachEntryStop( p->vTemp, Lit, i, p->nPiLits + 1 )
+        if ( !sat_solver_push(pSat, Lit) )
+        {
+            assert( 0 );
+        }
+    nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(p->vTemp) + p->nPiLits + 1, Vec_IntSize(p->vTemp) - p->nPiLits - 1, p->pMan->pPars->nConfLimit );
+    Vec_IntShrink( p->vTemp, p->nPiLits + 1 + nLits );
+
+p->pMan->tAbs += Abc_Clock() - clk;
+    for ( i = 0; i <= p->nPiLits; i++ )
+        sat_solver_pop(pSat);
+}
+//printf( "%d    ", nLits );
+*/
+
+
+    //check one last time
+    RetValue = sat_solver_solve( pSat, Vec_IntArray(p->vTemp), Vec_IntLimit(p->vTemp), 0, 0, 0, 0 );
+    assert( RetValue == l_False );
+
+    // use analyze final
+    nCoreLits = sat_solver_final(pSat, &pCoreLits);
+    //assert( Vec_IntSize(p->vTemp) <= nCoreLits );
+
+    Vec_IntClear( p->vTemp );
+    for ( i = 0; i < nCoreLits; i++ )
+        Vec_IntPush( p->vTemp, Abc_LitNot(pCoreLits[i]) );
+    Vec_IntSelectSort( Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp) );
+
+    if ( fVerbose )
+        Vec_IntPrint( p->vTemp );
+
+    // collect the resulting sets
+    Vec_IntClear( p->vPiLits );
+    Vec_IntClear( p->vFfLits );
+    vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->pMan->vVar2Ids, k );
+    Vec_IntForEachEntry( p->vTemp, Lit, i )
+    {
+        if ( Lit != Abc_LitNot(LitAux) )
+        {
+            int Id = Vec_IntEntry( vVar2Ids, Abc_Lit2Var(Lit) );
+            Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Id );
+            assert( Aig_ObjIsCi(pObj) );
+            if ( Saig_ObjIsPi(p->pMan->pAig, pObj) )
+                Vec_IntPush( p->vPiLits, Abc_Var2Lit(Aig_ObjCioId(pObj), Abc_LitIsCompl(Lit)) );
+            else
+                Vec_IntPush( p->vFfLits, Abc_Var2Lit(Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pMan->pAig), Abc_LitIsCompl(Lit)) );
+        }
+    }
+    assert( Vec_IntSize(p->vTemp) == Vec_IntSize(p->vPiLits) + Vec_IntSize(p->vFfLits) + 1 );
+
+    // move abstracted literals from flops to inputs
+    if ( p->pMan->pPars->fUseAbs && p->pMan->vAbsFlops )
+    {
+        int i, iLit, k = 0;
+        Vec_IntForEachEntry( p->vFfLits, iLit, i )
+        {
+            if ( Vec_IntEntry(p->pMan->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
+                Vec_IntWriteEntry( p->vFfLits, k++, iLit );
+            else
+                Vec_IntPush( p->vPiLits, 2*Saig_ManPiNum(p->pMan->pAig) + iLit );
+        }
+        Vec_IntShrink( p->vFfLits, k );
+    }
+
+    if ( fVerbose )
+        Vec_IntPrint( p->vPiLits );
+    if ( fVerbose )
+        Vec_IntPrint( p->vFfLits );
+    if ( fVerbose )
+        printf( "\n" );
+
+    // 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