From 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 08:01:00 -0800 Subject: Version abc80130 --- src/sat/fraig/fraigSat.c | 461 +++++++---------------------------------------- 1 file changed, 64 insertions(+), 397 deletions(-) (limited to 'src/sat/fraig/fraigSat.c') diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 53057fc3..17201e58 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -17,7 +17,6 @@ ***********************************************************************/ #include "fraigInt.h" -#include "math.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -34,7 +33,6 @@ static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pN 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 ); @@ -43,10 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); // 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 DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -60,13 +56,13 @@ static int nMuxes; SeeAlso [] ***********************************************************************/ -int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ) +int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) { if ( pNode1 == pNode2 ) return 1; if ( pNode1 == Fraig_Not(pNode2) ) return 0; - return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit ); + return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit ); } /**Function************************************************************* @@ -99,9 +95,9 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) // 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_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) ) { - if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) ) + if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ) p->vOutputs->pArray[i] = Fraig_Not(p->pConst1); else p->vOutputs->pArray[i] = p->pConst1; @@ -109,7 +105,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) } if ( p->fVerboseP ) { -// PRT( "Final miter proof time", clock() - clk ); + PRT( "Final miter proof time", clock() - clk ); } } @@ -127,158 +123,26 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) 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 ) + // 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; - // skip the boundary node - if ( pNode->TravId == pMan->nTravIds-1 ) + // consider the special case when the miter is constant 1 + if ( pNode == p->pConst1 ) { - pNode->TravId = pMan->nTravIds; - return 1; - } - pNode->TravId = pMan->nTravIds; - // skip the PI node - if ( pNode->NumPi >= 0 ) + // 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; - // 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? '+':'-' ); + // save the counter example + p->pModel = Fraig_ManSaveCounterExample( p, pNode ); + // if the model is not found, return undecided + if ( p->pModel == NULL ) + return -1; + return 0; } @@ -296,40 +160,34 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew SeeAlso [] ***********************************************************************/ -int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) +int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) { 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 ); + { + extern int timeSelect; + extern int timeAssign; + // allocate data for SAT solving + p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 ); + p->vVarsInt = Msat_SolverReadConeVars( p->pSat ); + p->vAdjacents = Msat_SolverReadAdjacents( p->pSat ); + p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat ); + timeSelect = 0; + timeAssign = 0; + } // 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 ); + Msat_SolverAddVar( p->pSat ); @@ -341,26 +199,17 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * } */ - 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 ); @@ -371,18 +220,14 @@ if ( fVerbose ) 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 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -415,31 +260,13 @@ 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++; + p->nSatFails++; return 0; } @@ -459,9 +286,8 @@ p->time3 += clock() - clk; Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); // run the solver clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); p->timeSat += clock() - clk; - if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -493,42 +319,17 @@ 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++; + p->nSatFails++; 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; } @@ -558,12 +359,32 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t // make sure the solver is allocated and has enough variables if ( p->pSat == NULL ) - Fraig_ManCreateSolver( p ); + { + extern int timeSelect; + extern int timeAssign; + // allocate data for SAT solving + p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 ); + p->vVarsInt = Msat_SolverReadConeVars( p->pSat ); + p->vAdjacents = Msat_SolverReadAdjacents( p->pSat ); + p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat ); + timeSelect = 0; + timeAssign = 0; + } // 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 ); + Msat_SolverAddVar( p->pSat ); + - // get the logic cone +/* + { + 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" ); + } +*/ + + + // get the logic cone clk = clock(); Fraig_OrderVariables( p, pOld, pNew ); // Fraig_PrepareCones( p, pOld, pNew ); @@ -590,7 +411,7 @@ if ( fVerbose ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); // run the solver clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -622,8 +443,8 @@ if ( fVerbose ) PRT( "time", clock() - clk ); } // record the counter example - Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); - p->nSatCounterImp++; +// Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); +// p->nSatCounterImp++; return 0; } else // if ( RetValue1 == MSAT_UNKNOWN ) @@ -634,96 +455,6 @@ p->time3 += clock() - clk; } } -/**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************************************************************* @@ -755,7 +486,6 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * Fraig_PrepareCones_rec( pMan, pNew ); Fraig_PrepareCones_rec( pMan, pOld ); - /* nVars = Msat_IntVecReadSize( pMan->vVarsInt ); pVars = Msat_IntVecReadArray( pMan->vVarsInt ); @@ -919,8 +649,6 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); Fraig_SupergateAddClausesMux( pMan, pNode ); // Fraig_DetectFanoutFreeConeMux( pMan, pNode ); - - nMuxes++; } else { @@ -1255,33 +983,6 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) 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 ); - } @@ -1414,40 +1115,6 @@ printf( "%d(%d)", vFanins->nSize, nCubes ); } - -/**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 /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3