Experiments with SAT-based simulation.

5 files changed, 146 insertions, 6 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 039628bf..fcdb3941 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -150,6 +150,7 @@ struct Gia_Man_t_
     Vec_Ptr_t *    vSeqModelVec;  // sequential counter-examples
     Vec_Int_t      vCopies;       // intermediate copies
     Vec_Int_t      vCopies2;      // intermediate copies
+    Vec_Int_t *    vVar2Obj;      // mapping of variables into objects
     Vec_Int_t *    vTruths;       // used for truth table computation
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
     Vec_Int_t *    vGateClasses;  // classes of gates for abstraction
@@ -209,6 +210,11 @@ struct Gia_Man_t_
     Vec_Wrd_t *    vSimsPi;
     Vec_Int_t *    vClassOld;
     Vec_Int_t *    vClassNew;
+    // incremental simulation
+    int            fIncrSim;
+    int            iNextPi;
+    int            iTimeStamp;
+    Vec_Int_t *    vTimeStamps;
     // truth table computation for small functions
     int            nTtVars;       // truth table variables
     int            nTtWords;      // truth table words
@@ -1518,6 +1524,10 @@ extern int                 Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0
 extern void                Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 );
 extern void                Gia_ManBuiltInSimResimulate( Gia_Man_t * p );
 extern int                 Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat );
+extern void                Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs );
+extern void                Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits );
+extern int                 Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 );
+extern int                 Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
 /*=== giaSpeedup.c ============================================================*/
 extern float               Gia_ManDelayTraceLut( Gia_Man_t * p );
 extern float               Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 7d0ef288..bc270168 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -92,6 +92,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vClassOld );
     Vec_WrdFreeP( &p->vSims );
     Vec_WrdFreeP( &p->vSimsPi );
+    Vec_IntFreeP( &p->vTimeStamps );
     Vec_FltFreeP( &p->vTiming );
     Vec_VecFreeP( &p->vClockDoms );
     Vec_IntFreeP( &p->vCofVars );
@@ -118,6 +119,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vTruths );
     Vec_IntErase( &p->vCopies );
     Vec_IntErase( &p->vCopies2 );
+    Vec_IntFreeP( &p->vVar2Obj );
     Vec_IntErase( &p->vCopiesTwo );
     Vec_IntErase( &p->vSuppVars );
     Vec_WrdFreeP( &p->vSuppWords );
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 192184c8..228f6fb4 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -800,7 +800,7 @@ void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj )
     word * pInfo  = Gia_ManBuiltInData( p, iObj ); 
     word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
     word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); 
-    assert( p->fBuiltInSim );
+    assert( p->fBuiltInSim || p->fIncrSim );
     if ( Gia_ObjFaninC0(pObj) )
     {
         if (  Gia_ObjFaninC1(pObj) )
@@ -860,7 +860,7 @@ int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
 {
     word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
     word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
-    assert( p->fBuiltInSim );
+    assert( p->fBuiltInSim || p->fIncrSim );
 
 //    printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
 //    Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
@@ -903,7 +903,7 @@ int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
 {
     word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
     word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
-    assert( p->fBuiltInSim );
+    assert( p->fBuiltInSim || p->fIncrSim );
 
 //    printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
 //    Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
@@ -1113,6 +1113,113 @@ int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vOb
     return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs );
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Bit-parallel simulation during AIG construction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManIncrSimUpdate( Gia_Man_t * p )
+{
+    int i, k;
+    // extend timestamp info
+    assert( Vec_IntSize(p->vTimeStamps) <= Gia_ManObjNum(p) );
+    Vec_IntFillExtra( p->vTimeStamps, Gia_ManObjNum(p), 0 );
+    // extend simulation info
+    assert( Vec_WrdSize(p->vSims) <= Gia_ManObjNum(p) * p->nSimWords );
+    Vec_WrdFillExtra( p->vSims,  Gia_ManObjNum(p) * p->nSimWords,  0 );
+    // extend PI info
+    assert( p->iNextPi <= Gia_ManCiNum(p) );
+    for ( i = p->iNextPi; i < Gia_ManCiNum(p); i++ )
+    {
+        word * pSims = Gia_ManBuiltInData( p, Gia_ManCiIdToId(p, i) );
+        for ( k = 0; k < p->nSimWords; k++ )
+            pSims[k] = Gia_ManRandomW(0);
+    }
+    p->iNextPi = Gia_ManCiNum(p);
+}
+void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs )
+{
+    assert( !p->fIncrSim );
+    p->fIncrSim  = 1;
+    p->iPatsPi   = 0;
+    p->nSimWords = nWords;
+    // init time stamps
+    p->iTimeStamp  = 1;
+    p->vTimeStamps = Vec_IntAlloc( p->nSimWords );
+    // init object sim info
+    p->iNextPi = 0;       
+    p->vSims   = Vec_WrdAlloc( p->nSimWords * nObjs );
+    Gia_ManRandomW( 1 );
+}
+void Gia_ManIncrSimStop( Gia_Man_t * p )
+{
+    assert( p->fIncrSim );
+    p->fIncrSim   = 0;
+    p->iPatsPi    = 0;
+    p->nSimWords  = 0;
+    p->iTimeStamp = 1;
+    Vec_IntFreeP( &p->vTimeStamps );
+    Vec_WrdFreeP( &p->vSims );
+}
+void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits )
+{
+    int i, iLit; 
+    assert( Vec_IntSize(vObjLits) > 0 );
+    p->iTimeStamp++;
+    Vec_IntForEachEntry( vObjLits, iLit, i )
+    {
+        word * pSims = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit) );
+        if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+            continue;
+        //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 );
+        //Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
+        if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) )
+             Abc_TtXorBit(pSims, p->iPatsPi);
+    }
+    p->iPatsPi = (p->iPatsPi == p->nSimWords * 64 - 1) ? 0 : p->iPatsPi + 1;
+}
+void Gia_ManIncrSimCone_rec( Gia_Man_t * p, int iObj )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    if ( Vec_IntEntry(p->vTimeStamps, iObj) == p->iTimeStamp )
+        return;
+    assert( Vec_IntEntry(p->vTimeStamps, iObj) < p->iTimeStamp );
+    Vec_IntWriteEntry( p->vTimeStamps, iObj, p->iTimeStamp );
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
+    Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
+    Gia_ManBuiltInSimPerformInt( p, iObj );
+}
+int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
+{
+    assert( iLit0 > 1 && iLit1 > 1 );
+    Gia_ManIncrSimUpdate( p );
+    Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
+    Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
+    return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 );
+}
+int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
+{
+    assert( iLit0 > 1 && iLit1 > 1 );
+    Gia_ManIncrSimUpdate( p );
+    Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
+    Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
+    return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index 0f4bf2bb..1d2ebd1d 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -301,12 +301,19 @@ void Cec2_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
 }
 void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat )
 {
+    int iVar;
     assert( !Gia_IsComplement(pObj) );
     assert( !Gia_ObjIsConst0(pObj) );
     if ( Cec2_ObjSatId(p, pObj) >= 0 )
         return;
     assert( Cec2_ObjSatId(p, pObj) == -1 );
-    Cec2_ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) );
+    iVar = satoko_add_variable(pSat, 0);
+    if ( p->vVar2Obj )
+    {
+        assert( Vec_IntSize(p->vVar2Obj) == iVar );
+        Vec_IntPush( p->vVar2Obj, Gia_ObjId(p, pObj) );
+    }
+    Cec2_ObjSetSatId( p, pObj, iVar );
     if ( Gia_ObjIsAnd(pObj) )
         Vec_PtrPush( vFrontier, pObj );
 }
@@ -322,7 +329,15 @@ int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr
         return Cec2_ObjSatId(pGia,pObj);
     assert( iObj > 0 );
     if ( Gia_ObjIsCi(pObj) )
-        return Cec2_ObjSetSatId( pGia, pObj, satoko_add_variable(pSat, 0) );
+    {
+        int iVar = satoko_add_variable(pSat, 0);
+        if ( pGia->vVar2Obj )
+        {
+            assert( Vec_IntSize(pGia->vVar2Obj) == iVar );
+            Vec_IntPush( pGia->vVar2Obj, iObj );
+        }
+        return Cec2_ObjSetSatId( pGia, pObj, iVar );
+    }
     assert( Gia_ObjIsAnd(pObj) );
     // start the frontier
     Vec_PtrClear( vFrontier );
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index adf30cef..79d48c3b 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -281,7 +281,13 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
         solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF);
         return (s->status = (solver_propagate(s) == UNDEF));
     }
-
+    if ( 0 ) {
+        for ( i = 0; i < vec_uint_size(s->temp_lits); i++ ) {
+            int lit = vec_uint_at(s->temp_lits, i);
+            printf( "%s%d ", lit&1 ? "!":"", lit>>1 );
+        }
+        printf( "\n" );
+    }
     cref = solver_clause_create(s, s->temp_lits, 0);
     clause_watch(s, cref);
     return SATOKO_OK;