summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/fraig')
-rw-r--r--src/sat/fraig/fraig.h1
-rw-r--r--src/sat/fraig/fraigApi.c8
-rw-r--r--src/sat/fraig/fraigFeed.c116
-rw-r--r--src/sat/fraig/fraigInt.h14
-rw-r--r--src/sat/fraig/fraigMan.c1
-rw-r--r--src/sat/fraig/fraigSat.c18
-rw-r--r--src/sat/fraig/fraigTable.c52
-rw-r--r--src/sat/fraig/fraigUtil.c65
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 17:03:56 +0000