Version abc80130

15 files changed, 104 insertions, 1063 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 1dad21e2..901bbac9 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -18,26 +18,11 @@
 
 #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                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -52,14 +37,12 @@ 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
@@ -69,39 +52,6 @@ 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
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -109,14 +59,14 @@ struct Prove_ParamsStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
  
 // macros working with complemented attributes of the nodes
-#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)))
+#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)))
 
 // these are currently not used
 #define Fraig_Ref(p)              
@@ -124,7 +74,7 @@ struct Prove_ParamsStruct_t_
 #define Fraig_RecursiveDeref(p,c)
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraigApi.c =============================================================*/
@@ -153,9 +103,6 @@ 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 );      
@@ -200,15 +147,10 @@ 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 );
@@ -220,11 +162,10 @@ 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, int nTimeLimit );
-extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
+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 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 );
@@ -259,9 +200,4 @@ 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 79a7c224..b92f6afd 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -64,12 +64,6 @@ 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 89bc924f..5a7d0563 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -24,7 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,8 +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;
+    int RetValue;
 
     // check for trivial cases
     if ( p1 == p2 )
@@ -69,7 +68,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) )
     {
@@ -126,7 +125,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
     {
@@ -168,8 +167,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
     // there is another node which looks the same according to simulation
 
     // use SAT to resolve the ambiguity
-    fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); 
-    if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
+    if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit ) )
     {
         // 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
deleted file mode 100644
index 896e5d2d..00000000
--- a/src/sat/fraig/fraigChoice.c
+++ /dev/null
@@ -1,241 +0,0 @@
-/**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 789bffca..b44bacd7 100644
--- a/src/sat/fraig/fraigFanout.c
+++ b/src/sat/fraig/fraigFanout.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 8a3cc6c7..73640387 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -463,10 +463,6 @@ 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 9c6e0d47..131b750c 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -47,7 +47,7 @@
 */
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
  
 // 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)>>5) + (((n)&31) > 0))
+#define FRAIG_NUM_WORDS(n)         ((n)/32 + (((n)%32) > 0))
 
 // maximum/minimum operators
 #define FRAIG_MIN(a,b)             (((a) < (b))? (a) : (b))
@@ -143,7 +143,6 @@ 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
@@ -152,7 +151,6 @@ 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
@@ -190,8 +188,7 @@ 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 due to resource limit or prediction
-    int                   nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
+    int                   nSatFails;     // the number of times the SAT solver failed to complete
 
     int                   nSatCallsImp;  // the number of times equivalence checking was called
     int                   nSatProofImp;  // the number of times a proof was found
@@ -245,9 +242,8 @@ 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    : 20; // the number of 1's in the random sim info
+    unsigned              nOnes    : 21; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child
@@ -283,9 +279,9 @@ struct Fraig_NodeStruct_t_
 // the vector of nodes
 struct Fraig_NodeVecStruct_t_
 {
-    int                   nCap;          // the number of allocated entries
-    int                   nSize;         // the number of entries in the array
     Fraig_Node_t **       pArray;        // the array of nodes
+    int                   nSize;         // the number of entries in the array
+    int                   nCap;          // the number of allocated entries
 };
 
 // the hash table 
@@ -368,7 +364,7 @@ struct Fraig_HashTableStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraigCanon.c =============================================================*/
@@ -384,8 +380,6 @@ 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 );
@@ -444,8 +438,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 7fd937d5..e5979c93 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -26,7 +26,7 @@ int timeSelect;
 int timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -40,89 +40,12 @@ 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
@@ -132,39 +55,6 @@ 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*************************************************************
@@ -184,8 +74,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     Fraig_Man_t * p;
 
     // set the random seed for simulation
-//    srand( 0xFEEDDEAF );
-    srand( 0xDEADCAFE );
+    srand( 0xFEEDDEAF );
 
     // set parameters for equivalence checking
     if ( pParams == NULL )
@@ -211,7 +100,6 @@ 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)
@@ -220,7 +108,6 @@ 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) );
@@ -266,7 +153,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 )
         {
@@ -307,31 +194,6 @@ 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*************************************************************
 
@@ -352,8 +214,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. FailReal = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCounter, p->nSatFails, 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 );
@@ -371,168 +233,6 @@ 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 500431c6..dbf42da4 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -43,7 +43,7 @@ struct Fraig_MemFixed_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
     int i;
     char * pTemp;
 
-    // deallocate all chunks except the first one
+    // delocate 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 6e3d3c7d..a6c1d5a6 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -176,7 +176,6 @@ 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 127ad478..0f37a586 100644
--- a/src/sat/fraig/fraigPrime.c
+++ b/src/sat/fraig/fraigPrime.c
@@ -22,7 +22,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// The 1,024 smallest prime numbers used to compute the hash value
+// The 1,000 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,12 +93,10 @@ 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, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
-8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
-8147, 8161 };
+7877, 7879, 7883, 7901, 7907, 7919 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function********************************************************************
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 53057fc3..17201e58 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -17,7 +17,6 @@
 ***********************************************************************/
 
 #include "fraigInt.h"
-#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -34,7 +33,6 @@ 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 );
 
@@ -43,10 +41,8 @@ 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -60,13 +56,13 @@ static int nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit )
+int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
 {
     if ( pNode1 == pNode2 )
         return 1;
     if ( pNode1 == Fraig_Not(pNode2) )
         return 0;
-    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
+    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit );
 }
 
 /**Function*************************************************************
@@ -99,9 +95,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, p->nSeconds ) )
+        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) )
         {
-            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
+            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
             else
                 p->vOutputs->pArray[i] = p->pConst1;
@@ -109,7 +105,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 );
     }
 }
 
@@ -127,158 +123,26 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
-    int i;
     FREE( p->pModel );
-    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 )
+    // 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) )
         return 1;
-    // skip the boundary node
-    if ( pNode->TravId == pMan->nTravIds-1 )
+    // consider the special case when the miter is constant 1
+    if ( pNode == p->pConst1 )
     {
-        pNode->TravId = pMan->nTravIds;
-        return 1;
-    }
-    pNode->TravId = pMan->nTravIds;
-    // skip the PI node
-    if ( pNode->NumPi >= 0 )
+        // 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;
-    // 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;
     }
-
-    // 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? '+':'-' );
+    // 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;
 }
 
 
@@ -296,40 +160,34 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
+int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
 {
     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 )
-        Fraig_ManCreateSolver( p );
+    {
+        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;
+    }
     // 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 );
+        Msat_SolverAddVar( p->pSat );
 
 
  
@@ -341,26 +199,17 @@ 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 );
@@ -371,18 +220,14 @@ 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, nTimeLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
@@ -415,31 +260,13 @@ 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;
-
-//        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++;
+        p->nSatFails++;
         return 0;
     }
 
@@ -459,9 +286,8 @@ 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, nTimeLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
-
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += clock() - clk;
@@ -493,42 +319,17 @@ 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;
-
-//        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++;
+        p->nSatFails++;
         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;
 }
 
@@ -558,12 +359,32 @@ 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 )
-        Fraig_ManCreateSolver( p );
+    {
+        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;
+    }
     // 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 );
+        Msat_SolverAddVar( p->pSat );
+
 
-   // get the logic cone
+/*
+    {
+        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
 clk = clock();
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
@@ -590,7 +411,7 @@ if ( fVerbose )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
@@ -622,8 +443,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 )
@@ -634,96 +455,6 @@ 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*************************************************************
@@ -755,7 +486,6 @@ 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 );
@@ -919,8 +649,6 @@ 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
             {
@@ -1255,33 +983,6 @@ 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 );
-
 }
 
 
@@ -1414,40 +1115,6 @@ 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 b68bbe0e..d0f22acd 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 342a7111..2155c4a3 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c
index ba3feecd..2e2603b0 100644
--- a/src/sat/fraig/fraigVec.c
+++ b/src/sat/fraig/fraigVec.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************