Put the implies() method in the right place.

liffiton · Sep 23, 2013 · f0f5100 · f0f5100
1 parent b60be3d
commit f0f5100
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 31 deletions.
diff --git a/core/Solver.cc b/core/Solver.cc
@@ -792,34 +792,6 @@ lbool Solver::solve_()
     return status;
 }
 
-bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out, bool all=false)
-{
-    trail_lim.push(trail.size());
-    for (int i = 0; i < assumps.size(); i++){
-        Lit a = assumps[i];
-
-        if (value(a) == l_False){
-            cancelUntil(0);
-            return false;
-        }else if (value(a) == l_Undef)
-            uncheckedEnqueue(a);
-    }
-
-    // Adapted from similar function in MiniSat
-    // Added option to get all implications, including level 0 assignments.
-    unsigned trail_before = (all) ? 0 : trail.size();
-    bool     ret          = true;
-    if (propagate() == CRef_Undef){
-        out.clear();
-        for (int j = trail_before; j < trail.size(); j++)
-            out.push(trail[j]);
-    }else
-        ret = false;
-
-    cancelUntil(0);
-    return ret;
-}
-
 //=================================================================================================
 // Writing CNF to DIMACS:
 // 

diff --git a/core/Solver.h b/core/Solver.h
@@ -64,9 +64,6 @@ class Solver {
     bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
-    // Adopted from newer version of Minisat
-    bool    implies      (const vec<Lit>& assumps, vec<Lit>& out, bool all);
-
     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
     void    toDimacs     (const char *file, const vec<Lit>& assumps);
     void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);

diff --git a/minicard/Solver.cc b/minicard/Solver.cc
@@ -1089,6 +1089,34 @@ lbool Solver::solve_()
     return status;
 }
 
+bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out, bool all=false)
+{
+    trail_lim.push(trail.size());
+    for (int i = 0; i < assumps.size(); i++){
+        Lit a = assumps[i];
+
+        if (value(a) == l_False){
+            cancelUntil(0);
+            return false;
+        }else if (value(a) == l_Undef)
+            uncheckedEnqueue(a);
+    }
+
+    // Adapted from similar function in MiniSat
+    // Added option to get all implications, including level 0 assignments.
+    unsigned trail_before = (all) ? 0 : trail.size();
+    bool     ret          = true;
+    if (propagate() == CRef_Undef){
+        out.clear();
+        for (int j = trail_before; j < trail.size(); j++)
+            out.push(trail[j]);
+    }else
+        ret = false;
+
+    cancelUntil(0);
+    return ret;
+}
+
 //=================================================================================================
 // Writing CNF to DIMACS:
 // 

diff --git a/minicard/Solver.h b/minicard/Solver.h
@@ -76,6 +76,9 @@ class Solver {
     bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
+    // Adopted from newer version of Minisat
+    bool    implies      (const vec<Lit>& assumps, vec<Lit>& out, bool all);
+
     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
     void    toDimacs     (const char *file, const vec<Lit>& assumps);
     void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);