Version abc50828

7 files changed, 110 insertions, 0 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 53a46584..946ed56b 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -97,6 +97,7 @@ extern int                 Fraig_ManReadFeedBack( Fraig_Man_t * p );
 extern int                 Fraig_ManReadDoSparse( Fraig_Man_t * p );      
 extern int                 Fraig_ManReadChoicing( Fraig_Man_t * p );      
 extern int                 Fraig_ManReadVerbose( Fraig_Man_t * p );       
+extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
 
 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@@ -157,6 +158,7 @@ extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );
 extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index d60c7168..0194f3b4 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -57,6 +57,7 @@ int               Fraig_ManReadFeedBack( Fraig_Man_t * p )                    {
 int               Fraig_ManReadDoSparse( Fraig_Man_t * p )                    { return p->fDoSparse;  }
 int               Fraig_ManReadChoicing( Fraig_Man_t * p )                    { return p->fChoicing;  }
 int               Fraig_ManReadVerbose( Fraig_Man_t * p )                     { return p->fVerbose;   }
+int *             Fraig_ManReadModel( Fraig_Man_t * p )                       { return p->pModel;     }
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 0a950aba..b46f6c41 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -765,6 +765,47 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
     p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Doubles the size of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
+{
+    int * pModel = NULL;
+    int iPattern;
+    int i;
+
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 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]->puSimD, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, 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]->puSimR, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    return pModel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 1139bdc0..5f8b3496 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -178,6 +178,7 @@ struct Fraig_ManStruct_t_
     Msat_Solver_t *       pSat;          // the SAT solver
     Msat_IntVec_t *       vProj;         // the temporary array of projection vars 
     int                   nSatNums;      // the counter of SAT variables
+    int *                 pModel;        // the assignment, which satisfies the miter
     // these arrays belong to the solver
     Msat_IntVec_t *       vVarsInt;      // the temporary array of variables
     Msat_ClauseVec_t *    vAdjacents;    // the temporary storage for connectivity
@@ -378,6 +379,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_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
@@ -404,6 +406,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 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 );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index d41f5d0b..65716340 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -171,6 +171,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
     if ( p->vProj )      Msat_IntVecFree( p->vProj );
     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
+    if ( p->pModel )     free( p->pModel );
 
     Fraig_MemFixedStop( p->mmNodes, 0 );
     Fraig_MemFixedStop( p->mmSims, 0 );
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index ba22cfad..13c09a9e 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -111,6 +111,31 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckMiter( Fraig_Man_t * p )
+{
+    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+        return 1;
+    // save the counter example
+    FREE( p->pModel );
+    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    // if the model is not found, return undecided
+    if ( p->pModel == NULL )
+        return -1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Checks whether two nodes are functinally equivalent.]
 
   Description [The flag (fComp) tells whether the nodes to be checked
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 5318c41e..4dc6afdc 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -373,6 +373,43 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
 
 /**Function*************************************************************
 
+  Synopsis    [Find the number of the different pattern.]
+
+  Description [Returns -1 if there is no such pattern]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
+{
+    int i, v;
+    assert( !Fraig_IsComplement(pNode1) );
+    assert( !Fraig_IsComplement(pNode2) );
+    if ( fUseRand )
+    {
+        // 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;
+    }
+    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;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Compares two pieces of simulation info.]
 
   Description [Returns 1 if they are equal.]