summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/core/Solver.cc28
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc52
-rw-r--r--src/prop/minisat/core/Solver.cc19
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc52
4 files changed, 91 insertions, 60 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 372f8eb04..a4b0248e0 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -357,8 +357,11 @@ void Solver::cancelUntil(int level) {
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (marker[x] == 2) marker[x] = 1;
- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
- polarity[x] = sign(trail[c]);
+ if (phase_saving > 1
+ || ((phase_saving == 1) && c > trail_lim.last()))
+ {
+ polarity[x] = sign(trail[c]);
+ }
insertVarOrder(x); }
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
@@ -1080,16 +1083,19 @@ lbool Solver::search(int nof_conflicts, UIP uip)
cancelUntil(assumptions.size());
throw e;
}
-
- if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
- !isWithinBudget) {
- // Reached bound on number of conflicts:
- Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
- progress_estimate = progressEstimate();
- cancelUntil(assumptions.size());
- return l_Undef;
+
+ if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
+ && conflictC >= nof_conflicts)
+ || !isWithinBudget)
+ {
+ // Reached bound on number of conflicts:
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " restarting " << std::endl;
+ progress_estimate = progressEstimate();
+ cancelUntil(assumptions.size());
+ return l_Undef;
}
-
+
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 2fa8d472d..698d2a776 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -255,17 +255,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
- 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 (ps[j] == ~qs[i])
- return false;
- else
- goto next;
- out_clause.push(qs[i]);
+ 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 (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ out_clause.push(qs[i]);
+ }
+ next:;
}
for (int i = 0; i < ps.size(); i++)
@@ -289,17 +295,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
size = ps.size()-1;
- 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 (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
- size++;
+ 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 (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ size++;
+ }
+ next:;
}
return true;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dbe417dbc..c8a2e16c2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1349,15 +1349,16 @@ lbool Solver::search(int nof_conflicts)
check_type = CHECK_WITH_THEORY;
}
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts ||
- !withinBudget(options::satConflictStep())) {
- // Reached bound on number of conflicts:
- progress_estimate = progressEstimate();
- cancelUntil(0);
- // [mdeters] notify theory engine of restarts for deferred
- // theory processing
- proxy->notifyRestart();
- return l_Undef;
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+ || !withinBudget(options::satConflictStep()))
+ {
+ // Reached bound on number of conflicts:
+ progress_estimate = progressEstimate();
+ cancelUntil(0);
+ // [mdeters] notify theory engine of restarts for deferred
+ // theory processing
+ proxy->notifyRestart();
+ return l_Undef;
}
// Simplify the set of problem clauses:
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 96fea2147..a101a0c2d 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -256,17 +256,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
- 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 (ps[j] == ~qs[i])
- return false;
- else
- goto next;
- out_clause.push(qs[i]);
+ 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 (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ out_clause.push(qs[i]);
+ }
+ next:;
}
for (int i = 0; i < ps.size(); i++)
@@ -290,17 +296,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
size = ps.size()-1;
- 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 (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
- size++;
+ 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 (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ size++;
+ }
+ next:;
}
return true;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback