diff options
Diffstat (limited to 'src/sat/fraig')
| -rw-r--r-- | src/sat/fraig/fraig.h | 5 | ||||
| -rw-r--r-- | src/sat/fraig/fraigCanon.c | 2 | ||||
| -rw-r--r-- | src/sat/fraig/fraigInt.h | 1 | ||||
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 2 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 14 |
5 files changed, 14 insertions, 10 deletions
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 901bbac9..75dfb812 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -43,6 +43,7 @@ struct Fraig_ParamsStruct_t_ int nPatsRand; // the number of words of random simulation info int nPatsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the timeout for the final proof int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables distance-1 patterns @@ -162,8 +163,8 @@ extern int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pO extern int Fraig_CountLevels( Fraig_Man_t * pMan ); /*=== fraigSat.c =============================================================*/ -extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ); -extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); +extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ); +extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ); extern void Fraig_ManProveMiter( Fraig_Man_t * p ); extern int Fraig_ManCheckMiter( Fraig_Man_t * p ); diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 5a7d0563..a8d6c3af 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -167,7 +167,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ // there is another node which looks the same according to simulation // use SAT to resolve the ambiguity - if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit ) ) + if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) ) { // set the node to be equivalent with this node // to prevent loops, only set if the old node is not in the TFI of the new node diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 131b750c..f14fb4c1 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -143,6 +143,7 @@ struct Fraig_ManStruct_t_ int nWordsRand; // the number of words of random simulation info int nWordsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the runtime limit for the miter proof int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables solver feedback diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index e5979c93..aa7e5999 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -46,6 +46,7 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) 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 + pParams->nSeconds = 20; // the max number of seconds to solve the miter pParams->fFuncRed = 1; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns @@ -100,6 +101,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit + p->nSeconds = pParams->nSeconds; // the timeout for the final miter p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed) p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation) p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation) diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 17201e58..fcb1018f 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -56,13 +56,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,7 +95,7 @@ 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]) ) p->vOutputs->pArray[i] = Fraig_Not(p->pConst1); @@ -160,7 +160,7 @@ 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; @@ -227,7 +227,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, nTimeLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -286,7 +286,7 @@ 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 ) { @@ -411,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 ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) |