satisfiability can be run as sequential in order to get speed up
[charm.git] / examples / charm++ / satisfiability / par_Solver.h
index b6d4fbabaa5f17fb36ba8f060da3036f1e3f555e..9ee99aea9cbd035de4c00d1066c4d13f6aa38cd9 100644 (file)
@@ -10,11 +10,8 @@ public:
     
     par_SolverState();
 
-    int nVars();
-
     int clausesSize();
     
-    int newVar (bool polarity = true, bool dvar = true);
     
     bool addClause(CkVec<par_Lit>& lits);
 
@@ -29,7 +26,6 @@ public:
     CkVec<par_Clause>   clauses;
     par_Lit             assigned_lit;
     int             var_size;
-    int             unsolved_vars;
     int             unsolved_clauses;
 
     int             var_frequency; // 1, -1, 1 freq = 3
@@ -66,7 +62,6 @@ public:
        }
 
        new_state->var_size = org->var_size;
-       new_state->unsolved_vars = org->unsolved_vars;
        new_state->occurrence.resize(org->occurrence.size());
        new_state->positive_occurrence.resize(org->occurrence.size());
        for(int _i=0; _i<org->occurrence.size(); _i++){