From 3db1557f45b03875a0a0b8adddcc15c4565895d2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 11 Jun 2006 08:01:00 -0700 Subject: Version abc60611 --- src/sat/fraig/fraig.h | 42 ++++++++++++++++++++++++++---------------- src/sat/fraig/fraigApi.c | 4 ++++ src/sat/fraig/fraigCanon.c | 4 +++- src/sat/fraig/fraigInt.h | 3 ++- src/sat/fraig/fraigMan.c | 12 +++++++++++- 5 files changed, 46 insertions(+), 19 deletions(-) (limited to 'src/sat/fraig') diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index d6215465..84363efe 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -27,6 +27,8 @@ extern "C" { /// INCLUDES /// //////////////////////////////////////////////////////////////////////// +#include "solver.h" + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// @@ -49,8 +51,6 @@ struct Fraig_ParamsStruct_t_ 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 nConfLimit; - int nImpLimit; int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables distance-1 patterns @@ -60,31 +60,39 @@ struct Fraig_ParamsStruct_t_ int fVerbose; // the verbosiness flag int fVerboseP; // the verbosiness flag (for proof reporting) int fInternal; // is set to 1 for internal fraig calls + int nConfLimit; // the limit on the number of conflicts + sint64 nInspLimit; // the limit on the number of inspections }; struct Prove_ParamsStruct_t_ { // general parameters - int fUseFraiging; // enables fraiging - int fUseRewriting; // enables rewriting - int fUseBdds; // enables BDD construction when other methods fail - int fVerbose; // prints verbose stats + int fUseFraiging; // enables fraiging + int fUseRewriting; // enables rewriting + int fUseBdds; // enables BDD construction when other methods fail + int fVerbose; // prints verbose stats // iterations - int nItersMax; // the number of iterations + int nItersMax; // the number of iterations // mitering - int nMiteringLimitStart; // starting mitering limit - float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration + int nMiteringLimitStart; // starting mitering limit + float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration // rewriting - int nRewritingLimitStart; // the number of rewriting iterations - float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration + int nRewritingLimitStart; // the number of rewriting iterations + float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration // fraiging - int nFraigingLimitStart; // starting backtrack(conflict) limit - float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration + int nFraigingLimitStart; // starting backtrack(conflict) limit + float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration // last-gasp BDD construction - int nBddSizeLimit; // the number of BDD nodes when construction is aborted - int fBddReorder; // enables dynamic BDD variable reordering + int nBddSizeLimit; // the number of BDD nodes when construction is aborted + int fBddReorder; // enables dynamic BDD variable reordering // last-gasp mitering - int nMiteringLimitLast; // final mitering limit + int nMiteringLimitLast; // final mitering limit + // global SAT solver limits + sint64 nTotalBacktrackLimit; // global limit on the number of backtracks + sint64 nTotalInspectLimit; // global limit on the number of clause inspects + // global resources applied + sint64 nTotalBacktracksMade; // the total number of backtracks made + sint64 nTotalInspectsMade; // the total number of inspects made }; //////////////////////////////////////////////////////////////////////// @@ -137,6 +145,8 @@ extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ); extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ); extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ); extern int Fraig_ManReadSatFails( Fraig_Man_t * p ); +extern int Fraig_ManReadConflicts( Fraig_Man_t * p ); +extern int Fraig_ManReadInspects( Fraig_Man_t * p ); extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed ); extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack ); diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index b4bdbcab..79a7c224 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -66,6 +66,10 @@ int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } // returns the number of times FRAIG package timed out int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFailsReal; } +// returns the number of conflicts in the SAT solver +int Fraig_ManReadConflicts( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; } +// returns the number of inspections in the SAT solver +int Fraig_ManReadInspects( Fraig_Man_t * p ) { return p->pSat? Msat_SolverReadInspects(p->pSat) : 0; } /**Function************************************************************* diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 4ebb9a9f..89bc924f 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -49,6 +49,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 ) { Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr; + int fUseSatCheck; // int RetValue; // check for trivial cases @@ -167,7 +168,8 @@ 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, 1000000 ) ) + fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); + if ( fUseSatCheck && 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 8e016331..9c6e0d47 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -66,7 +66,7 @@ // the bit masks #define FRAIG_MASK(n) ((~((unsigned)0)) >> (32-(n))) #define FRAIG_FULL (~((unsigned)0)) -#define FRAIG_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0)) +#define FRAIG_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0)) // maximum/minimum operators #define FRAIG_MIN(a,b) (((a) < (b))? (a) : (b)) @@ -152,6 +152,7 @@ struct Fraig_ManStruct_t_ int fTryProve; // tries to solve the final miter int fVerbose; // the verbosiness flag int fVerboseP; // the verbosiness flag + sint64 nInspLimit; // the inspection limit int nTravIds; // the traversal counter int nTravIds2; // the traversal counter diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 3268ac3a..ffb51a07 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -42,10 +42,12 @@ int timeAssign; ***********************************************************************/ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) { + // clean the parameter structure + memset( pParams, 0, sizeof(Prove_Params_t) ); // general parameters pParams->fUseFraiging = 1; // enables fraiging pParams->fUseRewriting = 1; // enables rewriting - pParams->fUseBdds = 1; // enables BDD construction when other methods fail + pParams->fUseBdds = 0; // enables BDD construction when other methods fail pParams->fVerbose = 0; // prints verbose stats // iterations pParams->nItersMax = 6; // the number of iterations @@ -63,6 +65,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) pParams->fBddReorder = 1; // enables dynamic BDD variable reordering // last-gasp mitering pParams->nMiteringLimitLast = 1000000; // final mitering limit + // global SAT solver limits + pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks + pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects } /**Function************************************************************* @@ -92,6 +97,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbose flag for reporting the proof pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections } /**Function************************************************************* @@ -121,6 +128,8 @@ void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbose flag for reporting the proof pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections } /**Function************************************************************* @@ -176,6 +185,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice) p->fVerbose = pParams->fVerbose; // disable verbose output p->fVerboseP = pParams->fVerboseP; // disable verbose output + p->nInspLimit = pParams->nInspLimit; // the limit on the number of inspections // start memory managers p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) ); -- cgit v1.2.3