diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.C')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 14b64b555..063332e74 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Constructor/Destructor: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { SimpSolver::SimpSolver() : grow (0) @@ -226,11 +227,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou for (int i = 0; i < qs.size(); i++){ if (var(qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) + if (var(ps[j]) == var(qs[i])) { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -258,11 +260,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v) for (int i = 0; i < qs.size(); i++){ if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) + if (var(__ps[j]) == var(__qs[i])) { if (__ps[j] == ~__qs[i]) return false; else goto next; + } } next:; } @@ -701,5 +704,6 @@ void SimpSolver::toDimacs(const char* file) fprintf(stderr, "could not open file %s\n", file); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ |