Version abc80130

1 files changed, 64 insertions, 397 deletions

diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 53057fc3..17201e58 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -17,7 +17,6 @@
 ***********************************************************************/
 
 #include "fraigInt.h"
-#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -34,7 +33,6 @@ static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pN
 static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 //static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 
 extern void * Msat_ClauseVecReadEntry( void * p, int i );
 
@@ -43,10 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
 // The best way seems to be fanins followed by fanouts. Slight changes to this order
 // leads to big degradation in quality.
 
-static int nMuxes;
-
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -60,13 +56,13 @@ static int nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit )
+int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
 {
     if ( pNode1 == pNode2 )
         return 1;
     if ( pNode1 == Fraig_Not(pNode2) )
         return 0;
-    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
+    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit );
 }
 
 /**Function*************************************************************
@@ -99,9 +95,9 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
         // skip nodes that are different according to simulation
         if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
             continue;
-        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
+        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) )
         {
-            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
+            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
             else
                 p->vOutputs->pArray[i] = p->pConst1;
@@ -109,7 +105,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
     }
     if ( p->fVerboseP ) 
     {
-//        PRT( "Final miter proof time", clock() - clk );
+        PRT( "Final miter proof time", clock() - clk );
     }
 }
 
@@ -127,158 +123,26 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
-    int i;
     FREE( p->pModel );
-    for ( i = 0; i < p->vOutputs->nSize; i++ )
-    {
-        // get the output node (it can be complemented!)
-        pNode = p->vOutputs->pArray[i];
-        // if the miter is constant 0, the problem is UNSAT
-        if ( pNode == Fraig_Not(p->pConst1) )
-            continue;
-        // consider the special case when the miter is constant 1
-        if ( pNode == p->pConst1 )
-        {
-            // in this case, any counter example will do to distinquish it from constant 0
-            // here we pick the counter example composed of all zeros
-            p->pModel = Fraig_ManAllocCounterExample( p );
-            return 0;
-        }
-        // save the counter example
-        p->pModel = Fraig_ManSaveCounterExample( p, pNode );
-        // if the model is not found, return undecided
-        if ( p->pModel == NULL )
-            return -1;
-        else
-            return 0;
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_MarkTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    // skip the visited node
-    if ( pNode->TravId == pMan->nTravIds )
-        return 0;
-    pNode->TravId = pMan->nTravIds;
-    // skip the PI node
-    if ( pNode->NumPi >= 0 )
-        return 1;
-    // check the children
-    return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) +
-           Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_MarkTfi2_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    // skip the visited node
-    if ( pNode->TravId == pMan->nTravIds )
-        return 0;
-    // skip the boundary node
-    if ( pNode->TravId == pMan->nTravIds-1 )
-    {
-        pNode->TravId = pMan->nTravIds;
-        return 1;
-    }
-    pNode->TravId = pMan->nTravIds;
-    // skip the PI node
-    if ( pNode->NumPi >= 0 )
-        return 1;
-    // check the children
-    return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) +
-           Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_MarkTfi3_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    // skip the visited node
-    if ( pNode->TravId == pMan->nTravIds )
+    // get the output node (it can be complemented!)
+    pNode = p->vOutputs->pArray[0];
+    // if the miter is constant 0, the problem is UNSAT
+    if ( pNode == Fraig_Not(p->pConst1) )
         return 1;
-    // skip the boundary node
-    if ( pNode->TravId == pMan->nTravIds-1 )
+    // consider the special case when the miter is constant 1
+    if ( pNode == p->pConst1 )
     {
-        pNode->TravId = pMan->nTravIds;
-        return 1;
-    }
-    pNode->TravId = pMan->nTravIds;
-    // skip the PI node
-    if ( pNode->NumPi >= 0 )
+        // in this case, any counter example will do to distinquish it from constant 0
+        // here we pick the counter example composed of all zeros
+        p->pModel = Fraig_ManAllocCounterExample( p );
         return 0;
-    // check the children
-    return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) *
-           Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
-{
-    int NumPis, NumCut, fContain;
-
-    // mark the TFI of pNew
-    p->nTravIds++;
-    NumPis = Fraig_MarkTfi_rec( p, pNew );
-    printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level );
-
-    // check if the old is in the TFI
-    if ( pOld->TravId == p->nTravIds )
-    {
-        printf( "* " );
-        return;
     }
-
-    // count the boundary of nodes in pOld
-    p->nTravIds++;
-    NumCut = Fraig_MarkTfi2_rec( p, pOld );
-    printf( "%d", NumCut );
-
-    // check if the new is contained in the old's support
-    p->nTravIds++;
-    fContain = Fraig_MarkTfi3_rec( p, pNew );
-    printf( "%c ", fContain? '+':'-' );
+    // save the counter example
+    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
+    // if the model is not found, return undecided
+    if ( p->pModel == NULL )
+        return -1;
+    return 0;
 }
 
 
@@ -296,40 +160,34 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
+int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
 {
     int RetValue, RetValue1, i, fComp, clk;
     int fVerbose = 0;
-    int fSwitch = 0;
 
     // make sure the nodes are not complemented
     assert( !Fraig_IsComplement(pNew) );
     assert( !Fraig_IsComplement(pOld) );
     assert( pNew != pOld );
 
-    // if at least one of the nodes is a failed node, perform adjustments:
-    // if the backtrack limit is small, simply skip this node
-    // if the backtrack limit is > 10, take the quare root of the limit
-    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
-    {
-        p->nSatFails++;
-//            return 0;
-//        if ( nBTLimit > 10 )
-//            nBTLimit /= 10;
-        if ( nBTLimit <= 10 )
-            return 0;
-        nBTLimit = (int)sqrt(nBTLimit);
-//        fSwitch = 1;
-    }
-
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-        Fraig_ManCreateSolver( p );
+    {
+        extern int timeSelect;
+        extern int timeAssign;
+        // allocate data for SAT solving
+        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
+        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
+        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
+        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
+        timeSelect = 0;
+        timeAssign = 0;
+    }
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
+        Msat_SolverAddVar( p->pSat );
 
 
  
@@ -341,26 +199,17 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
     }
 */
 
-    nMuxes = 0;
-
 
     // get the logic cone
 clk = clock();
-//    Fraig_VarsStudy( p, pOld, pNew );
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
 p->timeTrav += clock() - clk;
 
-//    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
-//    PRT( "Time", clock() - clk );
-
 if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
-    // prepare variable activity
-    Fraig_SetActivity( p, pOld, pNew );
-
     // get the complemented attribute
     fComp = Fraig_NodeComparePhase( pOld, pNew );
 //Msat_SolverPrintClauses( p->pSat );
@@ -371,18 +220,14 @@ if ( fVerbose )
     Msat_SolverPrepare( p->pSat, p->vVarsInt );
 //p->time3 += clock() - clk;
 
-
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
     Msat_IntVecClear( p->vProj );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
-
-//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
-
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
@@ -415,31 +260,13 @@ PRT( "time", clock() - clk );
 
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
-
-//        if ( pOld->fFailTfo || pNew->fFailTfo )
-//            printf( "*" );
-//        printf( "s(%d)", pNew->Level );
-        if ( fSwitch )
-             printf( "s(%d)", pNew->Level );
         p->nSatCounter++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-
-//        if ( pOld->fFailTfo || pNew->fFailTfo )
-//            printf( "*" );
-//        printf( "T(%d)", pNew->Level );
-
-        // mark the node as the failed node
-        if ( pOld != p->pConst1 ) 
-            pOld->fFailTfo = 1;
-        pNew->fFailTfo = 1;
-//        p->nSatFails++;
-        if ( fSwitch )
-             printf( "T(%d)", pNew->Level );
-        p->nSatFailsReal++;
+        p->nSatFails++;
         return 0;
     }
 
@@ -459,9 +286,8 @@ p->time3 += clock() - clk;
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
-
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += clock() - clk;
@@ -493,42 +319,17 @@ PRT( "time", clock() - clk );
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
         p->nSatCounter++;
-
-//        if ( pOld->fFailTfo || pNew->fFailTfo )
-//            printf( "*" );
-//        printf( "s(%d)", pNew->Level );
-        if ( fSwitch )
-             printf( "s(%d)", pNew->Level );
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-
-//        if ( pOld->fFailTfo || pNew->fFailTfo )
-//            printf( "*" );
-//        printf( "T(%d)", pNew->Level );
-        if ( fSwitch )
-             printf( "T(%d)", pNew->Level );
-
-        // mark the node as the failed node
-        pOld->fFailTfo = 1;
-        pNew->fFailTfo = 1;
-//        p->nSatFails++;
-        p->nSatFailsReal++;
+        p->nSatFails++;
         return 0;
     }
 
     // return SAT proof
     p->nSatProof++;
-
-//    if ( pOld->fFailTfo || pNew->fFailTfo )
-//        printf( "*" );
-//    printf( "u(%d)", pNew->Level );
-
-    if ( fSwitch )
-         printf( "u(%d)", pNew->Level );
-
     return 1;
 }
 
@@ -558,12 +359,32 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-        Fraig_ManCreateSolver( p );
+    {
+        extern int timeSelect;
+        extern int timeAssign;
+        // allocate data for SAT solving
+        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
+        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
+        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
+        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
+        timeSelect = 0;
+        timeAssign = 0;
+    }
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
+        Msat_SolverAddVar( p->pSat );
+
 
-   // get the logic cone
+/*
+    {
+        Fraig_Node_t * ppNodes[2] = { pOld, pNew };
+        extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
+        Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
+    }
+*/
+
+
+    // get the logic cone
 clk = clock();
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
@@ -590,7 +411,7 @@ if ( fVerbose )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
@@ -622,8 +443,8 @@ if ( fVerbose )
 PRT( "time", clock() - clk );
 }
         // record the counter example
-        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
-        p->nSatCounterImp++;
+//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
+//        p->nSatCounterImp++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
@@ -634,96 +455,6 @@ p->time3 += clock() - clk;
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Prepares the SAT solver to run on the two nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
-{
-    Fraig_Node_t * pNode1R, * pNode2R;
-    int RetValue, RetValue1, i, clk;
-    int fVerbose = 0;
-
-    pNode1R = Fraig_Regular(pNode1);
-    pNode2R = Fraig_Regular(pNode2);
-    assert( pNode1R != pNode2R );
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-        Fraig_ManCreateSolver( p );
-    // make sure the SAT solver has enough variables
-    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
-
-   // get the logic cone
-clk = clock();
-    Fraig_OrderVariables( p, pNode1R, pNode2R );
-//    Fraig_PrepareCones( p, pNode1R, pNode2R );
-p->timeTrav += clock() - clk;
-
-    ////////////////////////////////////////////
-    // prepare the solver to run incrementally on these variables
-//clk = clock();
-    Msat_SolverPrepare( p->pSat, p->vVarsInt );
-//p->time3 += clock() - clk;
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-    Msat_IntVecClear( p->vProj );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
-    // run the solver
-clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
-p->timeSat += clock() - clk;
-
-    if ( RetValue1 == MSAT_FALSE )
-    {
-//p->time1 += clock() - clk;
-
-if ( fVerbose )
-{
-    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
-}
-
-        // add the clause
-        Msat_IntVecClear( p->vProj );
-        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
-        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
-        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
-        assert( RetValue );
-//        p->nSatProofImp++;
-        return 1;
-    }
-    else if ( RetValue1 == MSAT_TRUE )
-    {
-//p->time2 += clock() - clk;
-
-if ( fVerbose )
-{
-    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
-}
-        // record the counter example
-//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
-        p->nSatCounterImp++;
-        return 0;
-    }
-    else // if ( RetValue1 == MSAT_UNKNOWN )
-    {
-p->time3 += clock() - clk;
-        p->nSatFailsImp++;
-        return 0;
-    }
-}
 
 
 /**Function*************************************************************
@@ -755,7 +486,6 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
     Fraig_PrepareCones_rec( pMan, pNew );
     Fraig_PrepareCones_rec( pMan, pOld );
 
-
 /*
     nVars = Msat_IntVecReadSize( pMan->vVarsInt );
     pVars = Msat_IntVecReadArray( pMan->vVarsInt );
@@ -919,8 +649,6 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
                 Fraig_SupergateAddClausesMux( pMan, pNode );
 //                Fraig_DetectFanoutFreeConeMux( pMan, pNode );
-
-                nMuxes++;
             }
             else
             {
@@ -1255,33 +983,6 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
     assert( RetValue );
-
-    // two additional clauses
-    // t' & e' -> f'
-    // t  & e  -> f 
-
-    // t  + e   + f'
-    // t' + e'  + f 
-
-    if ( VarT == VarE )
-    {
-//        assert( fCompT == !fCompE );
-        return;
-    }
-
-    Msat_IntVecClear( p->vProj );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
-    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
-    assert( RetValue );
-    Msat_IntVecClear( p->vProj );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
-    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
-    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
-    assert( RetValue );
-
 }
 
 
@@ -1414,40 +1115,6 @@ printf( "%d(%d)", vFanins->nSize, nCubes );
 }
 
 
-
-/**Function*************************************************************
-
-  Synopsis    [Collect variables using their proximity from the nodes.]
-
-  Description [This procedure creates a variable order based on collecting
-  first the nodes that are the closest to the given two target nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
-{
-    Fraig_Node_t * pNode;
-    int i, Number, MaxLevel;
-    float * pFactors = Msat_SolverReadFactors(pMan->pSat);
-    if ( pFactors == NULL )
-        return;
-    MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
-    // create the variable order
-    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
-    {
-        // get the new node on the frontier
-        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
-        pNode = pMan->vNodes->pArray[Number];
-        pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
-//        if ( pNode->Num % 50 == 0 )
-//        printf( "(%d) %.2f  ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
-    }
-//    printf( "\n" );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////