diff options
Diffstat (limited to 'src/sat/fraig/fraigSat.c')
-rw-r--r-- | src/sat/fraig/fraigSat.c | 461 |
1 files changed, 397 insertions, 64 deletions
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 17201e58..53057fc3 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -17,6 +17,7 @@ ***********************************************************************/ #include "fraigInt.h" +#include "math.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -33,6 +34,7 @@ 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 ); @@ -41,8 +43,10 @@ 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 DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -56,13 +60,13 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); SeeAlso [] ***********************************************************************/ -int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) +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 ); + return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit ); } /**Function************************************************************* @@ -95,9 +99,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 ) ) + if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) ) { - if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ) + 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; @@ -105,7 +109,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 ); } } @@ -123,26 +127,158 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) int Fraig_ManCheckMiter( Fraig_Man_t * p ) { Fraig_Node_t * pNode; + int i; 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) ) + 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; - // consider the special case when the miter is constant 1 - if ( pNode == p->pConst1 ) + // skip the boundary node + if ( pNode->TravId == pMan->nTravIds-1 ) { - // 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 ); + 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; } - // 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; + + // 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? '+':'-' ); } @@ -160,34 +296,40 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) +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 ) - { - 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; - } + 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 ); + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); @@ -199,17 +341,26 @@ 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 ); @@ -220,14 +371,18 @@ 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 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -260,13 +415,31 @@ 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; - p->nSatFails++; + +// 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; } @@ -286,8 +459,9 @@ 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 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -319,17 +493,42 @@ 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; - p->nSatFails++; + +// 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; } @@ -359,32 +558,12 @@ 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 ) - { - 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; - } + 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 ); - + 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" ); - } -*/ - - - // get the logic cone + // get the logic cone clk = clock(); Fraig_OrderVariables( p, pOld, pNew ); // Fraig_PrepareCones( p, pOld, pNew ); @@ -411,7 +590,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 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -443,8 +622,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 ) @@ -455,6 +634,96 @@ 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************************************************************* @@ -486,6 +755,7 @@ 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 ); @@ -649,6 +919,8 @@ 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 { @@ -983,6 +1255,33 @@ 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 ); + } @@ -1115,6 +1414,40 @@ 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 /// //////////////////////////////////////////////////////////////////////// |