Version abc60803

3 files changed, 22 insertions, 1 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;       //