Version abc51007

4 files changed, 291 insertions, 38 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index dc679907..33ae1e49 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -153,6 +153,9 @@ extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
+extern Fraig_NodeVec_t *   Fraig_ManGetSimInfo( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
+extern void                Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
 
 /*=== fraigDfs.c =============================================================*/
 extern Fraig_NodeVec_t *   Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
@@ -168,6 +171,7 @@ extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t *
 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
 extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index f14fb4c1..a5da2263 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -280,9 +280,9 @@ struct Fraig_NodeStruct_t_
 // the vector of nodes
 struct Fraig_NodeVecStruct_t_
 {
-    Fraig_Node_t **       pArray;        // the array of nodes
-    int                   nSize;         // the number of entries in the array
     int                   nCap;          // the number of allocated entries
+    int                   nSize;         // the number of entries in the array
+    Fraig_Node_t **       pArray;        // the array of nodes
 };
 
 // the hash table 
@@ -381,6 +381,8 @@ extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
 extern int *               Fraig_ManAllocCounterExample( Fraig_Man_t * p );
 extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
+/*=== fraigMan.c =============================================================*/
+extern void                Fraig_ManCreateSolver( Fraig_Man_t * p );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 1a34af86..ca6df9c1 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -225,6 +225,31 @@ void Fraig_ManFree( Fraig_Man_t * p )
     FREE( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares the SAT solver to run on the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManCreateSolver( Fraig_Man_t * p )
+{
+    extern int timeSelect;
+    extern int timeAssign;
+    assert( p->pSat == NULL );
+    // allocate data for SAT solving
+    p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
+    p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
+    p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
+    p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
+    timeSelect = 0;
+    timeAssign = 0;
+}
+
  
 /**Function*************************************************************
 
@@ -264,6 +289,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
 //    PRT( "Assignment", timeAssign );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation information for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+{
+    Fraig_NodeVec_t * vInfo;
+    unsigned * pUnsigned;
+    int i;
+    assert( nSize > 0 && nWords > 0 );
+    vInfo = Fraig_NodeVecAlloc( nSize );
+    pUnsigned = ALLOC( unsigned, nSize * nWords );
+    vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
+    if ( fClean )
+        memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
+    for ( i = 1; i < nSize; i++ )
+        vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
+    vInfo->nSize = nSize;
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns simulation info of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
+{
+    Fraig_NodeVec_t * vInfo;
+    Fraig_Node_t * pNode;
+    unsigned * pUnsigned;
+    int nRandom, nDynamic;
+    int i, k, nWords;
+
+    nRandom  = Fraig_ManReadPatternNumRandom( p );
+    nDynamic = Fraig_ManReadPatternNumDynamic( p );
+    nWords = nRandom / 32 + nDynamic / 32;
+
+    vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
+    for ( i = 0; i < p->vNodes->nSize; i++ )
+    {
+        pNode = p->vNodes->pArray[i];
+        assert( i == pNode->Num );
+        pUnsigned = (unsigned *)vInfo->pArray[i];
+        for ( k = 0; k < nRandom / 32; k++ )
+            pUnsigned[k] = pNode->puSimR[k];
+        for ( k = 0; k < nDynamic / 32; k++ )
+            pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
+    }
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if A v B is always true based on the siminfo.]
+
+  Description [A v B is always true iff A' * B' is always false.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
+{
+    int fCompl1, fCompl2, i;
+
+    fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
+    fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
+
+    pNode1 = Fraig_Regular(pNode1);
+    pNode2 = Fraig_Regular(pNode2);
+    assert( pNode1 != pNode2 );
+    
+    // check the simulation info
+    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( !fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( fCompl1 && !fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+//    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses to the solver.]
+
+  Description [This procedure is used to add external clauses to the solver.
+  The clauses are given by sets of nodes. Each node stands for one literal.
+  If the node is complemented, the literal is negated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
+{
+    Fraig_Node_t * pNode;
+    int i, fComp, RetValue;
+    if ( p->pSat == NULL )
+        Fraig_ManCreateSolver( p );
+    // create four clauses
+    Msat_IntVecClear( p->vProj );
+    for ( i = 0; i < nNodes; i++ )
+    {
+        pNode = Fraig_Regular(ppNodes[i]);
+        fComp = Fraig_IsComplement(ppNodes[i]);
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
+//        printf( "%d(%d) ", pNode->Num, fComp );
+    }
+//    printf( "\n" );
+    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+    assert( RetValue );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index d54a3119..e6b1667e 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -97,7 +97,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
             continue;
         if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
         {
-            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
+            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
             else
                 p->vOutputs->pArray[i] = p->pConst1;
@@ -180,17 +180,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-    {
-        extern int timeSelect;
-        extern int timeAssign;
-        // allocate data for SAT solving
-        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
-        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
-        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
-        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
-        timeSelect = 0;
-        timeAssign = 0;
-    }
+        Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat );
@@ -365,32 +355,12 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-    {
-        extern int timeSelect;
-        extern int timeAssign;
-        // allocate data for SAT solving
-        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
-        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
-        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
-        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
-        timeSelect = 0;
-        timeAssign = 0;
-    }
+        Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat );
 
-
-/*
-    {
-        Fraig_Node_t * ppNodes[2] = { pOld, pNew };
-        extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
-        Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
-    }
-*/
-
-
-    // get the logic cone
+   // get the logic cone
 clk = clock();
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
@@ -449,8 +419,8 @@ if ( fVerbose )
 PRT( "time", clock() - clk );
 }
         // record the counter example
-//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
-//        p->nSatCounterImp++;
+        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
+        p->nSatCounterImp++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
@@ -461,6 +431,96 @@ p->time3 += clock() - clk;
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares the SAT solver to run on the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
+{
+    Fraig_Node_t * pNode1R, * pNode2R;
+    int RetValue, RetValue1, i, clk;
+    int fVerbose = 0;
+
+    pNode1R = Fraig_Regular(pNode1);
+    pNode2R = Fraig_Regular(pNode2);
+    assert( pNode1R != pNode2R );
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+        Fraig_ManCreateSolver( p );
+    // make sure the SAT solver has enough variables
+    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
+        Msat_SolverAddVar( p->pSat );
+
+   // get the logic cone
+clk = clock();
+    Fraig_OrderVariables( p, pNode1R, pNode2R );
+//    Fraig_PrepareCones( p, pNode1R, pNode2R );
+p->timeTrav += clock() - clk;
+
+    ////////////////////////////////////////////
+    // prepare the solver to run incrementally on these variables
+//clk = clock();
+    Msat_SolverPrepare( p->pSat, p->vVarsInt );
+//p->time3 += clock() - clk;
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    Msat_IntVecClear( p->vProj );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
+    // run the solver
+clk = clock();
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
+p->timeSat += clock() - clk;
+
+    if ( RetValue1 == MSAT_FALSE )
+    {
+//p->time1 += clock() - clk;
+
+if ( fVerbose )
+{
+    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+PRT( "time", clock() - clk );
+}
+
+        // add the clause
+        Msat_IntVecClear( p->vProj );
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
+        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+        assert( RetValue );
+//        p->nSatProofImp++;
+        return 1;
+    }
+    else if ( RetValue1 == MSAT_TRUE )
+    {
+//p->time2 += clock() - clk;
+
+if ( fVerbose )
+{
+    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+PRT( "time", clock() - clk );
+}
+        // record the counter example
+//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
+        p->nSatCounterImp++;
+        return 0;
+    }
+    else // if ( RetValue1 == MSAT_UNKNOWN )
+    {
+p->time3 += clock() - clk;
+        p->nSatFailsImp++;
+        return 0;
+    }
+}
 
 
 /**Function*************************************************************