From f0f5100da1cc1254749ef5823e2a1213c1276b6c Mon Sep 17 00:00:00 2001
From: Mark Liffiton <liffiton@gmail.com>
Date: Mon, 23 Sep 2013 16:10:12 -0500
Subject: [PATCH] Put the implies() method in the right place.
---
core/Solver.cc | 28 ----------------------------
core/Solver.h | 3 ---
minicard/Solver.cc | 28 ++++++++++++++++++++++++++++
minicard/Solver.h | 3 +++
4 files changed, 31 insertions(+), 31 deletions(-)
diff --git a/core/Solver.cc b/core/Solver.cc
index d8204fb..7da7f18 100644
--- 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
index 66741fa..90119e5 100644
--- 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
index 5d02b32..05e4ddb 100644
--- 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
index dec8e8a..3ffb7de 100644
--- 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);