Version abc70930

17 files changed, 0 insertions, 5429 deletions

diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make
deleted file mode 100644
index 0dadfbe1..00000000
--- a/src/sat/msat/module.make
+++ /dev/null
@@ -1,13 +0,0 @@
-SRC +=  src/sat/msat/msatActivity.c \
-    src/sat/msat/msatClause.c \
-    src/sat/msat/msatClauseVec.c \
-    src/sat/msat/msatMem.c \
-    src/sat/msat/msatOrderJ.c \
-    src/sat/msat/msatQueue.c \
-    src/sat/msat/msatRead.c \
-    src/sat/msat/msatSolverApi.c \
-    src/sat/msat/msatSolverCore.c \
-    src/sat/msat/msatSolverIo.c \
-    src/sat/msat/msatSolverSearch.c \
-    src/sat/msat/msatSort.c \
-    src/sat/msat/msatVec.c
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
deleted file mode 100644
index 53353ba6..00000000
--- a/src/sat/msat/msat.h
+++ /dev/null
@@ -1,172 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msat.h]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [External definitions of the solver.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $]
-
-***********************************************************************/
-
-#ifndef __MSAT_H__
-#define __MSAT_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef bool
-#undef bool
-#endif
-
-#ifndef __MVTYPES_H__
-typedef int  bool;
-#endif
-
-typedef struct Msat_Solver_t_      Msat_Solver_t;
-
-// the vector of intergers and of clauses
-typedef struct Msat_IntVec_t_      Msat_IntVec_t;
-typedef struct Msat_ClauseVec_t_   Msat_ClauseVec_t;
-typedef struct Msat_VarHeap_t_     Msat_VarHeap_t;
-
-// the return value of the solver
-typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
-
-// representation of variables and literals
-// the literal (l) is the variable (v) and the sign (s)
-// s = 0 the variable is positive
-// s = 1 the variable is negative
-#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) 
-#define MSAT_LITNOT(l)    ((l)^1)
-#define MSAT_LITSIGN(l)   ((l)&1)     
-#define MSAT_LIT2VAR(l)   ((l)>>1)
-
-////////////////////////////////////////////////////////////////////////
-///                       GLOBAL VARIABLES                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DECLARATIONS                        ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== satRead.c ============================================================*/
-extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
-/*=== satSolver.c ===========================================================*/
-// adding vars, clauses, simplifying the database, and solving
-extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
-extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
-extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
-// printing stats, assignments, and clauses
-extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
-extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
-extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
-extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
-// access to the solver internal data
-extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
-extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
-extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
-extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
-extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
-extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
-extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
-extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
-extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
-extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
-extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
-extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
-extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
-extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
-extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
-// returns the solution after incremental solving
-extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
-extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
-extern Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p );
-extern Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p );
-extern Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p );
-/*=== satSolverSearch.c ===========================================================*/
-extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
-extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
-/*=== satSolverApi.c ===========================================================*/
-// allocation, cleaning, and freeing the solver
-extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose );
-extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
-extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
-extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
-extern void             Msat_SolverFree( Msat_Solver_t * p );
-/*=== satVec.c ===========================================================*/
-extern Msat_IntVec_t *  Msat_IntVecAlloc( int nCap );
-extern Msat_IntVec_t *  Msat_IntVecAllocArray( int * pArray, int nSize );
-extern Msat_IntVec_t *  Msat_IntVecAllocArrayCopy( int * pArray, int nSize );
-extern Msat_IntVec_t *  Msat_IntVecDup( Msat_IntVec_t * pVec );
-extern Msat_IntVec_t *  Msat_IntVecDupArray( Msat_IntVec_t * pVec );
-extern void             Msat_IntVecFree( Msat_IntVec_t * p );
-extern void             Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry );
-extern int *            Msat_IntVecReleaseArray( Msat_IntVec_t * p );
-extern int *            Msat_IntVecReadArray( Msat_IntVec_t * p );
-extern int              Msat_IntVecReadSize( Msat_IntVec_t * p );
-extern int              Msat_IntVecReadEntry( Msat_IntVec_t * p, int i );
-extern int              Msat_IntVecReadEntryLast( Msat_IntVec_t * p );
-extern void             Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry );
-extern void             Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin );
-extern void             Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew );
-extern void             Msat_IntVecClear( Msat_IntVec_t * p );
-extern void             Msat_IntVecPush( Msat_IntVec_t * p, int Entry );
-extern int              Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry );
-extern void             Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease );
-extern int              Msat_IntVecPop( Msat_IntVec_t * p );
-extern void             Msat_IntVecSort( Msat_IntVec_t * p, int fReverse );
-/*=== satHeap.c ===========================================================*/
-extern Msat_VarHeap_t * Msat_VarHeapAlloc();
-extern void             Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity );
-extern void             Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
-extern void             Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize );
-extern void             Msat_VarHeapStop( Msat_VarHeap_t * p );
-extern void             Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p );
-extern void             Msat_VarHeapCheck( Msat_VarHeap_t * p );
-extern void             Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar );
-extern int              Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar );
-extern void             Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar );  
-extern void             Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar );  
-extern void             Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar );  
-extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
-extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
-extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
-extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
- 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
deleted file mode 100644
index 1cd795bd..00000000
--- a/src/sat/msat/msatActivity.c
+++ /dev/null
@@ -1,160 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatActivity.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Procedures controlling activity of variables and clauses.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatActivity.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
-{
-    Msat_Var_t Var;
-    if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
-        return;
-    Var = MSAT_LIT2VAR(Lit);
-    p->pdActivity[Var] += p->dVarInc;
-//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
-    if ( p->pdActivity[Var] > 1e100 )
-        Msat_SolverVarRescaleActivity( p );
-    Msat_OrderUpdate( p->pOrder, Var );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverVarDecayActivity( Msat_Solver_t * p )
-{
-    if ( p->dVarDecay >= 0 )
-        p->dVarInc *= p->dVarDecay;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Divide all variable activities by 1e100.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverVarRescaleActivity( Msat_Solver_t * p )
-{
-    int i;
-    for ( i = 0; i < p->nVars; i++ )
-        p->pdActivity[i] *= 1e-100;
-    p->dVarInc *= 1e-100;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC )
-{
-    float Activ;
-    Activ = Msat_ClauseReadActivity(pC);
-    if ( Activ + p->dClaInc > 1e20 )
-    {
-        Msat_SolverClaRescaleActivity( p );
-        Activ = Msat_ClauseReadActivity( pC );
-    }
-    Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverClaDecayActivity( Msat_Solver_t * p )
-{
-    p->dClaInc *= p->dClaDecay;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Divide all constraint activities by 1e20.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverClaRescaleActivity( Msat_Solver_t * p )
-{
-    Msat_Clause_t ** pLearned;
-    int nLearned, i;
-    float Activ;
-    nLearned = Msat_ClauseVecReadSize( p->vLearned );
-    pLearned = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nLearned; i++ )
-    {
-        Activ = Msat_ClauseReadActivity( pLearned[i] );
-        Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 );
-    }
-    p->dClaInc *= 1e-20;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
deleted file mode 100644
index 2ba8cd32..00000000
--- a/src/sat/msat/msatClause.c
+++ /dev/null
@@ -1,529 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatClause.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Procedures working with SAT clauses.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatClause.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Msat_Clause_t_
-{
-    int           Num;              // unique number of the clause
-    unsigned      fLearned   :  1;  // 1 if the clause is learned
-    unsigned      fMark      :  1;  // used to mark visited clauses during proof recording
-    unsigned      fTypeA     :  1;  // used to mark clauses belonging to A for interpolant computation
-    unsigned      nSize      : 14;  // the number of literals in the clause
-    unsigned      nSizeAlloc : 15;  // the number of bytes allocated for the clause
-    Msat_Lit_t     pData[0];
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a new clause.]
-
-  Description [Returns FALSE if top-level conflict detected (must be handled); 
-  TRUE otherwise. 'pClause_out' may be set to NULL if clause is already 
-  satisfied by the top-level assignment.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out )
-{
-    int * pAssigns = Msat_SolverReadAssignsArray(p);
-    Msat_ClauseVec_t ** pvWatched;
-    Msat_Clause_t * pC;
-    int * pLits;
-    int nLits, i, j;
-    int nBytes;
-    Msat_Var_t Var;
-    bool Sign;
-
-    *pClause_out = NULL;
-
-    nLits = Msat_IntVecReadSize(vLits);
-    pLits = Msat_IntVecReadArray(vLits);
-
-    if ( !fLearned ) 
-    {
-        int * pSeen = Msat_SolverReadSeenArray( p );
-        int nSeenId;
-        assert( Msat_SolverReadDecisionLevel(p) == 0 );
-        // sorting literals makes the code trace-equivalent 
-        // with to the original C++ solver
-        Msat_IntVecSort( vLits, 0 );
-        // increment the counter of seen twice
-        nSeenId = Msat_SolverIncrementSeenId( p );
-        nSeenId = Msat_SolverIncrementSeenId( p );
-        // nSeenId - 1 stands for negative
-        // nSeenId     stands for positive
-        // Remove false literals
-
-        // there is a bug here!!!!
-        // when the same var in opposite polarities is given, it drops one polarity!!!
-
-        for ( i = j = 0; i < nLits; i++ ) {
-            // get the corresponding variable
-            Var  = MSAT_LIT2VAR(pLits[i]);
-            Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
-            // check if we already saw this variable in the this clause
-            if ( pSeen[Var] >= nSeenId - 1 )
-            {
-                if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
-                    continue;
-                return 1; // two opposite polarity lits -- don't add the clause
-            }
-            // mark the variable as seen
-            pSeen[Var] = nSeenId - !Sign;
-
-            // analize the value of this literal
-            if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
-            {
-                if ( pAssigns[Var] == pLits[i] )
-                    return 1;  // the clause is always true -- don't add anything
-                // the literal has no impact - skip it
-                continue;
-            }
-            // otherwise, add this literal to the clause
-            pLits[j++] = pLits[i];
-        }
-        Msat_IntVecShrink( vLits, j );
-        nLits = j;
-/*
-        // the problem with this code is that performance is very
-        // sensitive to the ordering of adjacency lits
-        // the best ordering requires fanins first, next fanouts
-        // this ordering is more convenient to make from FRAIG
-
-        // create the adjacency information
-        if ( nLits > 2 )
-        {
-            Msat_Var_t VarI, VarJ;
-            Msat_IntVec_t * pAdjI, * pAdjJ;
-
-            for ( i = 0; i < nLits; i++ )
-            {
-                VarI = MSAT_LIT2VAR(pLits[i]);
-                pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];
-
-                for ( j = i+1; j < nLits; j++ )
-                {
-                    VarJ = MSAT_LIT2VAR(pLits[j]);
-                    pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];
-
-                    Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
-                    Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
-                }
-            }
-        }
-*/
-    }
-    // 'vLits' is now the (possibly) reduced vector of literals.
-    if ( nLits == 0 )
-        return 0;
-    if ( nLits == 1 )
-        return Msat_SolverEnqueue( p, pLits[0], NULL );
-
-    // Allocate clause:
-//    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
-    nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
-#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    pC = (Msat_Clause_t *)ALLOC( char, nBytes );
-#else
-    pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
-#endif
-    pC->Num        = p->nClauses++;
-    pC->fTypeA     = 0;
-    pC->fMark      = 0;
-    pC->fLearned   = fLearned;
-    pC->nSize      = nLits;
-    pC->nSizeAlloc = nBytes;
-    memcpy( pC->pData, pLits, sizeof(int)*nLits );
-
-    // For learnt clauses only:
-    if ( fLearned )
-    {
-        int * pLevel = Msat_SolverReadDecisionLevelArray( p );
-        int iLevelMax, iLevelCur, iLitMax;
-
-        // Put the second watch on the literal with highest decision level:
-        iLitMax = 1;
-        iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
-        for ( i = 2; i < nLits; i++ )
-        {
-            iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
-            assert( iLevelCur != -1 );
-            if ( iLevelMax < iLevelCur )
-            // this is very strange - shouldn't it be???
-            // if ( iLevelMax > iLevelCur )
-                iLevelMax = iLevelCur, iLitMax = i;
-        }
-        pC->pData[1]       = pLits[iLitMax];
-        pC->pData[iLitMax] = pLits[1];
-
-        // Bumping:
-        // (newly learnt clauses should be considered active)
-        Msat_ClauseWriteActivity( pC, 0.0 );
-        Msat_SolverClaBumpActivity( p, pC ); 
-//        if ( nLits < 20 )
-        for ( i = 0; i < nLits; i++ )
-        {
-            Msat_SolverVarBumpActivity( p, pLits[i] );
-//            Msat_SolverVarBumpActivity( p, pLits[i] );
-//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
-        }
-    }
-
-    // Store clause:
-    pvWatched = Msat_SolverReadWatchedArray( p );
-    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
-    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
-    *pClause_out = pC;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched )
-{
-    if ( fRemoveWatched )
-    {
-        Msat_Lit_t Lit;
-        Msat_ClauseVec_t ** pvWatched;
-        pvWatched = Msat_SolverReadWatchedArray( p );
-        Lit = MSAT_LITNOT( pC->pData[0] );
-        Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
-        Lit = MSAT_LITNOT( pC->pData[1] );
-        Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
-    }
-
-#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    free( pC );
-#else
-    Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
-#endif
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Access the data field of the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool  Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
-int   Msat_ClauseReadSize( Msat_Clause_t * pC )     {  return pC->nSize;    }
-int * Msat_ClauseReadLits( Msat_Clause_t * pC )     {  return pC->pData;    }
-bool  Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
-int   Msat_ClauseReadNum( Msat_Clause_t * pC )      {  return pC->Num;      }
-bool  Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }
-
-void  Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark )   {  pC->fMark = fMark;   }
-void  Msat_ClauseSetNum( Msat_Clause_t * pC, int Num )       {  pC->Num = Num;       }
-void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTypeA; }
-
-/**Function*************************************************************
-
-  Synopsis    [Checks whether the learned clause is locked.]
-
-  Description [The clause may be locked if it is the reason of a
-  recent conflict. Such clause cannot be removed from the database.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
-{
-    Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
-    return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the activity of the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Msat_ClauseReadActivity( Msat_Clause_t * pC )
-{
-    return *((float *)(pC->pData + pC->nSize));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the activity of the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
-{
-    *((float *)(pC->pData + pC->nSize)) = Num;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propages the assignment.]
-
-  Description [The literal that has become true (Lit) is given to this 
-  procedure. The array of current variable assignments is given for
-  efficiency. The output literal (pLit_out) can be the second watched
-  literal (if TRUE is returned) or the conflict literal (if FALSE is 
-  returned). This messy interface is used to improve performance.
-  This procedure accounts for ~50% of the runtime of the solver.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
-{
-    // make sure the false literal is pC->pData[1]
-    Msat_Lit_t LitF = MSAT_LITNOT(Lit);
-    if ( pC->pData[0] == LitF )
-         pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
-    assert( pC->pData[1] == LitF );
-    // if the 0-th watch is true, clause is already satisfied
-    if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
-        return 1; 
-    // look for a new watch
-    if ( pC->nSize > 2 )
-    {
-        int i;
-        for ( i = 2; i < (int)pC->nSize; i++ )
-            if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
-            {
-                pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
-                *pLit_out = MSAT_LITNOT(pC->pData[1]);
-                return 1; 
-            }
-    }
-    // clause is unit under assignment
-    *pLit_out = pC->pData[0];
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simplifies the clause.]
-
-  Description [Assumes everything has been propagated! (esp. watches 
-  in clauses are NOT unsatisfied)]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
-{
-    Msat_Var_t Var;
-    int i, j;
-    for ( i = j = 0; i < (int)pC->nSize; i++ )
-    {
-        Var = MSAT_LIT2VAR(pC->pData[i]);
-        if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
-        {
-            pC->pData[j++] = pC->pData[i];
-            continue;
-        }
-        if ( pAssigns[Var] == pC->pData[i] )
-            return 1;
-        // otherwise, the value of the literal is false
-        // make sure, this literal is not watched
-        assert( i >= 2 );
-    }
-    // if the size has changed, update it and move activity
-    if ( j < (int)pC->nSize )
-    {
-        float Activ = Msat_ClauseReadActivity(pC);
-        pC->nSize = j;
-        Msat_ClauseWriteActivity(pC, Activ);
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes reason of conflict in the given clause.]
-
-  Description [If the literal is unassigned, finds the reason by 
-  complementing literals in the given cluase (pC). If the literal is
-  assigned, makes sure that this literal is the first one in the clause
-  and computes the complement of all other literals in the clause.
-  Returns the reason in the given array (vLits_out). If the clause is
-  learned, bumps its activity.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out )
-{
-    int i;
-    // clear the reason
-    Msat_IntVecClear( vLits_out );
-    assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
-    for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
-    {
-        assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
-        Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
-    }
-    if ( pC->fLearned ) 
-        Msat_SolverClaBumpActivity( p, pC );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes the given clause from the watched list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC )
-{
-    Msat_Clause_t ** pClauses;
-    int nClauses, i;
-    nClauses = Msat_ClauseVecReadSize( vClauses );
-    pClauses = Msat_ClauseVecReadArray( vClauses );
-    for ( i = 0; pClauses[i] != pC; i++ )
-        assert( i < nClauses );
-    for (      ; i < nClauses - 1; i++ )
-        pClauses[i] = pClauses[i+1];
-    Msat_ClauseVecPop( vClauses );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClausePrint( Msat_Clause_t * pC )
-{
-    int i;
-    if ( pC == NULL )
-        printf( "NULL pointer" );
-    else 
-    {
-        if ( pC->fLearned )
-            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
-        for ( i = 0; i < (int)pC->nSize; i++ )
-            printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the given clause in a file in DIMACS format.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement )
-{
-    int i;
-    for ( i = 0; i < (int)pC->nSize; i++ )
-        fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
-    if ( fIncrement )
-        fprintf( pFile, "0" );
-    fprintf( pFile, "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
-{
-    int i;
-    if ( pC == NULL )
-        printf( "NULL pointer" );
-    else 
-    {
-//        if ( pC->fLearned )
-//            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
-        for ( i = 0; i < (int)pC->nSize; i++ )
-            printf(" "L_LIT, L_lit(pC->pData[i]));
-    }
-    printf( "\n" );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
deleted file mode 100644
index 04691cf2..00000000
--- a/src/sat/msat/msatClauseVec.c
+++ /dev/null
@@ -1,232 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatClauseVec.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Procedures working with arrays of SAT clauses.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap )
-{
-    Msat_ClauseVec_t * p;
-    p = ALLOC( Msat_ClauseVec_t, 1 );
-    if ( nCap > 0 && nCap < 16 )
-        nCap = 16;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecFree( Msat_ClauseVec_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
-    p->nCap   = nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecClear( Msat_ClauseVec_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Msat_ClauseVecGrow( p, 16 );
-        else
-            Msat_ClauseVecGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p )
-{
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
deleted file mode 100644
index 03903abe..00000000
--- a/src/sat/msat/msatInt.h
+++ /dev/null
@@ -1,306 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatInt.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Internal definitions of the solver.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __MSAT_INT_H__
-#define __MSAT_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-//#include "leaks.h"       
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-#include <math.h>
-#include "msat.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef _MSC_VER
-typedef __int64     int64;
-#else
-typedef long long   int64;
-#endif
-
-// outputs the runtime in seconds
-#define PRT(a,t) \
-    printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
-
-// memory management macros
-#define ALLOC(type, num)    \
-    ((type *) malloc(sizeof(type) * (num)))
-#define REALLOC(type, obj, num)    \
-    ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num))))
-#define FREE(obj)        \
-    ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
-
-// By default, custom memory management is used
-// which guarantees constant time allocation/deallocation 
-// for SAT clauses and other frequently modified objects.
-// For debugging, it is possible use system memory management
-// directly. In which case, uncomment the macro below.
-//#define USE_SYSTEM_MEMORY_MANAGEMENT 
-
-// internal data structures
-typedef struct Msat_Clause_t_      Msat_Clause_t;
-typedef struct Msat_Queue_t_       Msat_Queue_t;
-typedef struct Msat_Order_t_       Msat_Order_t;
-// memory managers (duplicated from Extra for stand-aloneness)
-typedef struct Msat_MmFixed_t_     Msat_MmFixed_t;    
-typedef struct Msat_MmFlex_t_      Msat_MmFlex_t;     
-typedef struct Msat_MmStep_t_      Msat_MmStep_t;     
-// variables and literals
-typedef int                       Msat_Lit_t;  
-typedef int                       Msat_Var_t;  
-// the type of return value
-#define MSAT_VAR_UNASSIGNED (-1)
-#define MSAT_LIT_UNASSIGNED (-2)
-#define MSAT_ORDER_UNKNOWN  (-3)
-
-// printing the search tree
-#define L_IND      "%-*d"
-#define L_ind      Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
-#define L_LIT      "%s%d"
-#define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
-
-typedef struct Msat_SolverStats_t_ Msat_SolverStats_t;
-struct Msat_SolverStats_t_
-{
-    int64   nStarts;        // the number of restarts
-    int64   nDecisions;     // the number of decisions
-    int64   nPropagations;  // the number of implications
-    int64   nInspects;      // the number of times clauses are vising while watching them
-    int64   nConflicts;     // the number of conflicts
-    int64   nSuccesses;     // the number of sat assignments found
-};
-
-typedef struct Msat_SearchParams_t_ Msat_SearchParams_t;
-struct Msat_SearchParams_t_
-{
-    double  dVarDecay;
-    double  dClaDecay;
-};
-
-// sat solver data structure visible through all the internal files
-struct Msat_Solver_t_
-{
-    int                 nClauses;    // the total number of clauses
-    int                 nClausesStart; // the number of clauses before adding
-    Msat_ClauseVec_t *  vClauses;    // problem clauses
-    Msat_ClauseVec_t *  vLearned;    // learned clauses
-    double              dClaInc;     // Amount to bump next clause with.
-    double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
-
-    double *            pdActivity;  // A heuristic measurement of the activity of a variable.
-    float *             pFactors;    // the multiplicative factors of variable activity
-    double              dVarInc;     // Amount to bump next variable with.
-    double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
-    Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
-
-    Msat_ClauseVec_t ** pvWatched;   // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
-    Msat_Queue_t *      pQueue;      // Propagation queue.
-
-    int                 nVars;       // the current number of variables
-    int                 nVarsAlloc;  // the maximum allowed number of variables
-    int *               pAssigns;    // The current assignments (literals or MSAT_VAR_UNKOWN)
-    int *               pModel;      // The satisfying assignment
-    Msat_IntVec_t *     vTrail;      // List of assignments made. 
-    Msat_IntVec_t *     vTrailLim;   // Separator indices for different decision levels in 'trail'.
-    Msat_Clause_t **    pReasons;    // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
-    int *               pLevel;      // 'level[var]' is the decision level at which assignment was made. 
-    int                 nLevelRoot;  // Level of first proper decision.
-
-    double              dRandSeed;   // For the internal random number generator (makes solver deterministic over different platforms). 
-
-    bool                fVerbose;    // the verbosity flag
-    double              dProgress;   // Set by 'search()'.
-
-    // the variable cone and variable connectivity
-    Msat_IntVec_t *     vConeVars;
-    Msat_IntVec_t *     vVarsUsed;
-    Msat_ClauseVec_t *  vAdjacents;
-
-    // internal data used during conflict analysis
-    int *               pSeen;       // time when a lit was seen for the last time
-    int                 nSeenId;     // the id of current seeing
-    Msat_IntVec_t *     vReason;     // the temporary array of literals
-    Msat_IntVec_t *     vTemp;       // the temporary array of literals
-    int *               pFreq;       // the number of times each var participated in conflicts
-
-    // the memory manager
-    Msat_MmStep_t *     pMem;
-
-    // statistics
-    Msat_SolverStats_t  Stats;
-    int                 nTwoLits;
-    int                 nTwoLitsL;
-    int                 nClausesInit;
-    int                 nClausesAlloc;
-    int                 nClausesAllocL;
-    int                 nBackTracks;
-};
-
-struct Msat_ClauseVec_t_
-{
-    Msat_Clause_t **    pArray;
-    int                 nSize;
-    int                 nCap;
-};
-
-struct Msat_IntVec_t_
-{
-    int *               pArray;
-    int                 nSize;
-    int                 nCap;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                       GLOBAL VARIABLES                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DECLARATIONS                        ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== satActivity.c ===========================================================*/
-extern void                Msat_SolverVarDecayActivity( Msat_Solver_t * p );
-extern void                Msat_SolverVarRescaleActivity( Msat_Solver_t * p );
-extern void                Msat_SolverClaDecayActivity( Msat_Solver_t * p );
-extern void                Msat_SolverClaRescaleActivity( Msat_Solver_t * p );
-/*=== satSolverApi.c ===========================================================*/
-extern Msat_Clause_t *     Msat_SolverReadClause( Msat_Solver_t * p, int Num );
-/*=== satSolver.c ===========================================================*/
-extern int                 Msat_SolverReadDecisionLevel( Msat_Solver_t * p );
-extern int *               Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p );
-extern Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p );
-extern Msat_Type_t         Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var );
-extern Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p );
-extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p );
-extern int *               Msat_SolverReadSeenArray( Msat_Solver_t * p );
-extern int                 Msat_SolverIncrementSeenId( Msat_Solver_t * p );
-extern Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p );
-extern void                Msat_SolverClausesIncrement( Msat_Solver_t * p );
-extern void                Msat_SolverClausesDecrement( Msat_Solver_t * p );
-extern void                Msat_SolverClausesIncrementL( Msat_Solver_t * p );
-extern void                Msat_SolverClausesDecrementL( Msat_Solver_t * p );
-extern void                Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit );
-extern void                Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC );
-extern bool                Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
-extern double              Msat_SolverProgressEstimate( Msat_Solver_t * p );
-/*=== satSolverSearch.c ===========================================================*/
-extern bool                Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
-extern Msat_Clause_t *     Msat_SolverPropagate( Msat_Solver_t * p );
-extern void                Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
-extern Msat_Type_t         Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
-/*=== satQueue.c ===========================================================*/
-extern Msat_Queue_t *      Msat_QueueAlloc( int nVars );
-extern void                Msat_QueueFree( Msat_Queue_t * p );
-extern int                 Msat_QueueReadSize( Msat_Queue_t * p );
-extern void                Msat_QueueInsert( Msat_Queue_t * p, int Lit );
-extern int                 Msat_QueueExtract( Msat_Queue_t * p );
-extern void                Msat_QueueClear( Msat_Queue_t * p );
-/*=== satOrder.c ===========================================================*/
-extern Msat_Order_t *      Msat_OrderAlloc( Msat_Solver_t * pSat );
-extern void                Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax );
-extern void                Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone );
-extern int                 Msat_OrderCheck( Msat_Order_t * p );
-extern void                Msat_OrderFree( Msat_Order_t * p );
-extern int                 Msat_OrderVarSelect( Msat_Order_t * p );
-extern void                Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
-extern void                Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
-extern void                Msat_OrderUpdate( Msat_Order_t * p, int Var );
-/*=== satClause.c ===========================================================*/
-extern bool                Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out );
-extern Msat_Clause_t *     Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits );
-extern Msat_Clause_t *     Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit );
-extern bool                Msat_ClauseReadLearned( Msat_Clause_t * pC );
-extern int                 Msat_ClauseReadSize( Msat_Clause_t * pC );
-extern int *               Msat_ClauseReadLits( Msat_Clause_t * pC );
-extern bool                Msat_ClauseReadMark( Msat_Clause_t * pC );
-extern void                Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark );
-extern int                 Msat_ClauseReadNum( Msat_Clause_t * pC );
-extern void                Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
-extern bool                Msat_ClauseReadTypeA( Msat_Clause_t * pC );
-extern void                Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA );
-extern bool                Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
-extern float               Msat_ClauseReadActivity( Msat_Clause_t * pC );
-extern void                Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
-extern void                Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched );
-extern bool                Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
-extern bool                Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
-extern void                Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
-extern void                Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
-extern void                Msat_ClausePrint( Msat_Clause_t * pC );
-extern void                Msat_ClausePrintSymbols( Msat_Clause_t * pC );
-extern void                Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement );
-extern unsigned            Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
-/*=== satSort.c ===========================================================*/
-extern void                Msat_SolverSortDB( Msat_Solver_t * p );
-/*=== satClauseVec.c ===========================================================*/
-extern Msat_ClauseVec_t *  Msat_ClauseVecAlloc( int nCap );
-extern void                Msat_ClauseVecFree( Msat_ClauseVec_t * p );
-extern Msat_Clause_t **    Msat_ClauseVecReadArray( Msat_ClauseVec_t * p );
-extern int                 Msat_ClauseVecReadSize( Msat_ClauseVec_t * p );
-extern void                Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin );
-extern void                Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew );
-extern void                Msat_ClauseVecClear( Msat_ClauseVec_t * p );
-extern void                Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry );
-extern Msat_Clause_t *     Msat_ClauseVecPop( Msat_ClauseVec_t * p );
-extern void                Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry );
-extern Msat_Clause_t *     Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i );
-
-/*=== satMem.c ===========================================================*/
-// fixed-size-block memory manager
-extern Msat_MmFixed_t *    Msat_MmFixedStart( int nEntrySize );
-extern void                Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose );
-extern char *              Msat_MmFixedEntryFetch( Msat_MmFixed_t * p );
-extern void                Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry );
-extern void                Msat_MmFixedRestart( Msat_MmFixed_t * p );
-extern int                 Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p );
-// flexible-size-block memory manager
-extern Msat_MmFlex_t *     Msat_MmFlexStart();
-extern void                Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose );
-extern char *              Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes );
-extern int                 Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p );
-// hierarchical memory manager
-extern Msat_MmStep_t *     Msat_MmStepStart( int nSteps );
-extern void                Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose );
-extern char *              Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes );
-extern void                Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes );
-extern int                 Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
deleted file mode 100644
index 30bf4a96..00000000
--- a/src/sat/msat/msatMem.c
+++ /dev/null
@@ -1,529 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatMem.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Memory managers borrowed from Extra.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Msat_MmFixed_t_
-{
-    // information about individual entries
-    int           nEntrySize;    // the size of one entry
-    int           nEntriesAlloc; // the total number of entries allocated
-    int           nEntriesUsed;  // the number of entries in use
-    int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of free entries
-
-    // this is where the memory is stored
-    int           nChunkSize;    // the size of one chunk
-    int           nChunksAlloc;  // the maximum number of memory chunks 
-    int           nChunks;       // the current number of memory chunks 
-    char **       pChunks;       // the allocated memory
-
-    // statistics
-    int           nMemoryUsed;   // memory used in the allocated entries
-    int           nMemoryAlloc;  // memory allocated
-};
-
-struct Msat_MmFlex_t_
-{
-    // information about individual entries
-    int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to free memory
-    char *        pEnd;          // the first entry outside the free memory
-
-    // this is where the memory is stored
-    int           nChunkSize;    // the size of one chunk
-    int           nChunksAlloc;  // the maximum number of memory chunks 
-    int           nChunks;       // the current number of memory chunks 
-    char **       pChunks;       // the allocated memory
-
-    // statistics
-    int           nMemoryUsed;   // memory used in the allocated entries
-    int           nMemoryAlloc;  // memory allocated
-};
-
-
-struct Msat_MmStep_t_
-{
-    int                nMems;    // the number of fixed memory managers employed
-    Msat_MmFixed_t **   pMems;    // memory managers: 2^1 words, 2^2 words, etc
-    int                nMapSize; // the size of the memory array
-    Msat_MmFixed_t **   pMap;     // maps the number of bytes into its memory manager
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates memory pieces of fixed size.]
-
-  Description [The size of the chunk is computed as the minimum of
-  1024 entries and 64K. Can only work with entry size at least 4 byte long.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize )
-{
-    Msat_MmFixed_t * p;
-
-    p = ALLOC( Msat_MmFixed_t, 1 );
-    memset( p, 0, sizeof(Msat_MmFixed_t) );
-
-    p->nEntrySize    = nEntrySize;
-    p->nEntriesAlloc = 0;
-    p->nEntriesUsed  = 0;
-    p->pEntriesFree  = NULL;
-
-    if ( nEntrySize * (1 << 10) < (1<<16) )
-        p->nChunkSize = (1 << 10);
-    else
-        p->nChunkSize = (1<<16) / nEntrySize;
-    if ( p->nChunkSize < 8 )
-        p->nChunkSize = 8;
-
-    p->nChunksAlloc  = 64;
-    p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
-
-    p->nMemoryUsed   = 0;
-    p->nMemoryAlloc  = 0;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose )
-{
-    int i;
-    if ( p == NULL )
-        return;
-    if ( fVerbose )
-    {
-        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
-            p->nEntrySize, p->nChunkSize, p->nChunks );
-        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
-            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
-    }
-    for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p )
-{
-    char * pTemp;
-    int i;
-
-    // check if there are still free entries
-    if ( p->nEntriesUsed == p->nEntriesAlloc )
-    { // need to allocate more entries
-        assert( p->pEntriesFree == NULL );
-        if ( p->nChunks == p->nChunksAlloc )
-        {
-            p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
-        }
-        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
-        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
-        // transform these entries into a linked list
-        pTemp = p->pEntriesFree;
-        for ( i = 1; i < p->nChunkSize; i++ )
-        {
-            *((char **)pTemp) = pTemp + p->nEntrySize;
-            pTemp += p->nEntrySize;
-        }
-        // set the last link
-        *((char **)pTemp) = NULL;
-        // add the chunk to the chunk storage
-        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
-        // add to the number of entries allocated
-        p->nEntriesAlloc += p->nChunkSize;
-    }
-    // incrememt the counter of used entries
-    p->nEntriesUsed++;
-    if ( p->nEntriesMax < p->nEntriesUsed )
-        p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the free entry list
-    pTemp = p->pEntriesFree;
-    p->pEntriesFree = *((char **)pTemp);
-    return pTemp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry )
-{
-    // decrement the counter of used entries
-    p->nEntriesUsed--;
-    // add the entry to the linked list of free entries
-    *((char **)pEntry) = p->pEntriesFree;
-    p->pEntriesFree = pEntry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description [Relocates all the memory except the first chunk.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmFixedRestart( Msat_MmFixed_t * p )
-{
-    int i;
-    char * pTemp;
-
-    // deallocate all chunks except the first one
-    for ( i = 1; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    p->nChunks = 1;
-    // transform these entries into a linked list
-    pTemp = p->pChunks[0];
-    for ( i = 1; i < p->nChunkSize; i++ )
-    {
-        *((char **)pTemp) = pTemp + p->nEntrySize;
-        pTemp += p->nEntrySize;
-    }
-    // set the last link
-    *((char **)pTemp) = NULL;
-    // set the free entry list
-    p->pEntriesFree  = p->pChunks[0];
-    // set the correct statistics
-    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
-    p->nMemoryUsed   = 0;
-    p->nEntriesAlloc = p->nChunkSize;
-    p->nEntriesUsed  = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p )
-{
-    return p->nMemoryAlloc;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates entries of flexible size.]
-
-  Description [Can only work with entry size at least 4 byte long.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_MmFlex_t * Msat_MmFlexStart()
-{
-    Msat_MmFlex_t * p;
-
-    p = ALLOC( Msat_MmFlex_t, 1 );
-    memset( p, 0, sizeof(Msat_MmFlex_t) );
-
-    p->nEntriesUsed  = 0;
-    p->pCurrent      = NULL;
-    p->pEnd          = NULL;
-
-    p->nChunkSize    = (1 << 12);
-    p->nChunksAlloc  = 64;
-    p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
-
-    p->nMemoryUsed   = 0;
-    p->nMemoryAlloc  = 0;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose )
-{
-    int i;
-    if ( p == NULL )
-        return;
-    if ( fVerbose )
-    {
-        printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
-            p->nChunkSize, p->nChunks );
-        printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
-            p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
-    }
-    for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes )
-{
-    char * pTemp;
-    // check if there are still free entries
-    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
-    { // need to allocate more entries
-        if ( p->nChunks == p->nChunksAlloc )
-        {
-            p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
-        }
-        if ( nBytes > p->nChunkSize )
-        {
-            // resize the chunk size if more memory is requested than it can give
-            // (ideally, this should never happen)
-            p->nChunkSize = 2 * nBytes;
-        }
-        p->pCurrent = ALLOC( char, p->nChunkSize );
-        p->pEnd     = p->pCurrent + p->nChunkSize;
-        p->nMemoryAlloc += p->nChunkSize;
-        // add the chunk to the chunk storage
-        p->pChunks[ p->nChunks++ ] = p->pCurrent;
-    }
-    assert( p->pCurrent + nBytes <= p->pEnd );
-    // increment the counter of used entries
-    p->nEntriesUsed++;
-    // keep track of the memory used
-    p->nMemoryUsed += nBytes;
-    // return the next entry
-    pTemp = p->pCurrent;
-    p->pCurrent += nBytes;
-    return pTemp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p )
-{
-    return p->nMemoryAlloc;
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the hierarchical memory manager.]
-
-  Description [This manager can allocate entries of any size.
-  Iternally they are mapped into the entries with the number of bytes
-  equal to the power of 2. The smallest entry size is 8 bytes. The
-  next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 
-  8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
-  The input parameters "nSteps" says how many fixed memory managers
-  are employed internally. Calling this procedure with nSteps equal
-  to 10 results in 10 hierarchically arranged internal memory managers, 
-  which can allocate up to 4096 (1Kb) entries. Requests for larger 
-  entries are handed over to malloc() and then free()ed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_MmStep_t * Msat_MmStepStart( int nSteps )
-{
-    Msat_MmStep_t * p;
-    int i, k;
-    p = ALLOC( Msat_MmStep_t, 1 );
-    p->nMems = nSteps;
-    // start the fixed memory managers
-    p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems );
-    for ( i = 0; i < p->nMems; i++ )
-        p->pMems[i] = Msat_MmFixedStart( (8<<i) );
-    // set up the mapping of the required memory size into the corresponding manager
-    p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
-    p->pMap[0] = NULL;
-    for ( k = 1; k <= 4; k++ )
-        p->pMap[k] = p->pMems[0];
-    for ( i = 0; i < p->nMems; i++ )
-        for ( k = (4<<i)+1; k <= (8<<i); k++ )
-            p->pMap[k] = p->pMems[i];
-//for ( i = 1; i < 100; i ++ )
-//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose )
-{
-    int i;
-    for ( i = 0; i < p->nMems; i++ )
-        Msat_MmFixedStop( p->pMems[i], fVerbose );
-    free( p->pMems );
-    free( p->pMap );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the entry.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes )
-{
-    if ( nBytes == 0 )
-        return NULL;
-    if ( nBytes > p->nMapSize )
-    {
-//        printf( "Allocating %d bytes.\n", nBytes );
-        return ALLOC( char, nBytes );
-    }
-    return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recycles the entry.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes )
-{
-    if ( nBytes == 0 )
-        return;
-    if ( nBytes > p->nMapSize )
-    {
-        free( pEntry );
-        return;
-    }
-    Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_MmStepReadMemUsage( Msat_MmStep_t * p )
-{
-    int i, nMemTotal = 0;
-    for ( i = 0; i < p->nMems; i++ )
-        nMemTotal += p->pMems[i]->nMemoryAlloc;
-    return nMemTotal;
-}
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
deleted file mode 100644
index 956e7fc6..00000000
--- a/src/sat/msat/msatOrderH.c
+++ /dev/null
@@ -1,405 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatOrder.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The manager of variable assignment.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// the variable package data structure
-struct Msat_Order_t_
-{
-    Msat_Solver_t *      pSat;         // the SAT solver 
-    Msat_IntVec_t *      vIndex;       // the heap
-    Msat_IntVec_t *      vHeap;        // the mapping of var num into its heap num
-};
-
-//The solver can communicate to the variable order the following parts:
-//- the array of current assignments (pSat->pAssigns)
-//- the array of variable activities (pSat->pdActivity)
-//- the array of variables currently in the cone (pSat->vConeVars)
-//- the array of arrays of variables adjucent to each(pSat->vAdjacents)
-
-#define HLEFT(i)               ((i)<<1)
-#define HRIGHT(i)             (((i)<<1)+1)
-#define HPARENT(i)             ((i)>>1)
-#define HCOMPARE(p, i, j)      ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])
-#define HHEAP(p, i)            ((p)->vHeap->pArray[i])
-#define HSIZE(p)               ((p)->vHeap->nSize)
-#define HOKAY(p, i)            ((i) >= 0 && (i) < (p)->vIndex->nSize)
-#define HINHEAP(p, i)          (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)
-#define HEMPTY(p)              (HSIZE(p) == 1)
-
-static int Msat_HeapCheck_rec( Msat_Order_t * p, int i );
-static int Msat_HeapGetTop( Msat_Order_t * p );
-static void Msat_HeapInsert( Msat_Order_t * p, int n );
-static void Msat_HeapIncrease( Msat_Order_t * p, int n );
-static void Msat_HeapPercolateUp( Msat_Order_t * p, int i );
-static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
-
-extern int timeSelect;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
-{
-    Msat_Order_t * p;
-    p = ALLOC( Msat_Order_t, 1 );
-    memset( p, 0, sizeof(Msat_Order_t) );
-    p->pSat   = pSat;
-    p->vIndex = Msat_IntVecAlloc( 0 );
-    p->vHeap  = Msat_IntVecAlloc( 0 );
-    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the bound of the ordering structure.]
-
-  Description [Should be called whenever the SAT solver is resized.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax )
-{
-    Msat_IntVecGrow( p->vIndex, nVarsMax );
-    Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
-    p->vIndex->nSize = nVarsMax;
-    p->vHeap->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone )
-{
-    int i;
-    for ( i = 0; i < p->vIndex->nSize; i++ )
-        p->vIndex->pArray[i] = 0;
-    for ( i = 0; i < vCone->nSize; i++ )
-    {
-        assert( i+1 < p->vHeap->nCap );
-        p->vHeap->pArray[i+1] = vCone->pArray[i];
-
-        assert( vCone->pArray[i] < p->vIndex->nSize );
-        p->vIndex->pArray[vCone->pArray[i]] = i+1;
-    }
-    p->vHeap->nSize = vCone->nSize + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks that the J-boundary is okay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_OrderCheck( Msat_Order_t * p )
-{
-    return Msat_HeapCheck_rec( p, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderFree( Msat_Order_t * p )
-{
-    Msat_IntVecFree( p->vHeap );
-    Msat_IntVecFree( p->vIndex );
-    free( p );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Selects the next variable to assign.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_OrderVarSelect( Msat_Order_t * p )
-{
-    // Activity based decision:
-//    while (!heap.empty()){
-//        Var next = heap.getmin();
-//        if (toLbool(assigns[next]) == l_Undef)
-//            return next;
-//    }
-//    return var_Undef;
-
-    int Var;
-    int clk = clock();
-
-    while ( !HEMPTY(p) )
-    {
-        Var = Msat_HeapGetTop(p);
-        if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
-        {
-//assert( Msat_OrderCheck(p) );
-timeSelect += clock() - clk;
-            return Var;
-        }
-    }
-    return MSAT_ORDER_UNKNOWN;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates J-boundary when the variable is assigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
-{
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable is unassigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
-{
-//    if (!heap.inHeap(x))
-//        heap.insert(x);
-
-    int clk = clock();
-    if ( !HINHEAP(p,Var) )
-        Msat_HeapInsert( p, Var );
-timeSelect += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable changed weight.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderUpdate( Msat_Order_t * p, int Var )
-{
-//    if (heap.inHeap(x))
-//        heap.increase(x);
-
-    int clk = clock();
-    if ( HINHEAP(p,Var) )
-        Msat_HeapIncrease( p, Var );
-timeSelect += clock() - clk;
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the heap property recursively.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_HeapCheck_rec( Msat_Order_t * p, int i )
-{
-    return i >= HSIZE(p) ||
-        ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
-        Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Retrieves the minimum element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_HeapGetTop( Msat_Order_t * p )
-{
-    int Result, NewTop;
-    Result                    = HHEAP(p, 1);
-    NewTop                    = Msat_IntVecPop( p->vHeap );
-    p->vHeap->pArray[1]       = NewTop;
-    p->vIndex->pArray[NewTop] = 1;
-    p->vIndex->pArray[Result] = 0;
-    if ( p->vHeap->nSize > 1 )
-        Msat_HeapPercolateDown( p, 1 );
-    return Result;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the new element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_HeapInsert( Msat_Order_t * p, int n )
-{
-    assert( HOKAY(p, n) );
-    p->vIndex->pArray[n] = HSIZE(p);
-    Msat_IntVecPush( p->vHeap, n );
-    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the new element.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_HeapIncrease( Msat_Order_t * p, int n )
-{
-    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the entry up.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_HeapPercolateUp( Msat_Order_t * p, int i )
-{
-    int x = HHEAP(p, i);
-    while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) )
-    {
-        p->vHeap->pArray[i]            = HHEAP(p, HPARENT(i));
-        p->vIndex->pArray[HHEAP(p, i)] = i;
-        i                              = HPARENT(i);
-    }
-    p->vHeap->pArray[i]  = x;
-    p->vIndex->pArray[x] = i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the entry down.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_HeapPercolateDown( Msat_Order_t * p, int i )
-{
-    int x = HHEAP(p, i);
-    int Child;
-    while ( HLEFT(i) < HSIZE(p) )
-    {
-        if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) )
-            Child = HRIGHT(i);
-        else
-            Child = HLEFT(i);
-        if ( !HCOMPARE(p, HHEAP(p, Child), x) )
-            break;
-        p->vHeap->pArray[i]            = HHEAP(p, Child);
-        p->vIndex->pArray[HHEAP(p, i)] = i;
-        i                              = Child;
-    }
-    p->vHeap->pArray[i]  = x;
-    p->vIndex->pArray[x] = i;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
deleted file mode 100644
index 4db7ff7b..00000000
--- a/src/sat/msat/msatOrderJ.c
+++ /dev/null
@@ -1,472 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatOrder.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The manager of variable assignment.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-/* 
-The J-boundary (justification boundary) is defined as a set of unassigned 
-variables belonging to the cone of interest, such that for each of them,
-there exist an adjacent assigned variable in the cone of interest.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Msat_OrderVar_t_  Msat_OrderVar_t;
-typedef struct Msat_OrderRing_t_ Msat_OrderRing_t;
-
-// the variable data structure
-struct Msat_OrderVar_t_
-{
-    Msat_OrderVar_t    * pNext;
-    Msat_OrderVar_t    * pPrev;
-    int                  Num;
-};
-
-// the ring of variables data structure (J-boundary)
-struct Msat_OrderRing_t_
-{
-    Msat_OrderVar_t    * pRoot; 
-    int                 nItems;
-};
-
-// the variable package data structure
-struct Msat_Order_t_
-{
-    Msat_Solver_t *      pSat;         // the SAT solver 
-    Msat_OrderVar_t *    pVars;        // the storage for variables
-    int                 nVarsAlloc;   // the number of variables allocated
-    Msat_OrderRing_t     rVars;        // the J-boundary as a ring of variables
-};
-
-//The solver can communicate to the variable order the following parts:
-//- the array of current assignments (pSat->pAssigns)
-//- the array of variable activities (pSat->pdActivity)
-//- the array of variables currently in the cone (pSat->vConeVars)
-//- the array of arrays of variables adjucent to each(pSat->vAdjacents)
-
-#define Msat_OrderVarIsInBoundary( p, i )   ((p)->pVars[i].pNext)
-#define Msat_OrderVarIsAssigned( p, i )     ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED)
-#define Msat_OrderVarIsUsedInCone( p, i )   ((p)->pSat->vVarsUsed->pArray[i])
-
-// iterator through the entries in J-boundary
-#define Msat_OrderRingForEachEntry( pRing, pVar, pNext )         \
-    for ( pVar = pRing,                                         \
-          pNext = pVar? pVar->pNext : NULL;                     \
-          pVar;                                                 \
-          pVar = (pNext != pRing)? pNext : NULL,                \
-          pNext = pVar? pVar->pNext : NULL )
-
-static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar );
-static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar );
-
-extern int timeSelect;
-extern int timeAssign;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
-{
-    Msat_Order_t * p;
-    p = ALLOC( Msat_Order_t, 1 );
-    memset( p, 0, sizeof(Msat_Order_t) );
-    p->pSat = pSat;
-    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the bound of the ordering structure.]
-
-  Description [Should be called whenever the SAT solver is resized.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax )
-{
-    int i;
-    // add variables if they are missing
-    if ( p->nVarsAlloc < nVarsMax )
-    {
-        p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax );
-        for ( i = p->nVarsAlloc; i < nVarsMax; i++ )
-        {
-            p->pVars[i].pNext = p->pVars[i].pPrev = NULL;
-            p->pVars[i].Num = i;
-        }
-        p->nVarsAlloc = nVarsMax;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone )
-{
-    Msat_OrderVar_t * pVar, * pNext;
-    // quickly undo the ring
-    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
-        pVar->pNext = pVar->pPrev = NULL;
-    p->rVars.pRoot  = NULL;
-    p->rVars.nItems = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks that the J-boundary is okay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_OrderCheck( Msat_Order_t * p )
-{
-    Msat_OrderVar_t * pVar, * pNext;
-    Msat_IntVec_t * vRound;
-    int * pRound, nRound;
-    int * pVars, nVars, i, k;
-    int Counter = 0;
-
-    // go through all the variables in the boundary
-    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
-    {
-        assert( !Msat_OrderVarIsAssigned(p, pVar->Num) );
-        // go though all the variables in the neighborhood
-        // and check that it is true that there is least one assigned
-        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num );
-        nRound = Msat_IntVecReadSize( vRound );
-        pRound = Msat_IntVecReadArray( vRound );
-        for ( i = 0; i < nRound; i++ )
-        {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
-                continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
-                break;
-        }
-//        assert( i != nRound );
-//        if ( i == nRound )
-//            return 0;
-        if ( i == nRound )
-            Counter++;
-    }
-    if ( Counter > 0 )
-        printf( "%d(%d) ", Counter, p->rVars.nItems );
-
-    // we may also check other unassigned variables in the cone
-    // to make sure that if they are not in J-boundary, 
-    // then they do not have an assigned neighbor
-    nVars = Msat_IntVecReadSize( p->pSat->vConeVars );
-    pVars = Msat_IntVecReadArray( p->pSat->vConeVars );
-    for ( i = 0; i < nVars; i++ )
-    {
-        assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) );
-        // skip assigned vars, vars in the boundary, and vars not used in the cone
-        if ( Msat_OrderVarIsAssigned(p, pVars[i]) || 
-             Msat_OrderVarIsInBoundary(p, pVars[i]) )
-            continue;
-        // make sure, it does not have assigned neighbors
-        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
-        nRound = Msat_IntVecReadSize( vRound );
-        pRound = Msat_IntVecReadArray( vRound );
-        for ( k = 0; k < nRound; k++ )
-        {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
-                continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
-                break;
-        }
-//        assert( k == nRound );
-//        if ( k != nRound )
-//            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the ordering structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderFree( Msat_Order_t * p )
-{
-    free( p->pVars );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Selects the next variable to assign.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_OrderVarSelect( Msat_Order_t * p )
-{
-    Msat_OrderVar_t * pVar, * pNext, * pVarBest;
-    double * pdActs = p->pSat->pdActivity;
-    double dfActBest;
-//    int clk = clock();
-
-    pVarBest = NULL;
-    dfActBest = -1.0;
-    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
-    {
-        if ( dfActBest < pdActs[pVar->Num] )
-        {
-            dfActBest = pdActs[pVar->Num];
-            pVarBest  = pVar;
-        }
-    }
-//timeSelect += clock() - clk;
-//timeAssign += clock() - clk;
-
-//if ( pVarBest && pVarBest->Num % 1000 == 0 )
-//printf( "%d ", p->rVars.nItems );
-
-//    Msat_OrderCheck( p );
-    if ( pVarBest )
-    {
-        assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
-        return pVarBest->Num;
-    }
-    return MSAT_ORDER_UNKNOWN;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates J-boundary when the variable is assigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
-{
-    Msat_IntVec_t * vRound;
-    int i;//, clk = clock();
-
-    // make sure the variable is in the boundary
-    assert( Var < p->nVarsAlloc );
-    // if it is not in the boundary (initial decision, random decision), do not remove
-    if ( Msat_OrderVarIsInBoundary( p, Var ) )
-        Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] );
-    // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary
-    // because for them we know that there is a variable (Var) which is assigned
-    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
-    for ( i = 0; i < vRound->nSize; i++ )
-    {
-        if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) )
-            continue;
-        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) )
-            continue;
-        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
-            continue;
-        Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
-    }
-//timeSelect += clock() - clk;
-//    Msat_OrderCheck( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable is unassigned.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
-{
-    Msat_IntVec_t * vRound, * vRound2;
-    int i, k;//, clk = clock();
-
-    // make sure the variable is not in the boundary
-    assert( Var < p->nVarsAlloc );
-    assert( !Msat_OrderVarIsInBoundary( p, Var ) );
-    // go through its neigbors - if one of them is assigned add this var
-    // add to the boundary those neighbors that are not there already
-    // this will also get rid of variable outside of the current cone
-    // because they are unassigned in Msat_SolverPrepare()
-    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
-    for ( i = 0; i < vRound->nSize; i++ )
-        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) 
-            break;
-    if ( i != vRound->nSize )
-        Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] );
-
-    // unassigning a variable may lead to its adjacents dropping from the boundary
-    for ( i = 0; i < vRound->nSize; i++ )
-        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
-        { // the neighbor is in the J-boundary (and unassigned)
-            assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) );
-            vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]];
-            // go through its neighbors and determine if there is at least one assigned
-            for ( k = 0; k < vRound2->nSize; k++ )
-                if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) 
-                    break;
-            if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
-                Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
-        }
-//timeSelect += clock() - clk;
-//    Msat_OrderCheck( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the order after a variable changed weight.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderUpdate( Msat_Order_t * p, int Var )
-{
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Adds node to the end of the ring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
-{
-//printf( "adding %d\n", pVar->Num );
-    // check that the node is not in a ring
-    assert( pVar->pPrev == NULL );
-    assert( pVar->pNext == NULL );
-    // if the ring is empty, make the node point to itself
-    pRing->nItems++;
-    if ( pRing->pRoot == NULL )
-    {
-        pRing->pRoot  = pVar;
-        pVar->pPrev  = pVar;
-        pVar->pNext  = pVar;
-        return;
-    }
-    // if the ring is not empty, add it as the last entry
-    pVar->pPrev = pRing->pRoot->pPrev;
-    pVar->pNext = pRing->pRoot;
-    pVar->pPrev->pNext = pVar;
-    pVar->pNext->pPrev = pVar;
-
-    // move the root so that it points to the new entry
-//    pRing->pRoot = pRing->pRoot->pPrev;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes the node from the ring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
-{
-//printf( "removing %d\n", pVar->Num );
-    // check that the var is in a ring
-    assert( pVar->pPrev );
-    assert( pVar->pNext );
-    pRing->nItems--;
-    if ( pRing->nItems == 0 )
-    {
-        assert( pRing->pRoot == pVar );
-        pVar->pPrev = NULL;
-        pVar->pNext = NULL;
-        pRing->pRoot = NULL;
-        return;
-    }
-    // move the root if needed
-    if ( pRing->pRoot == pVar )
-        pRing->pRoot = pVar->pNext;
-    // move the root to the next entry after pVar
-    // this way all the additions to the list will be traversed first
-//    pRing->pRoot = pVar->pPrev;
-    // delete the node
-    pVar->pPrev->pNext = pVar->pNext;
-    pVar->pNext->pPrev = pVar->pPrev;
-    pVar->pPrev = NULL;
-    pVar->pNext = NULL;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
deleted file mode 100644
index 5938e042..00000000
--- a/src/sat/msat/msatQueue.c
+++ /dev/null
@@ -1,157 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatQueue.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The manager of the assignment propagation queue.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatQueue.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Msat_Queue_t_ 
-{
-    int         nVars;
-    int *       pVars;
-    int         iFirst;
-    int         iLast;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the variable propagation queue.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Queue_t * Msat_QueueAlloc( int nVars )
-{
-    Msat_Queue_t * p;
-    p = ALLOC( Msat_Queue_t, 1 );
-    memset( p, 0, sizeof(Msat_Queue_t) );
-    p->nVars  = nVars;
-    p->pVars  = ALLOC( int, nVars );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocate the variable propagation queue.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_QueueFree( Msat_Queue_t * p )
-{
-    free( p->pVars );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the queue size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_QueueReadSize( Msat_Queue_t * p )
-{
-    return p->iLast - p->iFirst;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Insert an entry into the queue.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_QueueInsert( Msat_Queue_t * p, int Lit )
-{
-    if ( p->iLast == p->nVars )
-    {
-        int i;
-        assert( 0 );
-        for ( i = 0; i < p->iLast; i++ )
-            printf( "entry = %2d  lit = %2d  var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
-    }
-    assert( p->iLast < p->nVars );
-    p->pVars[p->iLast++] = Lit;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Extracts an entry from the queue.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_QueueExtract( Msat_Queue_t * p )
-{
-    if ( p->iFirst == p->iLast )
-        return -1;
-    return p->pVars[p->iFirst++];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resets the queue.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_QueueClear( Msat_Queue_t * p )
-{
-    p->iFirst = 0;
-    p->iLast  = 0;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
deleted file mode 100644
index 738562ef..00000000
--- a/src/sat/msat/msatRead.c
+++ /dev/null
@@ -1,268 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatRead.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The reader of the CNF formula in DIMACS format.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatRead.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static char * Msat_FileRead( FILE * pFile );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Read the file into the internal buffer.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Msat_FileRead( FILE * pFile )
-{
-    int nFileSize;
-    char * pBuffer;
-    // get the file size, in bytes
-    fseek( pFile, 0, SEEK_END );  
-    nFileSize = ftell( pFile );  
-    // move the file current reading position to the beginning
-    rewind( pFile ); 
-    // load the contents of the file into memory
-    pBuffer = ALLOC( char, nFileSize + 3 );
-    fread( pBuffer, nFileSize, 1, pFile );
-    // terminate the string with '\0'
-    pBuffer[ nFileSize + 0] = '\n';
-    pBuffer[ nFileSize + 1] = '\0';
-    return pBuffer;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Msat_ReadWhitespace( char ** pIn ) 
-{
-    while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32)
-        (*pIn)++; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Msat_ReadNotWhitespace( char ** pIn ) 
-{
-    while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) )
-        (*pIn)++; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void skipLine( char ** pIn ) 
-{
-    while ( 1 )
-    {
-        if (**pIn == 0) 
-            return;
-        if (**pIn == '\n') 
-        { 
-            (*pIn)++; 
-            return; 
-        }
-        (*pIn)++; 
-    } 
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Msat_ReadInt( char ** pIn ) 
-{
-    int     val = 0;
-    bool    neg = 0;
-
-    Msat_ReadWhitespace( pIn );
-    if ( **pIn == '-' ) 
-        neg = 1, 
-        (*pIn)++;
-    else if ( **pIn == '+' ) 
-        (*pIn)++;
-    if ( **pIn < '0' || **pIn > '9' ) 
-        fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn), 
-        exit(1);
-    while ( **pIn >= '0' && **pIn <= '9' )
-        val = val*10 + (**pIn - '0'),
-        (*pIn)++;
-    return neg ? -val : val; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLits ) 
-{
-    int nVars = Msat_SolverReadVarNum( p );
-    int parsed_lit, var, sign;
-
-    Msat_IntVecClear( pLits );
-    while ( 1 )
-    {
-        parsed_lit = Msat_ReadInt(pIn);
-        if ( parsed_lit == 0 ) 
-            break;
-        var = abs(parsed_lit) - 1;
-        sign = (parsed_lit > 0);
-        if ( var >= nVars )
-        {
-            printf( "Variable %d is larger than the number of allocated variables (%d).\n", var+1, nVars );
-            exit(1);
-        }
-        Msat_IntVecPush( pLits, MSAT_VAR2LIT(var, !sign) );
-    }
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) 
-{
-    Msat_Solver_t * p;
-    Msat_IntVec_t * pLits;
-    char * pIn = pText;
-    int nVars, nClas;
-    while ( 1 )
-    {
-        Msat_ReadWhitespace( &pIn );
-        if ( *pIn == 0 )
-            break;
-        else if ( *pIn == 'c' )
-            skipLine( &pIn );
-        else if ( *pIn == 'p' )
-        {
-            pIn++;
-            Msat_ReadWhitespace( &pIn );
-            Msat_ReadNotWhitespace( &pIn );
-
-            nVars = Msat_ReadInt( &pIn );
-            nClas = Msat_ReadInt( &pIn );
-            skipLine( &pIn );
-            // start the solver
-            p = Msat_SolverAlloc( nVars, 1, 1, 1, 1, 0 ); 
-            Msat_SolverClean( p, nVars );
-            Msat_SolverSetVerbosity( p, fVerbose );
-            // allocate the vector
-            pLits = Msat_IntVecAlloc( nVars );
-        }
-        else
-        {
-            if ( p == NULL )
-            {
-                printf( "There is no parameter line.\n" );
-                exit(1);
-            }
-            Msat_ReadClause( &pIn, p, pLits );
-            if ( !Msat_SolverAddClause( p, pLits ) )
-                return 0;
-        }
-    }
-    Msat_IntVecFree( pLits );
-    *pS = p;
-    return Msat_SolverSimplifyDB( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the solver and reads the DIMAC file.]
-
-  Description [Returns FALSE upon immediate conflict.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
-{
-    char * pText;
-    bool Value;
-    pText = Msat_FileRead( pFile );
-    Value = Msat_ReadDimacs( pText, p, fVerbose );
-    free( pText );
-    return Value;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
deleted file mode 100644
index ee3507a6..00000000
--- a/src/sat/msat/msatSolverApi.c
+++ /dev/null
@@ -1,500 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatSolverApi.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [APIs of the SAT solver.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Simple SAT solver APIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;      }
-int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;   }
-int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc; }
-int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
-int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;     }
-Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )            { return p->pReasons;   }
-Msat_Lit_t          Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
-Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                { return p->vLearned;   }
-Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )           { return p->pvWatched;  }
-int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;   }
-int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;     }
-int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return (int)p->Stats.nConflicts; }
-int                Msat_SolverReadInspects( Msat_Solver_t * p )                { return (int)p->Stats.nInspects;  }
-Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                    { return p->pMem;       }
-int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;      }
-int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId;  }
-void               Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose )  { p->fVerbose = fVerbose; }
-void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;   }
-void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;   }
-void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++;  }
-void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--;  }
-void               Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p )         { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
-void               Msat_SolverMarkClausesStart( Msat_Solver_t * p )            { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
-float *            Msat_SolverReadFactors( Msat_Solver_t * p )                 { return p->pFactors;   }
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the clause with the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num )
-{
-    int nClausesP;
-    assert( Num < p->nClauses );
-    nClausesP = Msat_ClauseVecReadSize( p->vClauses );
-    if ( Num < nClausesP )
-        return Msat_ClauseVecReadEntry( p->vClauses, Num );
-    return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the clause with the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p )
-{
-    return p->vAdjacents;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the clause with the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p )
-{
-    return p->vConeVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the clause with the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p )
-{
-    return p->vVarsUsed;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the solver.]
-
-  Description [After the solver is allocated, the procedure
-  Msat_SolverClean() should be called to set the number of variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
-    double dClaInc, double dClaDecay, 
-    double dVarInc, double dVarDecay, 
-    bool fVerbose )
-{
-    Msat_Solver_t * p;
-    int i;
-
-    assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
-    assert(sizeof(float)     == sizeof(unsigned));
-
-    p = ALLOC( Msat_Solver_t, 1 );
-    memset( p, 0, sizeof(Msat_Solver_t) );
-
-    p->nVarsAlloc = nVarsAlloc;
-    p->nVars     = 0;
-
-    p->nClauses  = 0;
-    p->vClauses  = Msat_ClauseVecAlloc( 512 );
-    p->vLearned  = Msat_ClauseVecAlloc( 512 );
-
-    p->dClaInc   = dClaInc;
-    p->dClaDecay = dClaDecay;
-    p->dVarInc   = dVarInc;
-    p->dVarDecay = dVarDecay;
-
-    p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pFactors   = ALLOC( float, p->nVarsAlloc );
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-    {
-        p->pdActivity[i] = 0.0;
-        p->pFactors[i]   = 1.0;
-    }
-
-    p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
-    p->pModel    = ALLOC( int, p->nVarsAlloc ); 
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
-//    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
-    p->pOrder    = Msat_OrderAlloc( p );
-
-    p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
-    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
-        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
-    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
-
-    p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
-    p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
-    p->pReasons  = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
-    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
-    p->pLevel = ALLOC( int, p->nVarsAlloc );
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-        p->pLevel[i] = -1;
-    p->dRandSeed = 91648253;
-    p->fVerbose  = fVerbose;
-    p->dProgress = 0.0;
-//    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
-    p->pMem = Msat_MmStepStart( 10 );
-
-    p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
-    p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
-    p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
-    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
-
-
-    p->pSeen     = ALLOC( int, p->nVarsAlloc );
-    memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
-    p->nSeenId   = 1;
-    p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
-    p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the solver.]
-
-  Description [Assumes that the solver contains some clauses, and that 
-  it is currently between the calls. Resizes the solver to accomodate 
-  more variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
-{
-    int nVarsAllocOld, i;
-
-    nVarsAllocOld = p->nVarsAlloc;
-    p->nVarsAlloc = nVarsAlloc;
-
-    p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
-    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-    {
-        p->pdActivity[i] = 0.0;
-        p->pFactors[i]   = 1.0;
-    }
-
-    p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
-    p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
-    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
-
-//    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
-    Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
-
-    p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
-    for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
-        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
-
-    Msat_QueueFree( p->pQueue );
-    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
-
-    p->pReasons  = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
-    p->pLevel    = REALLOC( int, p->pLevel, p->nVarsAlloc );
-    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-    {
-        p->pReasons[i] = NULL;
-        p->pLevel[i] = -1;
-    }
-
-    p->pSeen     = REALLOC( int, p->pSeen, p->nVarsAlloc );
-    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-        p->pSeen[i] = 0;
-
-    Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
-    Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
-
-    // make sure the array of adjucents has room to store the variable numbers
-    for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
-        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
-    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the solver.]
-
-  Description [Cleans the solver assuming that the problem will involve 
-  the given number of variables (nVars). This procedure is useful 
-  for many small (incremental) SAT problems, to prevent the solver
-  from being reallocated each time.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverClean( Msat_Solver_t * p, int nVars )
-{
-    int i;
-    // free the clauses
-    int nClauses;
-    Msat_Clause_t ** pClauses;
-
-    assert( p->nVarsAlloc >= nVars );
-    p->nVars    = nVars;
-    p->nClauses = 0;
-
-    nClauses = Msat_ClauseVecReadSize( p->vClauses );
-    pClauses = Msat_ClauseVecReadArray( p->vClauses );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseFree( p, pClauses[i], 0 );
-//    Msat_ClauseVecFree( p->vClauses );
-    Msat_ClauseVecClear( p->vClauses );
-
-    nClauses = Msat_ClauseVecReadSize( p->vLearned );
-    pClauses = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseFree( p, pClauses[i], 0 );
-//    Msat_ClauseVecFree( p->vLearned );
-    Msat_ClauseVecClear( p->vLearned );
-
-//    FREE( p->pdActivity );
-    for ( i = 0; i < p->nVars; i++ )
-        p->pdActivity[i] = 0;
-
-//    Msat_OrderFree( p->pOrder );
-//    Msat_OrderClean( p->pOrder, p->nVars, NULL );
-    Msat_OrderSetBounds( p->pOrder, p->nVars );
-
-    for ( i = 0; i < 2 * p->nVars; i++ )
-//        Msat_ClauseVecFree( p->pvWatched[i] );
-        Msat_ClauseVecClear( p->pvWatched[i] );
-//    FREE( p->pvWatched );
-//    Msat_QueueFree( p->pQueue );
-    Msat_QueueClear( p->pQueue );
-
-//    FREE( p->pAssigns );
-    for ( i = 0; i < p->nVars; i++ )
-        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
-//    Msat_IntVecFree( p->vTrail );
-    Msat_IntVecClear( p->vTrail );
-//    Msat_IntVecFree( p->vTrailLim );
-    Msat_IntVecClear( p->vTrailLim );
-//    FREE( p->pReasons );
-    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
-//    FREE( p->pLevel );
-    for ( i = 0; i < p->nVars; i++ )
-        p->pLevel[i] = -1;
-//    Msat_IntVecFree( p->pModel );
-//    Msat_MmStepStop( p->pMem, 0 );
-    p->dRandSeed = 91648253;
-    p->dProgress = 0.0;
-
-//    FREE( p->pSeen );
-    memset( p->pSeen, 0, sizeof(int) * p->nVars );
-    p->nSeenId = 1;
-//    Msat_IntVecFree( p->vReason );
-    Msat_IntVecClear( p->vReason );
-//    Msat_IntVecFree( p->vTemp );
-    Msat_IntVecClear( p->vTemp );
-//    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
-//    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverFree( Msat_Solver_t * p )
-{
-    int i;
-
-    // free the clauses
-    int nClauses;
-    Msat_Clause_t ** pClauses;
-//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
-//                                         Msat_ClauseVecReadSize( p->vLearned ) );
-
-    nClauses = Msat_ClauseVecReadSize( p->vClauses );
-    pClauses = Msat_ClauseVecReadArray( p->vClauses );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseFree( p, pClauses[i], 0 );
-    Msat_ClauseVecFree( p->vClauses );
-
-    nClauses = Msat_ClauseVecReadSize( p->vLearned );
-    pClauses = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseFree( p, pClauses[i], 0 );
-    Msat_ClauseVecFree( p->vLearned );
-
-    FREE( p->pdActivity );
-    FREE( p->pFactors );
-    Msat_OrderFree( p->pOrder );
-
-    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
-        Msat_ClauseVecFree( p->pvWatched[i] );
-    FREE( p->pvWatched );
-    Msat_QueueFree( p->pQueue );
-
-    FREE( p->pAssigns );
-    FREE( p->pModel );
-    Msat_IntVecFree( p->vTrail );
-    Msat_IntVecFree( p->vTrailLim );
-    FREE( p->pReasons );
-    FREE( p->pLevel );
-
-    Msat_MmStepStop( p->pMem, 0 );
-
-    nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
-    pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
-    Msat_ClauseVecFree( p->vAdjacents );
-    Msat_IntVecFree( p->vConeVars );
-    Msat_IntVecFree( p->vVarsUsed );
-
-    FREE( p->pSeen );
-    Msat_IntVecFree( p->vReason );
-    Msat_IntVecFree( p->vTemp );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the solver to run on a subset of variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars )
-{
-
-    int i;
-    // undo the previous data
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-    {
-        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
-        p->pReasons[i]   = NULL;
-        p->pLevel[i]     = -1;
-        p->pdActivity[i] = 0.0;
-    }
-
-    // set the new variable order
-    Msat_OrderClean( p->pOrder, vVars );
-
-    Msat_QueueClear( p->pQueue );
-    Msat_IntVecClear( p->vTrail );
-    Msat_IntVecClear( p->vTrailLim );
-    p->dProgress = 0.0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets up the truth tables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
-{
-    int m, v;
-    // set up the truth tables
-    for ( m = 0; m < 32; m++ )
-        for ( v = 0; v < 5; v++ )
-            if ( m & (1 << v) )
-                uTruths[v][0] |= (1 << m);
-    // make adjustments for the case of 6 variables
-    for ( v = 0; v < 5; v++ )
-        uTruths[v][1] = uTruths[v][0];
-    uTruths[5][0] = 0;
-    uTruths[5][1] = ~((unsigned)0);
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
deleted file mode 100644
index f9fee73c..00000000
--- a/src/sat/msat/msatSolverCore.c
+++ /dev/null
@@ -1,212 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatSolverCore.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The SAT solver core procedures.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one variable to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
-{
-    if ( p->nVars == p->nVarsAlloc )
-        Msat_SolverResize( p, 2 * p->nVarsAlloc );
-    p->pLevel[p->nVars] = Level;
-    p->nVars++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one clause to the solver's clause database.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
-{
-    Msat_Clause_t * pC; 
-    bool Value;
-    Value = Msat_ClauseCreate( p, vLits, 0, &pC );
-    if ( pC != NULL )
-        Msat_ClauseVecPush( p->vClauses, pC );
-//    else if ( p->fProof )
-//        Msat_ClauseCreateFake( p, vLits );
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns search-space coverage. Not extremely reliable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-double Msat_SolverProgressEstimate( Msat_Solver_t * p )
-{
-    double dProgress = 0.0;
-    double dF = 1.0 / p->nVars;
-    int i;
-    for ( i = 0; i < p->nVars; i++ )
-        if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
-            dProgress += pow( dF, p->pLevel[i] );
-    return dProgress / p->nVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints statistics about the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverPrintStats( Msat_Solver_t * p )
-{
-    printf("C solver (%d vars; %d clauses; %d learned):\n", 
-        p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
-    printf("starts        : %lld\n", p->Stats.nStarts);
-    printf("conflicts     : %lld\n", p->Stats.nConflicts);
-    printf("decisions     : %lld\n", p->Stats.nDecisions);
-    printf("propagations  : %lld\n", p->Stats.nPropagations);
-    printf("inspects      : %lld\n", p->Stats.nInspects);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Top-level solve.]
-
-  Description [If using assumptions (non-empty 'assumps' vector), you must 
-  call 'simplifyDB()' first to see that no top-level conflict is present 
-  (which would put the solver in an undefined state. If the last argument
-  is given (vProj), the solver enumerates through the satisfying solutions,
-  which are projected on the variables listed in this array. Note that the
-  variables in the array may be complemented, in which case the derived
-  assignment for the variable is complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
-{
-    Msat_SearchParams_t Params = { 0.95, 0.999 };
-    double nConflictsLimit, nLearnedLimit;
-    Msat_Type_t Status;
-    int timeStart = clock();
-    int64 nConflictsOld = p->Stats.nConflicts;
-    int64 nDecisionsOld = p->Stats.nDecisions;
-
-//    p->pFreq = ALLOC( int, p->nVarsAlloc );
-//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
- 
-    if ( vAssumps )
-    {
-        int * pAssumps, nAssumps, i;
-
-        assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );
-
-        nAssumps = Msat_IntVecReadSize( vAssumps );
-        pAssumps = Msat_IntVecReadArray( vAssumps );
-        for ( i = 0; i < nAssumps; i++ )
-        {
-            if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
-            {
-                Msat_QueueClear( p->pQueue );
-                Msat_SolverCancelUntil( p, 0 );
-                return MSAT_FALSE;
-            }
-        }
-    }
-    p->nLevelRoot   = Msat_SolverReadDecisionLevel(p);
-    p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );    
-    nConflictsLimit = 100;
-    nLearnedLimit   = Msat_ClauseVecReadSize(p->vClauses) / 3;
-    Status = MSAT_UNKNOWN;
-    p->nBackTracks = (int)p->Stats.nConflicts;
-    while ( Status == MSAT_UNKNOWN )
-    {
-        if ( p->fVerbose )
-            printf("Solving -- conflicts=%d   learnts=%d   progress=%.4f %%\n", 
-                (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
-        Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
-        nConflictsLimit *= 1.5;
-        nLearnedLimit   *= 1.1;
-        // if the limit on the number of backtracks is given, quit the restart loop
-        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
-            break;
-        // if the runtime limit is exceeded, quit the restart loop
-        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
-            break;
-    }
-    Msat_SolverCancelUntil( p, 0 );
-    p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
-/*
-    PRT( "True solver runtime", clock() - timeStart );
-    // print the statistics
-    {
-        int i, Counter = 0;
-        for ( i = 0; i < p->nVars; i++ )
-            if ( p->pFreq[i] > 0 )
-            {
-                printf( "%d ", p->pFreq[i] );
-                Counter++;
-            }
-        if ( Counter )
-            printf( "\n" );
-        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
-        PRT( "Time", clock() - timeStart );
-    }
-*/
-    return Status;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
deleted file mode 100644
index 05b7f6a9..00000000
--- a/src/sat/msat/msatSolverIo.c
+++ /dev/null
@@ -1,177 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatSolverIo.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Input/output of CNFs.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatSolverIo.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static char * Msat_TimeStamp();
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverPrintAssignment( Msat_Solver_t * p )
-{
-    int i;
-    printf( "Current assignments are: \n" );
-    for ( i = 0; i < p->nVars; i++ )
-        printf( "%d", i % 10 );
-    printf( "\n" );
-    for ( i = 0; i < p->nVars; i++ )
-        if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
-            printf( "." );
-        else
-        {
-            assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
-            if ( MSAT_LITSIGN(p->pAssigns[i]) )
-                printf( "0" );
-            else 
-                printf( "1" );
-        }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverPrintClauses( Msat_Solver_t * p )
-{
-    Msat_Clause_t ** pClauses;
-    int nClauses, i;
-
-    printf( "Original clauses: \n" );
-    nClauses = Msat_ClauseVecReadSize( p->vClauses );
-    pClauses = Msat_ClauseVecReadArray( p->vClauses );
-    for ( i = 0; i < nClauses; i++ )
-    {
-        printf( "%3d: ", i );
-        Msat_ClausePrint( pClauses[i] );
-    }
-
-    printf( "Learned clauses: \n" );
-    nClauses = Msat_ClauseVecReadSize( p->vLearned );
-    pClauses = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nClauses; i++ )
-    {
-        printf( "%3d: ", i );
-        Msat_ClausePrint( pClauses[i] );
-    }
-
-    printf( "Variable activity: \n" );
-    for ( i = 0; i < p->nVars; i++ )
-        printf( "%3d : %.4f\n", i, p->pdActivity[i] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName )
-{
-    FILE * pFile;
-    Msat_Clause_t ** pClauses;
-    int nClauses, i;
-
-    nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
-    for ( i = 0; i < p->nVars; i++ )
-        nClauses += ( p->pLevel[i] == 0 );
-
-    pFile = fopen( pFileName, "wb" );
-    fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );
-
-    nClauses = Msat_ClauseVecReadSize( p->vClauses );
-    pClauses = Msat_ClauseVecReadArray( p->vClauses );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
-
-    nClauses = Msat_ClauseVecReadSize( p->vLearned );
-    pClauses = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nClauses; i++ )
-        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
-
-    // write zero-level assertions
-    for ( i = 0; i < p->nVars; i++ )
-        if ( p->pLevel[i] == 0 )
-            fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );
-
-    fprintf( pFile, "\n" );
-    fclose( pFile );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the time stamp.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Msat_TimeStamp()
-{
-    static char Buffer[100];
-    time_t ltime;
-    char * TimeStamp;
-    // get the current time
-    time( &ltime );
-    TimeStamp = asctime( localtime( &ltime ) );
-    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
-    strcpy( Buffer, TimeStamp );
-    return Buffer;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
deleted file mode 100644
index 11a6540c..00000000
--- a/src/sat/msat/msatSolverSearch.c
+++ /dev/null
@@ -1,629 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatSolverSearch.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [The search part of the solver.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void            Msat_SolverUndoOne( Msat_Solver_t * p );
-static void            Msat_SolverCancel( Msat_Solver_t * p );
-static Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits );
-static void            Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out );
-static void            Msat_SolverReduceDB( Msat_Solver_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the next assumption (Lit).]
-
-  Description [Returns FALSE if immediate conflict.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
-{
-    assert( Msat_QueueReadSize(p->pQueue) == 0 );
-    if ( p->fVerbose )
-        printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit));
-    Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
-//    assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
-//    assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
-    return Msat_SolverEnqueue( p, Lit, NULL );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reverts one variable binding on the trail.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverUndoOne( Msat_Solver_t * p )
-{
-    Msat_Lit_t Lit;
-    Msat_Var_t Var;
-    Lit = Msat_IntVecPop( p->vTrail ); 
-    Var = MSAT_LIT2VAR(Lit);
-    p->pAssigns[Var] = MSAT_VAR_UNASSIGNED;
-    p->pReasons[Var] = NULL;
-    p->pLevel[Var]   = -1;
-//    Msat_OrderUndo( p->pOrder, Var );
-    Msat_OrderVarUnassigned( p->pOrder, Var );
-
-    if ( p->fVerbose )
-        printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reverts to the state before last Msat_SolverAssume().]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverCancel( Msat_Solver_t * p )
-{
-    int c;
-    assert( Msat_QueueReadSize(p->pQueue) == 0 );
-    if ( p->fVerbose )
-    {
-        if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) )
-        {
-            Msat_Lit_t Lit;
-            Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); 
-            printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit));
-        }
-    }
-    for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- )
-        Msat_SolverUndoOne( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reverts to the state at given level.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level )
-{
-    while ( Msat_IntVecReadSize(p->vTrailLim) > Level )
-        Msat_SolverCancel(p);
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Record a clause and drive backtracking.]
-
-  Description [vLits[0] must contain the asserting literal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits )
-{
-    Msat_Clause_t * pC;
-    int Value;
-    assert( Msat_IntVecReadSize(vLits) != 0 );
-    Value = Msat_ClauseCreate( p, vLits, 1, &pC );
-    assert( Value );
-    Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC );
-    assert( Value );
-    if ( pC )
-        Msat_ClauseVecPush( p->vLearned, pC );
-    return pC;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Enqueues one variable assignment.]
-
-  Description [Puts a new fact on the propagation queue and immediately 
-  updates the variable value. Should a conflict arise, FALSE is returned.
-  Otherwise returns TRUE.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
-{
-    Msat_Var_t Var = MSAT_LIT2VAR(Lit);
-
-    // skip literals that are not in the current cone
-    if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) )
-        return 1;
-
-//    assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) );
-    // if the literal is assigned
-    // return 1 if the assignment is consistent
-    // return 0 if the assignment is inconsistent (conflict)
-    if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED )
-        return p->pAssigns[Var] == Lit;
-    // new fact - store it
-    if ( p->fVerbose )
-    {
-//        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
-        printf(L_IND"bind("L_LIT")  ", L_ind, L_lit(Lit));
-        Msat_ClausePrintSymbols( pC );
-    }
-    p->pAssigns[Var] = Lit;
-    p->pLevel[Var]   = Msat_IntVecReadSize(p->vTrailLim);
-//    p->pReasons[Var] = p->pLevel[Var]? pC: NULL;
-    p->pReasons[Var] = pC;
-    Msat_IntVecPush( p->vTrail, Lit );
-    Msat_QueueInsert( p->pQueue, Lit );
-
-    Msat_OrderVarAssigned( p->pOrder, Var );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates the assignments in the queue.]
-
-  Description [Propagates all enqueued facts. If a conflict arises, 
-  the conflicting clause is returned, otherwise NULL.]
-               
-  SideEffects [The propagation queue is empty, even if there was a conflict.]
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p )
-{
-    Msat_ClauseVec_t ** pvWatched = p->pvWatched;
-    Msat_Clause_t ** pClauses;
-    Msat_Clause_t * pConflict;
-    Msat_Lit_t Lit, Lit_out;
-    int i, j, nClauses;
-
-    // propagate all the literals in the queue
-    while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 )
-    {
-        p->Stats.nPropagations++;
-        // get the clauses watched by this literal
-        nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] );
-        pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] );
-        // go through the watched clauses and decide what to do with them
-        for ( i = j = 0; i < nClauses; i++ )
-        {
-            p->Stats.nInspects++;
-            // clear the returned literal
-            Lit_out = -1;
-            // propagate the clause
-            if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) )
-            {   // the clause is unit
-                // "Lit_out" contains the new assignment to be enqueued
-                if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) 
-                { // consistent assignment 
-                    // no changes to the implication queue; the watch is the same too
-                    pClauses[j++] = pClauses[i];
-                    continue;
-                }
-                // remember the reason of conflict (will be returned)
-                pConflict = pClauses[i];
-                // leave the remaning clauses in the same watched list
-                for ( ; i < nClauses; i++ )
-                    pClauses[j++] = pClauses[i];
-                Msat_ClauseVecShrink( pvWatched[Lit], j );
-                // clear the propagation queue
-                Msat_QueueClear( p->pQueue );
-                return pConflict;
-            }
-            // the clause is not unit
-            // in this case "Lit_out" contains the new watch if it has changed
-            if ( Lit_out >= 0 )
-                Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] );
-            else // the watch did not change
-                pClauses[j++] = pClauses[i];
-        }
-        Msat_ClauseVecShrink( pvWatched[Lit], j );
-    }
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simplifies the data base.]
-
-  Description [Simplify all constraints according to the current top-level 
-  assigment (redundant constraints may be removed altogether).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_SolverSimplifyDB( Msat_Solver_t * p )
-{
-    Msat_ClauseVec_t * vClauses;
-    Msat_Clause_t ** pClauses;
-    int nClauses, Type, i, j;
-    int * pAssigns;
-    int Counter;
-
-    assert( Msat_SolverReadDecisionLevel(p) == 0 );
-    if ( Msat_SolverPropagate(p) != NULL )
-        return 0;
-//Msat_SolverPrintClauses( p );
-//Msat_SolverPrintAssignment( p );
-//printf( "Simplification\n" );
-
-    // simplify and reassign clause numbers
-    Counter = 0;
-    pAssigns = Msat_SolverReadAssignsArray( p );
-    for ( Type = 0; Type < 2; Type++ )
-    {
-        vClauses = Type? p->vLearned : p->vClauses;
-        nClauses = Msat_ClauseVecReadSize( vClauses );
-        pClauses = Msat_ClauseVecReadArray( vClauses );
-        for ( i = j = 0; i < nClauses; i++ )
-            if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) )
-                Msat_ClauseFree( p, pClauses[i], 1 );
-            else
-            {
-                pClauses[j++] = pClauses[i];
-                Msat_ClauseSetNum( pClauses[i], Counter++ );
-            }
-        Msat_ClauseVecShrink( vClauses, j );
-    }
-    p->nClauses = Counter;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the clause databased from the useless learnt clauses.]
-
-  Description [Removes half of the learnt clauses, minus the clauses locked 
-  by the current assignment. Locked clauses are clauses that are reason 
-  to a some assignment.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverReduceDB( Msat_Solver_t * p )
-{
-    Msat_Clause_t ** pLearned;
-    int nLearned, i, j;
-    double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned); 
-    // Remove any clause below this activity
-
-    // sort the learned clauses in the increasing order of activity
-    Msat_SolverSortDB( p );
-
-    // discard the first half the clauses (the less active ones)
-    nLearned = Msat_ClauseVecReadSize( p->vLearned );
-    pLearned = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = j = 0; i < nLearned / 2; i++ )
-        if ( !Msat_ClauseIsLocked( p, pLearned[i]) )
-            Msat_ClauseFree( p, pLearned[i], 1 );
-        else
-            pLearned[j++] = pLearned[i];
-    // filter the more active clauses and leave those above the limit
-    for (  ; i < nLearned; i++ )
-        if ( !Msat_ClauseIsLocked( p, pLearned[i] ) && 
-            Msat_ClauseReadActivity(pLearned[i]) < dExtraLim )
-            Msat_ClauseFree( p, pLearned[i], 1 );
-        else
-            pLearned[j++] = pLearned[i];
-    Msat_ClauseVecShrink( p->vLearned, j );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes the learned clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverRemoveLearned( Msat_Solver_t * p )
-{
-    Msat_Clause_t ** pLearned;
-    int nLearned, i;
-
-    // discard the learned clauses
-    nLearned = Msat_ClauseVecReadSize( p->vLearned );
-    pLearned = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nLearned; i++ )
-    {
-        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
-        
-        Msat_ClauseFree( p, pLearned[i], 1 );
-    }
-    Msat_ClauseVecShrink( p->vLearned, 0 );
-    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
-
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-        p->pReasons[i] = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes the recently added clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverRemoveMarked( Msat_Solver_t * p )
-{
-    Msat_Clause_t ** pLearned, ** pClauses;
-    int nLearned, nClauses, i;
-
-    // discard the learned clauses
-    nClauses = Msat_ClauseVecReadSize( p->vClauses );
-    pClauses = Msat_ClauseVecReadArray( p->vClauses );
-    for ( i = p->nClausesStart; i < nClauses; i++ )
-    {
-//        assert( !Msat_ClauseIsLocked( p, pClauses[i]) );
-        Msat_ClauseFree( p, pClauses[i], 1 );
-    }
-    Msat_ClauseVecShrink( p->vClauses, p->nClausesStart );
-
-    // discard the learned clauses
-    nLearned = Msat_ClauseVecReadSize( p->vLearned );
-    pLearned = Msat_ClauseVecReadArray( p->vLearned );
-    for ( i = 0; i < nLearned; i++ )
-    {
-//        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
-        Msat_ClauseFree( p, pLearned[i], 1 );
-    }
-    Msat_ClauseVecShrink( p->vLearned, 0 );
-    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
-/*
-    // undo the previous data
-    for ( i = 0; i < p->nVarsAlloc; i++ )
-    {
-        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
-        p->pReasons[i]   = NULL;
-        p->pLevel[i]     = -1;
-        p->pdActivity[i] = 0.0;
-    }
-    Msat_OrderClean( p->pOrder, p->nVars, NULL );
-    Msat_QueueClear( p->pQueue );
-*/
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Analyze conflict and produce a reason clause.]
-
-  Description [Current decision level must be greater than root level.]
-               
-  SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.]
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out )
-{
-    Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED;
-    Msat_Var_t VarQ, Var;
-    int * pReasonArray, nReasonSize;
-    int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim);
-    int iStep = Msat_IntVecReadSize(p->vTrail) - 1;
-
-    // increment the seen counter
-    p->nSeenId++;
-    // empty the vector array
-    Msat_IntVecClear( vLits_out );
-    Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal)
-    *pLevel_out = 0;
-    do {
-        assert( pC != NULL );  // (otherwise should be UIP)
-        // get the reason of conflict
-        Msat_ClauseCalcReason( p, pC, Lit, p->vReason );
-        nReasonSize  = Msat_IntVecReadSize( p->vReason );
-        pReasonArray = Msat_IntVecReadArray( p->vReason );
-        for ( j = 0; j < nReasonSize; j++ ) {
-            LitQ = pReasonArray[j];
-            VarQ = MSAT_LIT2VAR(LitQ);
-            if ( p->pSeen[VarQ] != p->nSeenId ) {
-                p->pSeen[VarQ] = p->nSeenId;
-
-                // added to better fine-tune the search
-                Msat_SolverVarBumpActivity( p, LitQ );
-
-                // skip all the literals on this decision level
-                if ( p->pLevel[VarQ] == nLevelCur )
-                    pathC++;
-                else if ( p->pLevel[VarQ] > 0 ) { 
-                    // add the literals on other decision levels but
-                    // exclude variables from decision level 0
-                    Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) );
-                    if ( *pLevel_out < p->pLevel[VarQ] )
-                        *pLevel_out = p->pLevel[VarQ];
-                }
-            }
-        }
-        // Select next clause to look at:
-        do {
-//            Lit = Msat_IntVecReadEntryLast(p->vTrail);
-            Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- );
-            Var = MSAT_LIT2VAR(Lit);
-            pC = p->pReasons[Var];
-//            Msat_SolverUndoOne( p );
-        } while ( p->pSeen[Var] != p->nSeenId );
-        pathC--;
-    } while ( pathC > 0 );
-    // we do not unbind the variables above
-    // this will be done after conflict analysis
-
-    Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) );
-    if ( p->fVerbose )
-    {
-        printf( L_IND"Learnt {", L_ind );
-        nReasonSize  = Msat_IntVecReadSize( vLits_out );
-        pReasonArray = Msat_IntVecReadArray( vLits_out );
-        for ( j = 0; j < nReasonSize; j++ ) 
-            printf(" "L_LIT, L_lit(pReasonArray[j]));
-        printf(" } at level %d\n", *pLevel_out); 
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [The search procedure called between the restarts.]
-
-  Description [Search for a satisfying solution as long as the number of 
-  conflicts does not exceed the limit (nConfLimit) while keeping the number 
-  of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use 
-  negative value for nConfLimit or nLearnedLimit to indicate infinity.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars )
-{
-    Msat_Clause_t * pConf;
-    Msat_Var_t Var;
-    int nLevelBack, nConfs, nAssigns, Value;
-    int i;
-
-    assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
-    p->Stats.nStarts++;
-    p->dVarDecay = 1 / pPars->dVarDecay;
-    p->dClaDecay = 1 / pPars->dClaDecay;
-
-    // reset the activities
-    for ( i = 0; i < p->nVars; i++ )
-       p->pdActivity[i] = (double)p->pFactors[i];
-//       p->pdActivity[i] = 0.0;
-
-    nConfs = 0;
-    while ( 1 )
-    {
-        pConf = Msat_SolverPropagate( p );
-        if ( pConf != NULL ){
-            // CONFLICT
-            if ( p->fVerbose )
-            {
-//                printf(L_IND"**CONFLICT**\n", L_ind);
-                printf(L_IND"**CONFLICT**  ", L_ind);
-                Msat_ClausePrintSymbols( pConf );
-            }
-            // count conflicts
-            p->Stats.nConflicts++;
-            nConfs++;
-
-            // if top level, return UNSAT
-            if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot )
-                return MSAT_FALSE;
-
-            // perform conflict analysis
-            Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack );
-            Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack );
-            Msat_SolverRecord( p, p->vTemp );
-
-            // it is important that recording is done after cancelling
-            // because canceling cleans the queue while recording adds to it
-            Msat_SolverVarDecayActivity( p );
-            Msat_SolverClaDecayActivity( p );
-
-        }
-        else{
-            // NO CONFLICT
-            if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) {
-                // Simplify the set of problem clauses:
-//                Value = Msat_SolverSimplifyDB(p);
-//                assert( Value );
-            }
-            nAssigns = Msat_IntVecReadSize( p->vTrail );
-            if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) {
-                // Reduce the set of learnt clauses:
-                Msat_SolverReduceDB(p);
-            }
-
-            Var = Msat_OrderVarSelect( p->pOrder );
-            if ( Var == MSAT_ORDER_UNKNOWN ) {
-                // Model found and stored in p->pAssigns
-                memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars );
-                Msat_QueueClear( p->pQueue );
-                Msat_SolverCancelUntil( p, p->nLevelRoot );
-                return MSAT_TRUE;
-            }
-            if ( nConfLimit > 0 && nConfs > nConfLimit ) {
-                // Reached bound on number of conflicts:
-                p->dProgress = Msat_SolverProgressEstimate( p );
-                Msat_QueueClear( p->pQueue );
-                Msat_SolverCancelUntil( p, p->nLevelRoot );
-                return MSAT_UNKNOWN; 
-            }
-            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
-                // Reached bound on number of conflicts:
-                Msat_QueueClear( p->pQueue );
-                Msat_SolverCancelUntil( p, p->nLevelRoot );
-                return MSAT_UNKNOWN; 
-            }
-            else{
-                // New variable decision:
-                p->Stats.nDecisions++;
-                assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars );
-                Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) );
-                assert( Value );
-            }
-        }
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
deleted file mode 100644
index 3b89d102..00000000
--- a/src/sat/msat/msatSort.c
+++ /dev/null
@@ -1,173 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatSort.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Sorting clauses.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatSort.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 );
-
-// Returns a random float 0 <= x < 1. Seed must never be 0.
-static double drand(double seed) {
-    int q;
-    seed *= 1389796;
-    q = (int)(seed / 2147483647);
-    seed -= (double)q * 2147483647;
-    return seed / 2147483647; }
-
-// Returns a random integer 0 <= x < size. Seed must never be 0.
-static int irand(double seed, int size) {
-    return (int)(drand(seed) * size); }
-
-static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Msat_SolverSort the learned clauses in the increasing order of activity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverSortDB( Msat_Solver_t * p )
-{
-    Msat_ClauseVec_t * pVecClauses;
-    Msat_Clause_t ** pLearned;
-    int nLearned;
-    // read the parameters
-    pVecClauses = Msat_SolverReadLearned( p );
-    nLearned    = Msat_ClauseVecReadSize( pVecClauses );
-    pLearned    = Msat_ClauseVecReadArray( pVecClauses );
-    // Msat_SolverSort the array
-//    qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 
-//            (int (*)(const void *, const void *)) Msat_SolverSortCompare );
-//    printf( "Msat_SolverSorting.\n" );
-    Msat_SolverSort( pLearned, nLearned, 91648253 );
-/*
-    if ( nLearned > 2 )
-    {
-    printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
-    printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
-    printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
-    }
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 )
-{
-    float Value1 = Msat_ClauseReadActivity( *ppC1 );
-    float Value2 = Msat_ClauseReadActivity( *ppC2 );
-    if ( Value1 < Value2 )
-        return -1;
-    if ( Value1 > Value2 )
-        return 1;
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Selection sort for small array size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverSortSelection( Msat_Clause_t ** array, int size )
-{
-    Msat_Clause_t * tmp;
-    int i, j, best_i;
-    for ( i = 0; i < size-1; i++ )
-    {
-        best_i = i;
-        for (j = i+1; j < size; j++)
-        {
-            if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) )
-                best_i = j;
-        }
-        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [The original MiniSat sorting procedure.]
-
-  Description [This procedure is used to preserve trace-equivalence
-  with the orignal C++ implemenation of the solver.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed )
-{
-    if (size <= 15)
-        Msat_SolverSortSelection( array, size );
-    else
-    {
-        Msat_Clause_t *   pivot = array[irand(seed, size)];
-        Msat_Clause_t *   tmp;
-        int              i = -1;
-        int              j = size;
-
-        for(;;)
-        {
-            do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) );
-            do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) );
-
-            if ( i >= j ) break;
-
-            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
-        }
-        Msat_SolverSort(array    , i     , seed);
-        Msat_SolverSort(&array[i], size-i, seed);
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
deleted file mode 100644
index 75f53047..00000000
--- a/src/sat/msat/msatVec.c
+++ /dev/null
@@ -1,495 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatVec.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Integer vector borrowed from Extra.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
-static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t * Msat_IntVecAlloc( int nCap )
-{
-    Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
-    if ( nCap > 0 && nCap < 16 )
-        nCap = 16;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
-{
-    Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = pArray;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
-{
-    Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = ALLOC( int, nSize );
-    memcpy( p->pArray, pArray, sizeof(int) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the integer array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec )
-{
-    Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
-    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the array into another vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec )
-{
-    Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = pVec->pArray;
-    pVec->nSize  = 0;
-    pVec->nCap   = 0;
-    pVec->pArray = NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecFree( Msat_IntVec_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry )
-{
-    int i;
-    Msat_IntVecGrow( p, nSize );
-    p->nSize = nSize;
-    for ( i = 0; i < p->nSize; i++ )
-        p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Msat_IntVecReleaseArray( Msat_IntVec_t * p )
-{
-    int * pArray = p->pArray;
-    p->nCap = 0;
-    p->nSize = 0;
-    p->pArray = NULL;
-    return pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Msat_IntVecReadArray( Msat_IntVec_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecReadSize( Msat_IntVec_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecReadEntryLast( Msat_IntVec_t * p )
-{
-    return p->pArray[p->nSize-1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
-    p->nCap   = nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecClear( Msat_IntVec_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecPush( Msat_IntVec_t * p, int Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Msat_IntVecGrow( p, 16 );
-        else
-            Msat_IntVecGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Add the element while ensuring uniqueness.]
-
-  Description [Returns 1 if the element was found, and 0 if it was new. ]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return 1;
-    Msat_IntVecPush( p, Entry );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the element while sorting in the increasing order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease )
-{
-    int Entry1, Entry2;
-    int i;
-    Msat_IntVecPushUnique( p, Entry );
-    // find the p of the node
-    for ( i = p->nSize-1; i > 0; i-- )
-    {
-        Entry1 = p->pArray[i  ];
-        Entry2 = p->pArray[i-1];
-        if ( fIncrease && Entry1 >= Entry2 || 
-            !fIncrease && Entry1 <= Entry2 )
-            break;
-        p->pArray[i  ] = Entry2;
-        p->pArray[i-1] = Entry1;
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the last entry and removes it from the list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecPop( Msat_IntVec_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their integer value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse )
-{
-    if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
-                (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
-    else
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
-                (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecSortCompare1( int * pp1, int * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Msat_IntVecSortCompare2( int * pp1, int * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 > *pp2 )
-        return -1;
-    if ( *pp1 < *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-