diff options
Diffstat (limited to 'abc70930/src/sat/fraig/fraigSat.c')
| -rw-r--r-- | abc70930/src/sat/fraig/fraigSat.c | 1455 |
1 files changed, 0 insertions, 1455 deletions
diff --git a/abc70930/src/sat/fraig/fraigSat.c b/abc70930/src/sat/fraig/fraigSat.c deleted file mode 100644 index 53057fc3..00000000 --- a/abc70930/src/sat/fraig/fraigSat.c +++ /dev/null @@ -1,1455 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraigSat.c] - - PackageName [FRAIG: Functionally reduced AND-INV graphs.] - - Synopsis [Proving functional equivalence using SAT.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - October 1, 2004] - - Revision [$Id: fraigSat.c,v 1.10 2005/07/08 01:01:32 alanmi Exp $] - -***********************************************************************/ - -#include "fraigInt.h" -#include "math.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); -static void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ); -static void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ); -static void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); -static void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); - -static void Fraig_SupergateAddClauses( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper ); -static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -//static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); - -extern void * Msat_ClauseVecReadEntry( void * p, int i ); - -// The lesson learned seems to be that variable should be in reverse topological order -// from the output of the miter. The ordering of adjacency lists is very important. -// The best way seems to be fanins followed by fanouts. Slight changes to this order -// leads to big degradation in quality. - -static int nMuxes; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Checks equivalence of two nodes.] - - Description [Returns 1 iff the nodes are equivalent.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ) -{ - if ( pNode1 == pNode2 ) - return 1; - if ( pNode1 == Fraig_Not(pNode2) ) - return 0; - return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit ); -} - -/**Function************************************************************* - - Synopsis [Tries to prove the final miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_ManProveMiter( Fraig_Man_t * p ) -{ - Fraig_Node_t * pNode; - int i, clk; - - if ( !p->fTryProve ) - return; - - clk = clock(); - // consider all outputs of the multi-output miter - for ( i = 0; i < p->vOutputs->nSize; i++ ) - { - pNode = Fraig_Regular(p->vOutputs->pArray[i]); - // skip already constant nodes - if ( pNode == p->pConst1 ) - continue; - // skip nodes that are different according to simulation - if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) ) - continue; - if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) ) - { - 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; - } - } - if ( p->fVerboseP ) - { -// PRT( "Final miter proof time", clock() - clk ); - } -} - -/**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 ) -{ - Fraig_Node_t * pNode; - int i; - FREE( p->pModel ); - for ( i = 0; i < p->vOutputs->nSize; i++ ) - { - // get the output node (it can be complemented!) - pNode = p->vOutputs->pArray[i]; - // if the miter is constant 0, the problem is UNSAT - if ( pNode == Fraig_Not(p->pConst1) ) - continue; - // 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 - p->pModel = Fraig_ManSaveCounterExample( p, pNode ); - // if the model is not found, return undecided - if ( p->pModel == NULL ) - return -1; - else - return 0; - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [Returns 1 if pOld is in the TFI of pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_MarkTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - // skip the visited node - if ( pNode->TravId == pMan->nTravIds ) - return 0; - pNode->TravId = pMan->nTravIds; - // skip the PI node - if ( pNode->NumPi >= 0 ) - return 1; - // check the children - return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) + - Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pOld is in the TFI of pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_MarkTfi2_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - // skip the visited node - if ( pNode->TravId == pMan->nTravIds ) - return 0; - // skip the boundary node - if ( pNode->TravId == pMan->nTravIds-1 ) - { - pNode->TravId = pMan->nTravIds; - return 1; - } - pNode->TravId = pMan->nTravIds; - // skip the PI node - if ( pNode->NumPi >= 0 ) - return 1; - // check the children - return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) + - Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pOld is in the TFI of pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_MarkTfi3_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - // skip the visited node - if ( pNode->TravId == pMan->nTravIds ) - return 1; - // skip the boundary node - if ( pNode->TravId == pMan->nTravIds-1 ) - { - pNode->TravId = pMan->nTravIds; - return 1; - } - pNode->TravId = pMan->nTravIds; - // skip the PI node - if ( pNode->NumPi >= 0 ) - return 0; - // check the children - return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) * - Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) -{ - int NumPis, NumCut, fContain; - - // mark the TFI of pNew - p->nTravIds++; - NumPis = Fraig_MarkTfi_rec( p, pNew ); - printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level ); - - // check if the old is in the TFI - if ( pOld->TravId == p->nTravIds ) - { - printf( "* " ); - return; - } - - // count the boundary of nodes in pOld - p->nTravIds++; - NumCut = Fraig_MarkTfi2_rec( p, pOld ); - printf( "%d", NumCut ); - - // check if the new is contained in the old's support - p->nTravIds++; - fContain = Fraig_MarkTfi3_rec( p, pNew ); - printf( "%c ", fContain? '+':'-' ); -} - - -/**Function************************************************************* - - Synopsis [Checks whether two nodes are functinally equivalent.] - - Description [The flag (fComp) tells whether the nodes to be checked - are in the opposite polarity. The second flag (fSkipZeros) tells whether - the checking should be performed if the simulation vectors are zeros. - Returns 1 if the nodes are equivalent; 0 othewise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) -{ - int RetValue, RetValue1, i, fComp, clk; - int fVerbose = 0; - int fSwitch = 0; - - // make sure the nodes are not complemented - assert( !Fraig_IsComplement(pNew) ); - assert( !Fraig_IsComplement(pOld) ); - assert( pNew != pOld ); - - // if at least one of the nodes is a failed node, perform adjustments: - // if the backtrack limit is small, simply skip this node - // if the backtrack limit is > 10, take the quare root of the limit - if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) - { - p->nSatFails++; -// return 0; -// if ( nBTLimit > 10 ) -// nBTLimit /= 10; - if ( nBTLimit <= 10 ) - return 0; - nBTLimit = (int)sqrt(nBTLimit); -// fSwitch = 1; - } - - p->nSatCalls++; - - // 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, p->vNodes->pArray[i]->Level ); - - - -/* - { - 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" ); - } -*/ - - nMuxes = 0; - - - // get the logic cone -clk = clock(); -// Fraig_VarsStudy( p, pOld, pNew ); - Fraig_OrderVariables( p, pOld, pNew ); -// Fraig_PrepareCones( p, pOld, pNew ); -p->timeTrav += clock() - clk; - -// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); -// PRT( "Time", clock() - clk ); - -if ( fVerbose ) - printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); - - - // prepare variable activity - Fraig_SetActivity( p, pOld, pNew ); - - // get the complemented attribute - fComp = Fraig_NodeComparePhase( pOld, pNew ); -//Msat_SolverPrintClauses( p->pSat ); - - //////////////////////////////////////////// - // 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(pOld->Num, 0) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); - -//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); - - // run the solver -clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); -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(pOld->Num, 1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - // continue solving the other implication - } - 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, pOld, pNew ); - -// if ( pOld->fFailTfo || pNew->fFailTfo ) -// printf( "*" ); -// printf( "s(%d)", pNew->Level ); - if ( fSwitch ) - printf( "s(%d)", pNew->Level ); - p->nSatCounter++; - return 0; - } - else // if ( RetValue1 == MSAT_UNKNOWN ) - { -p->time3 += clock() - clk; - -// if ( pOld->fFailTfo || pNew->fFailTfo ) -// printf( "*" ); -// printf( "T(%d)", pNew->Level ); - - // mark the node as the failed node - if ( pOld != p->pConst1 ) - pOld->fFailTfo = 1; - pNew->fFailTfo = 1; -// p->nSatFails++; - if ( fSwitch ) - printf( "T(%d)", pNew->Level ); - p->nSatFailsReal++; - return 0; - } - - // if the old node was constant 0, we already know the answer - if ( pOld == p->pConst1 ) - return 1; - - //////////////////////////////////////////// - // prepare the solver to run incrementally -//clk = clock(); - Msat_SolverPrepare( p->pSat, p->vVarsInt ); -//p->time3 += clock() - clk; - // solve under assumptions - // A = 0; B = 1 OR A = 0; B = 0 - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); - // run the solver -clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); -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(pOld->Num, 0) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - // continue solving the other implication - } - 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, pOld, pNew ); - p->nSatCounter++; - -// if ( pOld->fFailTfo || pNew->fFailTfo ) -// printf( "*" ); -// printf( "s(%d)", pNew->Level ); - if ( fSwitch ) - printf( "s(%d)", pNew->Level ); - return 0; - } - else // if ( RetValue1 == MSAT_UNKNOWN ) - { -p->time3 += clock() - clk; - -// if ( pOld->fFailTfo || pNew->fFailTfo ) -// printf( "*" ); -// printf( "T(%d)", pNew->Level ); - if ( fSwitch ) - printf( "T(%d)", pNew->Level ); - - // mark the node as the failed node - pOld->fFailTfo = 1; - pNew->fFailTfo = 1; -// p->nSatFails++; - p->nSatFailsReal++; - return 0; - } - - // return SAT proof - p->nSatProof++; - -// if ( pOld->fFailTfo || pNew->fFailTfo ) -// printf( "*" ); -// printf( "u(%d)", pNew->Level ); - - if ( fSwitch ) - printf( "u(%d)", pNew->Level ); - - return 1; -} - - -/**Function************************************************************* - - Synopsis [Checks whether pOld => pNew.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) -{ - int RetValue, RetValue1, i, fComp, clk; - int fVerbose = 0; - - // make sure the nodes are not complemented - assert( !Fraig_IsComplement(pNew) ); - assert( !Fraig_IsComplement(pOld) ); - assert( pNew != pOld ); - - p->nSatCallsImp++; - - // 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, p->vNodes->pArray[i]->Level ); - - // get the logic cone -clk = clock(); - Fraig_OrderVariables( p, pOld, pNew ); -// Fraig_PrepareCones( p, pOld, pNew ); -p->timeTrav += clock() - clk; - -if ( fVerbose ) - printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); - - - // get the complemented attribute - fComp = Fraig_NodeComparePhase( pOld, pNew ); -//Msat_SolverPrintClauses( p->pSat ); - - //////////////////////////////////////////// - // 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(pOld->Num, 0) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); - // 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(pOld->Num, 1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); - 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, pOld, pNew ); - p->nSatCounterImp++; - return 0; - } - else // if ( RetValue1 == MSAT_UNKNOWN ) - { -p->time3 += clock() - clk; - p->nSatFailsImp++; - return 0; - } -} - -/**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, p->vNodes->pArray[i]->Level ); - - // 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************************************************************* - - Synopsis [Prepares the SAT solver to run on the two nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) -{ -// Msat_IntVec_t * vAdjs; -// int * pVars, nVars, i, k; - int nVarsAlloc; - - assert( pOld != pNew ); - assert( !Fraig_IsComplement(pOld) ); - assert( !Fraig_IsComplement(pNew) ); - // clean the variables - nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); - Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); - Msat_IntVecClear( pMan->vVarsInt ); - - pMan->nTravIds++; - Fraig_PrepareCones_rec( pMan, pNew ); - Fraig_PrepareCones_rec( pMan, pOld ); - - -/* - nVars = Msat_IntVecReadSize( pMan->vVarsInt ); - pVars = Msat_IntVecReadArray( pMan->vVarsInt ); - for ( i = 0; i < nVars; i++ ) - { - // process its connections - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); - printf( "%d=%d { ", pVars[i], Msat_IntVecReadSize(vAdjs) ); - for ( k = 0; k < Msat_IntVecReadSize(vAdjs); k++ ) - printf( "%d ", Msat_IntVecReadEntry(vAdjs,k) ); - printf( "}\n" ); - - } - i = 0; -*/ -} - -/**Function************************************************************* - - Synopsis [Traverses the cone, collects the numbers and adds the clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - Fraig_Node_t * pFanin; - Msat_IntVec_t * vAdjs; - int fUseMuxes = 1, i; - int fItIsTime; - - // skip if the node is aleady visited - assert( !Fraig_IsComplement(pNode) ); - if ( pNode->TravId == pMan->nTravIds ) - return; - pNode->TravId = pMan->nTravIds; - - // collect the node's number (closer to reverse topological order) - Msat_IntVecPush( pMan->vVarsInt, pNode->Num ); - Msat_IntVecWriteEntry( pMan->vVarsUsed, pNode->Num, 1 ); - if ( !Fraig_NodeIsAnd( pNode ) ) - return; - - // if the node does not have fanins, create them - fItIsTime = 0; - if ( pNode->vFanins == NULL ) - { - fItIsTime = 1; - // create the fanins of the supergate - assert( pNode->fClauses == 0 ); - if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) - { - pNode->vFanins = Fraig_NodeVecAlloc( 4 ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); - Fraig_SupergateAddClausesMux( pMan, pNode ); - } - else - { - pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes ); - Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins ); - } - assert( pNode->vFanins->nSize > 1 ); - pNode->fClauses = 1; - pMan->nVarsClauses++; - - // add fanins - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pNode->Num ); - assert( Msat_IntVecReadSize( vAdjs ) == 0 ); - for ( i = 0; i < pNode->vFanins->nSize; i++ ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[i]); - Msat_IntVecPush( vAdjs, pFanin->Num ); - } - } - - // recursively visit the fanins - for ( i = 0; i < pNode->vFanins->nSize; i++ ) - Fraig_PrepareCones_rec( pMan, Fraig_Regular(pNode->vFanins->pArray[i]) ); - - if ( fItIsTime ) - { - // recursively visit the fanins - for ( i = 0; i < pNode->vFanins->nSize; i++ ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[i]); - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); - Msat_IntVecPush( vAdjs, pNode->Num ); - } - } -} - -/**Function************************************************************* - - Synopsis [Collect variables using their proximity from the nodes.] - - Description [This procedure creates a variable order based on collecting - first the nodes that are the closest to the given two target nodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) -{ - Fraig_Node_t * pNode, * pFanin; - int i, k, Number, fUseMuxes = 1; - int nVarsAlloc; - - assert( pOld != pNew ); - assert( !Fraig_IsComplement(pOld) ); - assert( !Fraig_IsComplement(pNew) ); - - pMan->nTravIds++; - - // clean the variables - nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); - Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); - Msat_IntVecClear( pMan->vVarsInt ); - - // add the first node - Msat_IntVecPush( pMan->vVarsInt, pOld->Num ); - Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 ); - pOld->TravId = pMan->nTravIds; - - // add the second node - Msat_IntVecPush( pMan->vVarsInt, pNew->Num ); - Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 ); - pNew->TravId = pMan->nTravIds; - - // create the variable order - for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ ) - { - // get the new node on the frontier - Number = Msat_IntVecReadEntry(pMan->vVarsInt, i); - pNode = pMan->vNodes->pArray[Number]; - if ( !Fraig_NodeIsAnd(pNode) ) - continue; - - // if the node does not have fanins, create them - if ( pNode->vFanins == NULL ) - { - // create the fanins of the supergate - assert( pNode->fClauses == 0 ); - // detecting a fanout-free cone (experiment only) -// Fraig_DetectFanoutFreeCone( pMan, pNode ); - - if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) - { - pNode->vFanins = Fraig_NodeVecAlloc( 4 ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) ); - Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); - Fraig_SupergateAddClausesMux( pMan, pNode ); -// Fraig_DetectFanoutFreeConeMux( pMan, pNode ); - - nMuxes++; - } - else - { - pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes ); - Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins ); - } - assert( pNode->vFanins->nSize > 1 ); - pNode->fClauses = 1; - pMan->nVarsClauses++; - - pNode->fMark2 = 1; // goes together with Fraig_SetupAdjacentMark() - } - - // explore the implication fanins of pNode - for ( k = 0; k < pNode->vFanins->nSize; k++ ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); - if ( pFanin->TravId == pMan->nTravIds ) // already collected - continue; - // collect and mark - Msat_IntVecPush( pMan->vVarsInt, pFanin->Num ); - Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 ); - pFanin->TravId = pMan->nTravIds; - } - } - - // set up the adjacent variable information -// Fraig_SetupAdjacent( pMan, pMan->vVarsInt ); - Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt ); -} - - - -/**Function************************************************************* - - Synopsis [Set up the adjacent variable information.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ) -{ - Fraig_Node_t * pNode, * pFanin; - Msat_IntVec_t * vAdjs; - int * pVars, nVars, i, k; - - // clean the adjacents for the variables - nVars = Msat_IntVecReadSize( vConeVars ); - pVars = Msat_IntVecReadArray( vConeVars ); - for ( i = 0; i < nVars; i++ ) - { - // process its connections - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); - Msat_IntVecClear( vAdjs ); - - pNode = pMan->vNodes->pArray[pVars[i]]; - if ( !Fraig_NodeIsAnd(pNode) ) - continue; - - // add fanins - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); - for ( k = 0; k < pNode->vFanins->nSize; k++ ) -// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); - Msat_IntVecPush( vAdjs, pFanin->Num ); -// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); - } - } - // add the fanouts - for ( i = 0; i < nVars; i++ ) - { - pNode = pMan->vNodes->pArray[pVars[i]]; - if ( !Fraig_NodeIsAnd(pNode) ) - continue; - - // add the edges - for ( k = 0; k < pNode->vFanins->nSize; k++ ) -// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); - Msat_IntVecPush( vAdjs, pNode->Num ); -// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); - } - } -} - - -/**Function************************************************************* - - Synopsis [Set up the adjacent variable information.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars ) -{ - Fraig_Node_t * pNode, * pFanin; - Msat_IntVec_t * vAdjs; - int * pVars, nVars, i, k; - - // clean the adjacents for the variables - nVars = Msat_IntVecReadSize( vConeVars ); - pVars = Msat_IntVecReadArray( vConeVars ); - for ( i = 0; i < nVars; i++ ) - { - pNode = pMan->vNodes->pArray[pVars[i]]; - if ( pNode->fMark2 == 0 ) - continue; -// pNode->fMark2 = 0; - - // process its connections -// vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); -// Msat_IntVecClear( vAdjs ); - - if ( !Fraig_NodeIsAnd(pNode) ) - continue; - - // add fanins - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] ); - for ( k = 0; k < pNode->vFanins->nSize; k++ ) -// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); - Msat_IntVecPush( vAdjs, pFanin->Num ); -// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); - } - } - // add the fanouts - for ( i = 0; i < nVars; i++ ) - { - pNode = pMan->vNodes->pArray[pVars[i]]; - if ( pNode->fMark2 == 0 ) - continue; - pNode->fMark2 = 0; - - if ( !Fraig_NodeIsAnd(pNode) ) - continue; - - // add the edges - for ( k = 0; k < pNode->vFanins->nSize; k++ ) -// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- ) - { - pFanin = Fraig_Regular(pNode->vFanins->pArray[k]); - vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num ); - Msat_IntVecPush( vAdjs, pNode->Num ); -// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num ); - } - } -} - - - - -/**Function************************************************************* - - Synopsis [Adds clauses to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SupergateAddClauses( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper ) -{ - int fComp1, RetValue, nVars, Var, Var1, i; - - assert( Fraig_NodeIsAnd( pNode ) ); - nVars = Msat_SolverReadVarNum(p->pSat); - - Var = pNode->Num; - assert( Var < nVars ); - for ( i = 0; i < vSuper->nSize; i++ ) - { - // get the predecessor nodes - // get the complemented attributes of the nodes - fComp1 = Fraig_IsComplement(vSuper->pArray[i]); - // determine the variable numbers - Var1 = Fraig_Regular(vSuper->pArray[i])->Num; - // check that the variables are in the SAT manager - assert( Var1 < nVars ); - - // suppose the AND-gate is A * B = C - // add !A => !C or A + !C - // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, fComp1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 1) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - } - - // add A & B => C or !A + !B + C -// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 ); - Msat_IntVecClear( p->vProj ); - for ( i = 0; i < vSuper->nSize; i++ ) - { - // get the predecessor nodes - // get the complemented attributes of the nodes - fComp1 = Fraig_IsComplement(vSuper->pArray[i]); - // determine the variable numbers - Var1 = Fraig_Regular(vSuper->pArray[i])->Num; - - // add this variable to the array - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, !fComp1) ); - } - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 0) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); -} - -/**Function************************************************************* - - Synopsis [Adds clauses to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SupergateAddClausesExor( Fraig_Man_t * p, Fraig_Node_t * pNode ) -{ - Fraig_Node_t * pNode1, * pNode2; - int fComp, RetValue; - - assert( !Fraig_IsComplement( pNode ) ); - assert( Fraig_NodeIsExorType( pNode ) ); - // get nodes - pNode1 = Fraig_Regular(Fraig_Regular(pNode->p1)->p1); - pNode2 = Fraig_Regular(Fraig_Regular(pNode->p1)->p2); - // get the complemented attribute of the EXOR/NEXOR gate - fComp = Fraig_NodeIsExor( pNode ); // 1 if EXOR, 0 if NEXOR - - // create four clauses - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); -} - -/**Function************************************************************* - - Synopsis [Adds clauses to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) -{ - Fraig_Node_t * pNodeI, * pNodeT, * pNodeE; - int RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; - - assert( !Fraig_IsComplement( pNode ) ); - assert( Fraig_NodeIsMuxType( pNode ) ); - // get nodes (I = if, T = then, E = else) - pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); - // get the variable numbers - VarF = pNode->Num; - VarI = pNodeI->Num; - VarT = Fraig_Regular(pNodeT)->Num; - VarE = Fraig_Regular(pNodeE)->Num; - // get the complementation flags - fCompT = Fraig_IsComplement(pNodeT); - fCompE = Fraig_IsComplement(pNodeE); - - // f = ITE(i, t, e) - - // i' + t' + f - // i' + t + f' - // i + e' + f - // i + e + f' - - // create four clauses - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - - // two additional clauses - // t' & e' -> f' - // t & e -> f - - // t + e + f' - // t' + e' + f - - if ( VarT == VarE ) - { -// assert( fCompT == !fCompE ); - return; - } - - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - Msat_IntVecClear( p->vProj ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); - Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); - RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); - assert( RetValue ); - -} - - - - - -/**Function************************************************************* - - Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_DetectFanoutFreeCone_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst ) -{ - // make the pointer regular - pNode = Fraig_Regular(pNode); - // if the new node is complemented or a PI, another gate begins - if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) ) - { - Fraig_NodeVecPushUnique( vSuper, pNode ); - return; - } - // go through the branches - Fraig_DetectFanoutFreeCone_rec( pNode->p1, vSuper, vInside, 0 ); - Fraig_DetectFanoutFreeCone_rec( pNode->p2, vSuper, vInside, 0 ); - // add the node - Fraig_NodeVecPushUnique( vInside, pNode ); -} - -/**Function************************************************************* - - Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -/* -void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - Fraig_NodeVec_t * vFanins; - Fraig_NodeVec_t * vInside; - int nCubes; - extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside ); - - vFanins = Fraig_NodeVecAlloc( 8 ); - vInside = Fraig_NodeVecAlloc( 8 ); - - Fraig_DetectFanoutFreeCone_rec( pNode, vFanins, vInside, 1 ); - assert( vInside->pArray[vInside->nSize-1] == pNode ); - - nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside ); - -printf( "%d(%d)", vFanins->nSize, nCubes ); - Fraig_NodeVecFree( vFanins ); - Fraig_NodeVecFree( vInside ); -} -*/ - - - -/**Function************************************************************* - - Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_DetectFanoutFreeConeMux_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst ) -{ - // make the pointer regular - pNode = Fraig_Regular(pNode); - // if the new node is complemented or a PI, another gate begins - if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) || !Fraig_NodeIsMuxType(pNode) ) - { - Fraig_NodeVecPushUnique( vSuper, pNode ); - return; - } - // go through the branches - Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p1, vSuper, vInside, 0 ); - Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p2, vSuper, vInside, 0 ); - Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p1, vSuper, vInside, 0 ); - Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p2, vSuper, vInside, 0 ); - // add the node - Fraig_NodeVecPushUnique( vInside, pNode ); -} - -/**Function************************************************************* - - Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) -{ - Fraig_NodeVec_t * vFanins; - Fraig_NodeVec_t * vInside; - int nCubes; - extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside ); - - vFanins = Fraig_NodeVecAlloc( 8 ); - vInside = Fraig_NodeVecAlloc( 8 ); - - Fraig_DetectFanoutFreeConeMux_rec( pNode, vFanins, vInside, 1 ); - assert( vInside->pArray[vInside->nSize-1] == pNode ); - -// nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside ); - nCubes = 0; - -printf( "%d(%d)", vFanins->nSize, nCubes ); - Fraig_NodeVecFree( vFanins ); - Fraig_NodeVecFree( vInside ); -} - - - -/**Function************************************************************* - - Synopsis [Collect variables using their proximity from the nodes.] - - Description [This procedure creates a variable order based on collecting - first the nodes that are the closest to the given two target nodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) -{ - Fraig_Node_t * pNode; - int i, Number, MaxLevel; - float * pFactors = Msat_SolverReadFactors(pMan->pSat); - if ( pFactors == NULL ) - return; - MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level ); - // create the variable order - for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ ) - { - // get the new node on the frontier - Number = Msat_IntVecReadEntry(pMan->vVarsInt, i); - pNode = pMan->vNodes->pArray[Number]; - pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level ); -// if ( pNode->Num % 50 == 0 ) -// printf( "(%d) %.2f ", MaxLevel - pNode->Level, pFactors[pNode->Num] ); - } -// printf( "\n" ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |