Version abc50904

8 files changed, 235 insertions, 40 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 946ed56b..39c6fae8 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -50,6 +50,7 @@ struct Fraig_ParamsStruct_t_
     int  fTryProve;     // tries to solve the final miter
     int  fVerbose;      // the verbosiness flag
     int  fVerboseP;     // the verbosiness flag (for proof reporting)
+    int  fInternal;     // is set to 1 for internal fraig calls
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index 0194f3b4..c9e6960c 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -164,10 +164,9 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a new node.]
+  Synopsis    [Creates a new PO node.]
 
-  Description [This procedure should be called to create the constant
-  node and the PI nodes first.]
+  Description [This procedure may take a complemented node.]
                
   SideEffects []
 
@@ -176,9 +175,8 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i )
 ***********************************************************************/
 void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode )
 {
-//    assert( pNode->fNodePo == 0 ); 
     // internal node may be a PO two times
-    pNode->fNodePo = 1;
+    Fraig_Regular(pNode)->fNodePo = 1;
     Fraig_NodeVecPush( p->vOutputs, pNode );
 }
 
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index b46f6c41..73640387 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -768,7 +768,80 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Doubles the size of simulation info.]
+  Synopsis    [Generated trivial counter example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fraig_ManAllocCounterExample( Fraig_Man_t * p )
+{
+    int * pModel;
+    pModel = ALLOC( int, p->vInputs->nSize );
+    memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+    return pModel;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the counter example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManSimulateBitNode_rec( Fraig_Man_t * p, Fraig_Node_t * pNode )
+{
+    int Value0, Value1;
+    if ( Fraig_NodeIsTravIdCurrent( p, pNode ) )
+        return pNode->fMark3;
+    Fraig_NodeSetTravIdCurrent( p, pNode );
+    Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) );
+    Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) );
+    Value0 ^= Fraig_IsComplement(pNode->p1);
+    Value1 ^= Fraig_IsComplement(pNode->p2);
+    pNode->fMark3 = Value0 & Value1;
+    return pNode->fMark3;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one bit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManSimulateBitNode( Fraig_Man_t * p, Fraig_Node_t * pNode, int * pModel )
+{
+    int fCompl, RetValue, i;
+    // set the PI values
+    Fraig_ManIncrementTravId( p );
+    for ( i = 0; i < p->vInputs->nSize; i++ )
+    {
+        Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] );
+        p->vInputs->pArray[i]->fMark3 = pModel[i];
+    }
+    // perform the traversal
+    fCompl = Fraig_IsComplement(pNode);
+    RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) );
+    return fCompl ^ RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the counter example.]
 
   Description []
                
@@ -779,33 +852,52 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
 ***********************************************************************/
 int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
 {
-    int * pModel = NULL;
+    int * pModel;
     int iPattern;
-    int i;
+    int i, fCompl;
 
-    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 );
+    // the node can be complemented
+    fCompl = Fraig_IsComplement(pNode);
+    // because we compare with constant 0, p->pConst1 should also be complemented
+    fCompl = !fCompl;
+
+    // derive the model
+    pModel = Fraig_ManAllocCounterExample( p );
+    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 );
     if ( iPattern >= 0 )
     {
-        pModel = ALLOC( int, p->vInputs->nSize );
-        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
         for ( i = 0; i < p->vInputs->nSize; i++ )
-            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
                 pModel[i] = 1;
+/*
+printf( "SAT solver's pattern:\n" );
+for ( i = 0; i < p->vInputs->nSize; i++ )
+    printf( "%d", pModel[i] );
+printf( "\n" );
+*/
+        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
         return pModel;
     }
-    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 );
+    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 );
     if ( iPattern >= 0 )
     {
-        pModel = ALLOC( int, p->vInputs->nSize );
-        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
         for ( i = 0; i < p->vInputs->nSize; i++ )
-            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
                 pModel[i] = 1;
+/*
+printf( "SAT solver's pattern:\n" );
+for ( i = 0; i < p->vInputs->nSize; i++ )
+    printf( "%d", pModel[i] );
+printf( "\n" );
+*/
+        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
         return pModel;
     }
-    return pModel;
+    FREE( pModel );
+    return NULL;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 5f8b3496..1c765c12 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -239,10 +239,11 @@ struct Fraig_NodeStruct_t_
     unsigned              fMark0   :  1; // the mark used for traversals
     unsigned              fMark1   :  1; // the mark used for traversals
     unsigned              fMark2   :  1; // the mark used for traversals
+    unsigned              fMark3   :  1; // the mark used for traversals
     unsigned              fFeedUse :  1; // the presence of the variable in the feedback
     unsigned              fFeedVal :  1; // the value of the variable in the feedback
     unsigned              nFanouts :  2; // the indicator of fanouts (none, one, or many)
-    unsigned              nOnes    : 22; // the number of 1's in the random sim info
+    unsigned              nOnes    : 21; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child
@@ -379,6 +380,7 @@ extern void                Fraig_FeedBackInit( Fraig_Man_t * p );
 extern void                Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 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 );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
@@ -406,7 +408,7 @@ extern Fraig_Node_t *      Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No
 extern void                Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern int                 Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
-extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
+extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand );
 extern void                Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
 extern void                Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
 extern void                Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
@@ -416,10 +418,6 @@ extern int                 Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEqu
 extern int                 Fraig_NodeCountPis( Msat_IntVec_t * vVars, int nVarsPi );
 extern int                 Fraig_NodeCountSuppVars( Fraig_Man_t * p, Fraig_Node_t * pNode, int fSuppStr );
 extern int                 Fraig_NodesCompareSupps( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
-extern void                Fraig_ManIncrementTravId( Fraig_Man_t * pMan );
-extern void                Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-extern int                 Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_NodeAndSimpleCase_rec( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern int                 Fraig_NodeIsExorType( Fraig_Node_t * pNode );
 extern void                Fraig_ManSelectBestChoice( Fraig_Man_t * p );
@@ -435,6 +433,10 @@ extern int                 Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_No
 extern int                 Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );
 extern int                 Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums );
+extern void                Fraig_ManIncrementTravId( Fraig_Man_t * pMan );
+extern void                Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+extern int                 Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 /*=== fraigVec.c ===============================================================*/
 extern void                Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
 
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 65716340..cfdba619 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -42,6 +42,7 @@ int timeAssign;
 ***********************************************************************/
 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 {
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
     pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
     pParams->nBTLimit   = 99;                     // the max number of backtracks to perform
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index da9e8e2b..17201e58 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -122,11 +122,23 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 ***********************************************************************/
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
-    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+    Fraig_Node_t * pNode;
+    FREE( p->pModel );
+    // get the output node (it can be complemented!)
+    pNode = p->vOutputs->pArray[0];
+    // if the miter is constant 0, the problem is UNSAT
+    if ( pNode == Fraig_Not(p->pConst1) )
         return 1;
+    // consider the special case when the miter is constant 1
+    if ( pNode == p->pConst1 )
+    {
+        // in this case, any counter example will do to distinquish it from constant 0
+        // here we pick the counter example composed of all zeros
+        p->pModel = Fraig_ManAllocCounterExample( p );
+        return 0;
+    }
     // save the counter example
-    FREE( p->pModel );
-    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
     // if the model is not found, return undecided
     if ( p->pModel == NULL )
         return -1;
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 4dc6afdc..7a8af749 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -382,28 +382,52 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
+int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand )
 {
     int i, v;
     assert( !Fraig_IsComplement(pNode1) );
     assert( !Fraig_IsComplement(pNode2) );
-    if ( fUseRand )
+    // take into account possible internal complementation
+    fCompl ^= pNode1->fInv;
+    fCompl ^= pNode2->fInv;
+    // find the pattern
+    if ( fCompl )
     {
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimR[i] !=  pNode2->puSimR[i] )
-                for ( v = 0; v < 32; v++ )
-                    if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
-                        return i * 32 + v;
+        if ( fUseRand )
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
+        else
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimD[i] !=  ~pNode2->puSimD[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
     }
     else
     {
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
-                for ( v = 0; v < 32; v++ )
-                    if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
-                        return i * 32 + v;
+        if ( fUseRand )
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
+        else
+        {
+            for ( i = 0; i < iWordLast; i++ )
+                if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
+                    for ( v = 0; v < 32; v++ )
+                        if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
+                            return i * 32 + v;
+        }
     }
     return -1;
 }
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 6b7431f2..2155c4a3 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -962,6 +962,71 @@ Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux )
     return vSuper;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManIncrementTravId( Fraig_Man_t * pMan )
+{
+    pMan->nTravIds2++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    pNode->TravId2 = pMan->nTravIds2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    return pNode->TravId2 == pMan->nTravIds2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
+{
+    return pNode->TravId2 == pMan->nTravIds2 - 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////