fixed ipasir mode for use with simp-solver

fkutzner · Jun 8, 2017 · b80241f · b80241f
1 parent a751d66
commit b80241f
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 21 deletions.
diff --git a/src/candy/core/Solver.h b/src/candy/core/Solver.h
@@ -764,9 +764,6 @@ template<class PickBranchLitT>
 template<typename Iterator>
 bool Solver<PickBranchLitT>::addClause(Iterator begin, Iterator end) {
     assert(decisionLevel() == 0);
-    if (!ok) {
-        return false;
-    }
 
     uint32_t size = static_cast<uint32_t>(std::distance(begin, end));
 
@@ -780,7 +777,7 @@ bool Solver<PickBranchLitT>::addClause(Iterator begin, Iterator end) {
         }
         else if (value(*begin) == l_True) {
             vardata[var(*begin)].reason = nullptr;
-            return true;
+            return ok;
         }
         else {
             return ok = false;
@@ -792,7 +789,7 @@ bool Solver<PickBranchLitT>::addClause(Iterator begin, Iterator end) {
         attachClause(cr);
     }
 
-    return true;
+    return ok;
 }
 
 template<class PickBranchLitT>

diff --git a/src/candy/simp/SimpSolver.h b/src/candy/simp/SimpSolver.h
@@ -660,28 +660,34 @@ bool SimpSolver<PickBranchLitT>::eliminateVar(Var v) {
 
     // produce clauses in cross product
     for (Clause* pc : pos) for (Clause* nc : neg) {
-        if (merge(*pc, *nc, v, resolvent) && !this->addClause(resolvent)) {
-            return false;
-        } else {
+        if (merge(*pc, *nc, v, resolvent)) {
             this->certificate->added(resolvent.begin(), resolvent.end());
+            this->addClause(resolvent);
         }
     }
 
-    for (auto it = this->clauses.begin() + size; it != this->clauses.end(); it++) {
-        elimAttach(*it);
-    }
+    if (!this->isInConflictingState()) {
+        for (auto it = this->clauses.begin() + size; it != this->clauses.end(); it++) {
+            elimAttach(*it);
+        }
+        for (Clause* c : cls) {
+            this->removeClause(c);
+            elimDetach(c, false);
+        }
+        occurs[v].clear();
+        this->watches[mkLit(v)].clear();
+        this->watches[~mkLit(v)].clear();
+        this->watchesBin[mkLit(v)].clear();
+        this->watchesBin[~mkLit(v)].clear();
 
-    for (Clause* c : cls) {
-        this->removeClause(c);
-        elimDetach(c, false);
+        return backwardSubsumptionCheck();
+    }
+    else {
+        for (Clause* c : cls) {
+            this->removeClause(c);
+        }
+        return false;
     }
-
-    // free references to eliminated variable
-    occurs[v].clear();
-    this->watches[mkLit(v)].clear();
-    this->watches[~mkLit(v)].clear();
-
-    return backwardSubsumptionCheck();
 }
 
 template<class PickBranchLitT>
@@ -732,6 +738,9 @@ void SimpSolver<PickBranchLitT>::setupEliminate(bool full) {
             setFrozen(v, true);
         }
     }
+    for (Lit lit : this->assumptions) {
+        setFrozen(var(lit), true);
+    }
 }
 
 template<class PickBranchLitT>
@@ -742,6 +751,9 @@ void SimpSolver<PickBranchLitT>::cleanupEliminate() {
             setFrozen(v, false);
         }
     }
+    for (Lit lit : this->assumptions) {
+        setFrozen(var(lit), false);
+    }
 
     n_occ.clear();
     touched.clear();