diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
commit | 77ff33bc6be64f338f035bd9d077737f83280944 (patch) | |
tree | 3593a4f931ca107cdcb9b2e6891f7008f6d3be76 /src/prop/bvminisat | |
parent | 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 (diff) |
several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 13 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 1 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index d53507def..41c0c4ac9 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -101,6 +101,7 @@ Solver::Solver(CVC4::context::Context* c) : , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + , need_to_propagate(false) , only_bcp(false) , clause_added(false) , ok (true) @@ -187,13 +188,12 @@ bool Solver::addClause_(vec<Lit>& ps) else if (ps.size() == 1){ uncheckedEnqueue(ps[0]); return ok = (propagate() == CRef_Undef); - }else{ + } else { CRef cr = ca.alloc(ps, false); clauses.push(cr); attachClause(cr); } - - return true; + return ok; } void Solver::attachClause(CRef cr) { @@ -514,8 +514,8 @@ void Solver::popAssumption() { } lbool Solver::assertAssumption(Lit p, bool propagate) { - - assert(marker[var(p)] == 1); + + // assert(marker[var(p)] == 1); if (decisionLevel() > assumptions.size()) { cancelUntil(assumptions.size()); @@ -759,7 +759,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) analyzeFinal(p, conflict); return l_False; } - + varDecayActivity(); claDecayActivity(); @@ -927,7 +927,6 @@ lbool Solver::solve_() // void Solver::explain(Lit p, std::vector<Lit>& explanation) { - vec<Lit> queue; queue.push(p); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index ae5efd81e..ea8e98c4c 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -190,6 +190,7 @@ public: marker[var] = 1; } + bool need_to_propagate; // true if we added new clauses, set to true in propagation bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} void explain(Lit l, std::vector<Lit>& explanation); |