Version abc60407

7 files changed, 123 insertions, 9 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 4e2a295e..d6215465 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -41,6 +41,7 @@ typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
 typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
 typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;
 typedef struct Fraig_PatternsStruct_t_    Fraig_Patterns_t;
+typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
 
 struct Fraig_ParamsStruct_t_
 {
@@ -61,6 +62,31 @@ struct Fraig_ParamsStruct_t_
     int  fInternal;     // is set to 1 for internal fraig calls
 };
 
+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
+    // iterations
+    int   nItersMax;             // the number of iterations
+    // mitering 
+    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
+    // fraiging 
+    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
+    // last-gasp mitering
+    int   nMiteringLimitLast;    // final mitering limit
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                       GLOBAL VARIABLES                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -155,6 +181,7 @@ extern Fraig_Node_t *      Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode,
 extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );
 
 /*=== fraigMan.c =============================================================*/
+extern void                Prove_ParamsSetDefault( Prove_Params_t * pParams );
 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
 extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index 3b8da17f..b4bdbcab 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -65,7 +65,7 @@ int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           {
 // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
 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->nSatFails;        }      
+int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFailsReal;    }      
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 890af13c..8e016331 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -189,7 +189,8 @@ struct Fraig_ManStruct_t_
     int                   nSatCalls;     // the number of times equivalence checking was called
     int                   nSatProof;     // the number of times a proof was found
     int                   nSatCounter;   // the number of times a counter example was found
-    int                   nSatFails;     // the number of times the SAT solver failed to complete
+    int                   nSatFails;     // the number of times the SAT solver failed to complete due to resource limit or prediction
+    int                   nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
 
     int                   nSatCallsImp;  // the number of times equivalence checking was called
     int                   nSatProofImp;  // the number of times a proof was found
@@ -243,8 +244,9 @@ struct Fraig_NodeStruct_t_
     unsigned              fMark3   :  1; // the mark used for traversals
     unsigned              fFeedUse :  1; // the presence of the variable in the feedback
     unsigned              fFeedVal :  1; // the value of the variable in the feedback
+    unsigned              fFailTfo :  1; // the node is in the TFO of the failed SAT run
     unsigned              nFanouts :  2; // the indicator of fanouts (none, one, or many)
-    unsigned              nOnes    : 21; // the number of 1's in the random sim info
+    unsigned              nOnes    : 20; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index ff6faa33..3268ac3a 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -40,6 +40,42 @@ int timeAssign;
   SeeAlso     []
 
 ***********************************************************************/
+void Prove_ParamsSetDefault( Prove_Params_t * pParams )
+{
+    // general parameters
+    pParams->fUseFraiging         = 1;       // enables fraiging
+    pParams->fUseRewriting        = 1;       // enables rewriting
+    pParams->fUseBdds             = 1;       // enables BDD construction when other methods fail
+    pParams->fVerbose             = 0;       // prints verbose stats
+    // iterations
+    pParams->nItersMax            = 6;       // the number of iterations
+    // mitering 
+    pParams->nMiteringLimitStart  = 1000;    // starting mitering limit
+    pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    pParams->nRewritingLimitStart = 3;       // the number of rewriting iterations
+    pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
+    pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
+    pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for equivalence checking.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 {
     memset( pParams, 0, sizeof(Fraig_Params_t) );
@@ -271,8 +307,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
         (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
     printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
         p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
-    printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
     printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", 
         Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
     if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 84509e9e..6e3d3c7d 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -176,6 +176,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_
     // compute the level of this node
     pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
+    pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
 
     // derive the simulation info 
 clk = clock();
diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c
index 9745b7e6..127ad478 100644
--- a/src/sat/fraig/fraigPrime.c
+++ b/src/sat/fraig/fraigPrime.c
@@ -22,7 +22,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// The 1,000 smallest prime numbers used to compute the hash value
+// The 1,024 smallest prime numbers used to compute the hash value
 // http://www.math.utah.edu/~alfeld/math/primelist.html
 int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, 
 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
@@ -93,7 +93,9 @@ int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5,
 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
-7877, 7879, 7883, 7901, 7907, 7919 };
+7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
+8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
+8147, 8161 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index d4358772..aa28a4f2 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "fraigInt.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -304,6 +305,20 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
     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);
+    }
+
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
@@ -394,13 +409,27 @@ 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 );
         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++;
+        p->nSatFailsReal++;
         return 0;
     }
 
@@ -454,17 +483,34 @@ 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 );
         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
+        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 );
     return 1;
 }