Version abc80130_2

15 files changed, 1063 insertions, 104 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 901bbac9..1dad21e2 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -18,11 +18,26 @@
 
 #ifndef __FRAIG_H__
 #define __FRAIG_H__
- 
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef SINT64
+#define SINT64
+
+#ifdef _WIN32
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
+#else
+typedef long long          sint64;
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,12 +52,14 @@ 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_
 {
     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
@@ -52,6 +69,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
+    // 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 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
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -59,14 +109,14 @@ struct Fraig_ParamsStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
 // macros working with complemented attributes of the nodes
-#define Fraig_IsComplement(p)    (((int)((long) (p) & 01)))
-#define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned)(p) & ~01)) 
-#define Fraig_Not(p)             ((Fraig_Node_t *)((long)(p) ^ 01)) 
-#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((long)(p) ^ (c)))
+#define Fraig_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
+#define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned long)(p) & ~01)) 
+#define Fraig_Not(p)             ((Fraig_Node_t *)((unsigned long)(p) ^ 01)) 
+#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))
 
 // these are currently not used
 #define Fraig_Ref(p)              
@@ -74,7 +124,7 @@ struct Fraig_ParamsStruct_t_
 #define Fraig_RecursiveDeref(p,c)
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraigApi.c =============================================================*/
@@ -103,6 +153,9 @@ extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
 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 );      
@@ -147,10 +200,15 @@ 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 );
 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
+extern Fraig_NodeVec_t *   Fraig_ManGetSimInfo( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
+extern void                Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
 
 /*=== fraigDfs.c =============================================================*/
 extern Fraig_NodeVec_t *   Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
@@ -162,10 +220,11 @@ 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 );
+extern int                 Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
@@ -200,4 +259,9 @@ extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ 
+#ifdef __cplusplus
+}
+#endif
+
 #endif
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index b92f6afd..79a7c224 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -64,6 +64,12 @@ int               Fraig_ManReadPatternNumRandom( Fraig_Man_t * p )            {
 int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           { return p->iWordStart * 32;  }
 // 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->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 5a7d0563..89bc924f 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -24,7 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,7 +49,8 @@
 Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 )
 {
     Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
-    int RetValue;
+    int fUseSatCheck;
+//    int RetValue;
 
     // check for trivial cases
     if ( p1 == p2 )
@@ -68,7 +69,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
             return p1;
         return Fraig_Not(pMan->pConst1);
     }
-
+/*
     // check for less trivial cases
     if ( Fraig_IsComplement(p1) )
     {
@@ -125,7 +126,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
             return Fraig_Not(pMan->pConst1);
         }
     }
-
+*/
     // perform level-one structural hashing
     if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
     {
@@ -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 ) )
+    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/fraigChoice.c b/src/sat/fraig/fraigChoice.c
new file mode 100644
index 00000000..896e5d2d
--- /dev/null
+++ b/src/sat/fraig/fraigChoice.c
@@ -0,0 +1,241 @@
+/**CFile****************************************************************
+
+  FileName    [fraigTrans.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Adds the additive and distributive choices to the AIG.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fraigTrans.c,v 1.1 2005/02/28 05:34:34 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fraigInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds choice nodes based on associativity.]
+
+  Description [Make nLimit big AND gates and add all decompositions
+               to the Fraig.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit )
+{
+//    ProgressBar * pProgress;
+    char Buffer[100];
+    int clkTotal = clock();
+    int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes;
+    int /*nMaxLevel,*/ nDistributive;
+    Fraig_Node_t *pNode, *pRepr;
+    Fraig_Node_t *pX, *pA, *pB, *pC, /* *pD,*/ *pN, /* *pQ, *pR,*/ *pT;
+    int fShortCut = 0;
+
+    nDistributive = 0;
+
+//    Fraig_ManSetApprox( pMan, 1 );
+
+    // NO functional reduction
+    if (fShortCut) Fraig_ManSetFuncRed( pMan, 0 );
+
+    // First we mark critical functions i.e. compute those
+    // nodes which lie on the critical path. Note that this
+    // doesn't update the required times on any choice nodes
+    // which are not the representatives
+/*
+    nMaxLevel = Fraig_GetMaxLevel( pMan );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+    {
+        Fraig_SetNodeRequired( pMan, pMan->pOutputs[i], nMaxLevel );
+    }
+*/
+    nNodesBefore = Fraig_ManReadNodeNum( pMan );
+    nInputs      = Fraig_ManReadInputNum( pMan );
+    nMaxNodes    = nInputs + nLimit * ( nNodesBefore - nInputs );
+
+    printf ("Limit = %d, Before = %d\n", nMaxNodes, nNodesBefore );
+
+    if (0) 
+    {
+        char buffer[128];
+        sprintf (buffer, "test" );
+//        Fraig_MappingShow( pMan, buffer );
+    }
+
+//    pProgress = Extra_ProgressBarStart( stdout, nMaxNodes );
+Fraig_ManCheckConsistency( pMan );
+
+    for ( i = nInputs+1; (i < Fraig_ManReadNodeNum( pMan )) 
+            && (nMaxNodes > Fraig_ManReadNodeNum( pMan )); ++i )
+    {
+//        if ( i == nNodesBefore )
+//            break;
+
+        pNode = Fraig_ManReadIthNode( pMan, i );
+        assert ( pNode );
+
+        pRepr = pNode->pRepr ? pNode->pRepr : pNode;
+        //printf ("Slack: %d\n", Fraig_NodeReadSlack( pRepr ));
+        
+        // All the new associative choices we add will have huge slack
+        // since we do not redo timing, and timing doesnt handle choices
+        // well anyway. However every newly added node is a choice of an
+        // existing critical node, so they are considered critical.
+//        if ( (Fraig_NodeReadSlack( pRepr ) > 3) && (i < nNodesBefore)  )     
+//            continue;
+
+//        if ( pNode->pRepr )
+//            continue;
+
+        // Try ((ab)c), x = ab -> (a(bc)) and (b(ac))
+        pX = Fraig_NodeReadOne(pNode);
+        pC = Fraig_NodeReadTwo(pNode);
+        if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX))
+        {
+            pA = Fraig_NodeReadOne(Fraig_Regular(pX));
+            pB = Fraig_NodeReadTwo(Fraig_Regular(pX));
+
+//            pA = Fraig_NodeGetRepr( pA );
+//            pB = Fraig_NodeGetRepr( pB );
+//            pC = Fraig_NodeGetRepr( pC );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pB, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pA, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, pA, Fraig_NodeAnd(pMan, pB, pC));
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pB, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, pB, Fraig_NodeAnd(pMan, pA, pC));
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+        }
+
+
+        // Try (a(bc)), x = bc -> ((ab)c) and ((ac)b)
+        pA = Fraig_NodeReadOne(pNode);
+        pX = Fraig_NodeReadTwo(pNode);
+        if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX))
+        {
+            pB = Fraig_NodeReadOne(Fraig_Regular(pX));
+            pC = Fraig_NodeReadTwo(Fraig_Regular(pX));
+
+//            pA = Fraig_NodeGetRepr( pA );
+//            pB = Fraig_NodeGetRepr( pB );
+//            pC = Fraig_NodeGetRepr( pC );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pB);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pC, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pB), pC);
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pB, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pC), pB);
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+        }
+
+
+/*
+        // Try distributive transform
+        pQ = Fraig_NodeReadOne(pNode);
+        pR = Fraig_NodeReadTwo(pNode);
+        if ( (Fraig_IsComplement(pQ) && Fraig_NodeIsAnd(pQ))
+             && (Fraig_IsComplement(pR) && Fraig_NodeIsAnd(pR)) )
+        {
+            pA = Fraig_NodeReadOne(Fraig_Regular(pQ));
+            pB = Fraig_NodeReadTwo(Fraig_Regular(pQ));
+            pC = Fraig_NodeReadOne(Fraig_Regular(pR));
+            pD = Fraig_NodeReadTwo(Fraig_Regular(pR));
+
+            // Now detect the !(xy + xz) pattern, store 
+            // x in pA, y in pB and z in pC and set pD = 0 to indicate
+            // pattern was found
+            assert (pD != 0);
+            if (pA == pC) { pC = pD;                   pD = 0; } 
+            if (pA == pD) {                            pD = 0; } 
+            if (pB == pC) { pB = pA; pA = pC; pC = pD; pD = 0; }
+            if (pB == pD) { pB = pA; pA = pD;          pD = 0; }
+            if (pD == 0)
+            {
+                nDistributive++;
+                pN = Fraig_Not(Fraig_NodeAnd(pMan, pA, 
+                        Fraig_NodeOr(pMan, pB, pC)));
+                if (fShortCut) Fraig_NodeAddChoice( pMan, pNode, pN );
+                // assert ( Fraig_NodesEqual(pN, pNode) );
+            }
+        }
+*/            
+        if ( i % 1000 == 0 )
+        {
+            sprintf( Buffer, "Adding choice %6d...", i - nNodesBefore );
+//            Extra_ProgressBarUpdate( pProgress, i, Buffer );
+        }
+    }
+
+//    Extra_ProgressBarStop( pProgress );
+
+Fraig_ManCheckConsistency( pMan );
+
+    nNodesAfter = Fraig_ManReadNodeNum( pMan );
+    printf ( "Nodes before = %6d. Nodes with associative choices = %6d. Increase = %4.2f %%.\n", 
+            nNodesBefore, nNodesAfter, ((float)(nNodesAfter - nNodesBefore)) * 100.0/(nNodesBefore - nInputs) );
+    printf ( "Distributive = %d\n", nDistributive );
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/fraig/fraigFanout.c b/src/sat/fraig/fraigFanout.c
index b44bacd7..789bffca 100644
--- a/src/sat/fraig/fraigFanout.c
+++ b/src/sat/fraig/fraigFanout.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 73640387..8a3cc6c7 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -37,7 +37,7 @@ static void  Fraig_ReallocateSimulationInfo( Fraig_Man_t * p );
 
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -463,6 +463,10 @@ Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p )
             Fraig_NodeVecPush( p->vCones, pEntD );
         if ( p->vCones->nSize == 1 )
             continue;
+        //////////////////////////////// bug fix by alanmi, September 14, 2006
+        if ( p->vCones->nSize > 20 ) 
+            continue;
+        ////////////////////////////////
 
         for ( k = 0; k < p->vCones->nSize; k++ )
             for ( m = k+1; m < p->vCones->nSize; m++ )
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 131b750c..9c6e0d47 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -47,7 +47,7 @@
 */
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
 // enable this macro to support the fanouts
@@ -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))
@@ -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
@@ -151,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
@@ -188,7 +190,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
@@ -242,8 +245,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
@@ -279,9 +283,9 @@ struct Fraig_NodeStruct_t_
 // the vector of nodes
 struct Fraig_NodeVecStruct_t_
 {
-    Fraig_Node_t **       pArray;        // the array of nodes
-    int                   nSize;         // the number of entries in the array
     int                   nCap;          // the number of allocated entries
+    int                   nSize;         // the number of entries in the array
+    Fraig_Node_t **       pArray;        // the array of nodes
 };
 
 // the hash table 
@@ -364,7 +368,7 @@ struct Fraig_HashTableStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraigCanon.c =============================================================*/
@@ -380,6 +384,8 @@ extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
 extern int *               Fraig_ManAllocCounterExample( Fraig_Man_t * p );
 extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
+/*=== fraigMan.c =============================================================*/
+extern void                Fraig_ManCreateSolver( Fraig_Man_t * p );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
@@ -438,8 +444,8 @@ extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig
 /*=== fraigVec.c ===============================================================*/
 extern void                Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index e5979c93..7fd937d5 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -26,7 +26,7 @@ int timeSelect;
 int timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -40,12 +40,89 @@ int timeAssign;
   SeeAlso     []
 
 ***********************************************************************/
+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             = 0;       // enables BDD construction when other methods fail
+    pParams->fVerbose             = 0;       // prints verbose stats
+    // iterations
+    pParams->nItersMax            = 6;       // the number of iterations
+    // mitering 
+    pParams->nMiteringLimitStart  = 300;    // starting mitering limit
+    pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
+    // rewriting (currently not used)
+    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
+    pParams->nMiteringLimitLast   = 0;       // 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
+//    pParams->nTotalInspectLimit   = 100000000;  // global limit on the number of clause inspects
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints out the current values of CEC engine parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Prove_ParamsPrint( Prove_Params_t * pParams )
+{
+    printf( "CEC enging parameters:\n" );
+    printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
+    printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
+    printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
+    printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
+    printf( "Solver iterations: %d\n", pParams->nItersMax );
+    printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
+    printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
+    printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
+    printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
+    printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
+    printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
+    printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
+    printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
+    printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
+    printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
+    printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
+    printf( "Parameter dump complete.\n" );
+}
+
+/**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) );
     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
@@ -55,6 +132,39 @@ 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*************************************************************
+
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for complete FRAIGing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
+{
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
+    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   = -1;                     // 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
+    pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
+    pParams->fChoicing  =  0;                     // enables recording structural choices
+    pParams->fTryProve  =  0;                     // tries to solve the final miter
+    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*************************************************************
@@ -74,7 +184,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     Fraig_Man_t * p;
 
     // set the random seed for simulation
-    srand( 0xFEEDDEAF );
+//    srand( 0xFEEDDEAF );
+    srand( 0xDEADCAFE );
 
     // set parameters for equivalence checking
     if ( pParams == NULL )
@@ -100,6 +211,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)
@@ -108,6 +220,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) );
@@ -153,7 +266,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
 //        Fraig_TablePrintStatsF( p );
 //        Fraig_TablePrintStatsF0( p );
     }
-
+ 
     for ( i = 0; i < p->vNodes->nSize; i++ )
         if ( p->vNodes->pArray[i]->vFanins )
         {
@@ -194,6 +307,31 @@ void Fraig_ManFree( Fraig_Man_t * p )
     FREE( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares the SAT solver to run on the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManCreateSolver( Fraig_Man_t * p )
+{
+    extern int timeSelect;
+    extern int timeAssign;
+    assert( p->pSat == NULL );
+    // 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;
+}
+
  
 /**Function*************************************************************
 
@@ -214,8 +352,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 );
@@ -233,6 +371,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
 //    PRT( "Assignment", timeAssign );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation information for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+{
+    Fraig_NodeVec_t * vInfo;
+    unsigned * pUnsigned;
+    int i;
+    assert( nSize > 0 && nWords > 0 );
+    vInfo = Fraig_NodeVecAlloc( nSize );
+    pUnsigned = ALLOC( unsigned, nSize * nWords );
+    vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
+    if ( fClean )
+        memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
+    for ( i = 1; i < nSize; i++ )
+        vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
+    vInfo->nSize = nSize;
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns simulation info of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
+{
+    Fraig_NodeVec_t * vInfo;
+    Fraig_Node_t * pNode;
+    unsigned * pUnsigned;
+    int nRandom, nDynamic;
+    int i, k, nWords;
+
+    nRandom  = Fraig_ManReadPatternNumRandom( p );
+    nDynamic = Fraig_ManReadPatternNumDynamic( p );
+    nWords = nRandom / 32 + nDynamic / 32;
+
+    vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
+    for ( i = 0; i < p->vNodes->nSize; i++ )
+    {
+        pNode = p->vNodes->pArray[i];
+        assert( i == pNode->Num );
+        pUnsigned = (unsigned *)vInfo->pArray[i];
+        for ( k = 0; k < nRandom / 32; k++ )
+            pUnsigned[k] = pNode->puSimR[k];
+        for ( k = 0; k < nDynamic / 32; k++ )
+            pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
+    }
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if A v B is always true based on the siminfo.]
+
+  Description [A v B is always true iff A' * B' is always false.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
+{
+    int fCompl1, fCompl2, i;
+
+    fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
+    fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
+
+    pNode1 = Fraig_Regular(pNode1);
+    pNode2 = Fraig_Regular(pNode2);
+    assert( pNode1 != pNode2 );
+    
+    // check the simulation info
+    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( !fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( fCompl1 && !fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+//    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses to the solver.]
+
+  Description [This procedure is used to add external clauses to the solver.
+  The clauses are given by sets of nodes. Each node stands for one literal.
+  If the node is complemented, the literal is negated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
+{
+    Fraig_Node_t * pNode;
+    int i, fComp, RetValue;
+    if ( p->pSat == NULL )
+        Fraig_ManCreateSolver( p );
+    // create four clauses
+    Msat_IntVecClear( p->vProj );
+    for ( i = 0; i < nNodes; i++ )
+    {
+        pNode = Fraig_Regular(ppNodes[i]);
+        fComp = Fraig_IsComplement(ppNodes[i]);
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
+//        printf( "%d(%d) ", pNode->Num, fComp );
+    }
+//    printf( "\n" );
+    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+    assert( RetValue );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c
index dbf42da4..500431c6 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -43,7 +43,7 @@ struct Fraig_MemFixed_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index a6c1d5a6..6e3d3c7d 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -26,7 +26,7 @@
 #define Fraig_NodeIsSimComplement(p) (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -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 0f37a586..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,10 +93,12 @@ 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function********************************************************************
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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index d0f22acd..b68bbe0e 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -26,7 +26,7 @@ static void Fraig_TableResizeS( Fraig_HashTable_t * p );
 static void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 2155c4a3..342a7111 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -38,7 +38,7 @@ static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeV
 static int  Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c
index 2e2603b0..ba3feecd 100644
--- a/src/sat/fraig/fraigVec.c
+++ b/src/sat/fraig/fraigVec.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************