diff options
Diffstat (limited to 'src/sat/fraig/fraigFeed.c')
-rw-r--r-- | src/sat/fraig/fraigFeed.c | 116 |
1 files changed, 104 insertions, 12 deletions
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 /// //////////////////////////////////////////////////////////////////////// |