Version abc60803

9 files changed, 36 insertions, 6 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index 832bc0cf..100b823b 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -209,6 +209,23 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars)
     s->nPrefVars = nPrefVars;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the preferred variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_SolverSetFactors(solver * s, int * pFactors)
+{
+    assert( s->factors == NULL );
+    s->factors = pFactors;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 548abd1d..f2642c38 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -254,6 +254,7 @@ static inline void act_var_rescale(solver* s) {
 static inline void act_var_bump(solver* s, int v) {
     double* activity = s->activity;
     if ((activity[v] += s->var_inc) > 1e100)
+//    if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100)
         act_var_rescale(s);
 
     //printf("bump %d %f\n", v-1, activity[v]);
@@ -947,6 +948,7 @@ solver* solver_new(void)
     // initialize arrays
     s->wlists    = 0;
     s->activity  = 0;
+    s->factors   = 0;
     s->assigns   = 0;
     s->orderpos  = 0;
     s->reasons   = 0;
@@ -1039,9 +1041,9 @@ void solver_delete(solver* s)
         free(s->trail    );
         free(s->tags     );
     }
-
     if ( s->pJMan )     Asat_JManStop( s );
     if ( s->pPrefVars ) free( s->pPrefVars );
+    if ( s->factors )   free( s->factors );
     free(s);
 }
 
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 05e9dafa..7edfb537 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -89,6 +89,7 @@ extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        int incrementVars);
 extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
 extern void    Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars );
+extern void    Asat_SolverSetFactors( solver * s, int * pFactors );
 
 // J-frontier support
 extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
@@ -127,6 +128,7 @@ struct solver_t
 
     vec*     wlists;        // 
     double*  activity;      // A heuristic measurement of the activity of a variable.
+    int *    factors;       // the factor of variable activity
     lbool*   assigns;       // Current values of variables.
     int*     orderpos;      // Index in variable order.
     clause** reasons;       //
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index aa28a4f2..1a56cf0e 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -326,7 +326,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
         Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat );
+        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
 
  
@@ -543,7 +543,7 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t
         Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat );
+        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
    // get the logic cone
 clk = clock();
@@ -642,7 +642,7 @@ int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_
         Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
-        Msat_SolverAddVar( p->pSat );
+        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
    // get the logic cone
 clk = clock();
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 5f8603a7..1d9c0005 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -80,7 +80,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 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 );
+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 );
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index 0947d6d5..f808d9bc 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -46,6 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
         return;
     Var = MSAT_LIT2VAR(Lit);
     if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
+//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 03e7b873..15932c67 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -119,6 +119,7 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
+    int *               pLevels;     // the levels of the variables
     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.
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index e3d85774..8c1542df 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -174,8 +174,12 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
+    p->pLevels    = ALLOC( int, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
+    {
         p->pdActivity[i] = 0;
+        p->pLevels = 0;
+    }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
     p->pModel    = ALLOC( int, p->nVarsAlloc ); 
@@ -239,6 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
+    p->pLevels    = REALLOC( int, p->pLevels, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
         p->pdActivity[i] = 0;
 
@@ -394,6 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
+    FREE( p->pLevels );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 397dbcdc..f9fee73c 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -39,10 +39,11 @@
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p )
+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;
 }