Version abc60611

5 files changed, 46 insertions, 19 deletions

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) );