diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
commit | d54c761087af01874ea6674111888cb94ffa4ee6 (patch) | |
tree | 2f196940df9b488a1298ccfdee9bf1b54a70ccac /src/prop | |
parent | e148b0a99917b21499b2f596aa22403559baf677 (diff) |
fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 50 |
1 files changed, 38 insertions, 12 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 41c0c4ac9..2eadbdf22 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -31,19 +31,26 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA using namespace BVMinisat; -// purely debugging functions -void printDebug2 (BVMinisat::Lit l) { - std::cout<< (sign(l) ? "-" : "") << var(l) + 1 << std::endl; +namespace CVC4 { + +#define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] " + +std::ostream& operator << (std::ostream& out, const BVMinisat::Lit& l) { + out << (sign(l) ? "-" : "") << var(l) + 1; + return out; } -void printDebug2 (BVMinisat::Clause& c) { +std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - std::cout << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + if (i > 0) { + out << " "; + } + out << c[i]; } - std::cout << std::endl; + return out; } - +} //================================================================================================= // Options: @@ -243,7 +250,8 @@ bool Solver::satisfied(const Clause& c) const { // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl; + for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; if (marker[x] == 2) marker[x] = 1; @@ -502,6 +510,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) trail.push_(p); if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) { if (notify) { + Debug("bvminisat::explain") << OUTPUT_TAG << "propagating " << p << std::endl; notify->notify(p); } } @@ -757,6 +766,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (assumption) { assert(decisionLevel() < assumptions.size()); analyzeFinal(p, conflict); + Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl; return l_False; } @@ -779,17 +789,24 @@ lbool Solver::search(int nof_conflicts, UIP uip) // NO CONFLICT if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ // 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()) + if (decisionLevel() == 0 && !simplify()) { + Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; return l_False; + } - if (learnts.size()-nAssigns() >= max_learnts) + // We can't erase clauses if there is unprocessed assumptions, there might be some + // propagationg we need to redu + if (decisionLevel() >= assumptions.size() && learnts.size()-nAssigns() >= max_learnts) { // Reduce the set of learnt clauses: + Debug("bvminisat::search") << OUTPUT_TAG << " cleaning up database" << std::endl; reduceDB(); + } Lit next = lit_Undef; while (decisionLevel() < assumptions.size()){ @@ -800,6 +817,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) newDecisionLevel(); }else if (value(p) == l_False){ analyzeFinal(~p, conflict); + Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; return l_False; }else{ marker[var(p)] = 2; @@ -811,6 +829,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (next == lit_Undef){ if (only_bcp) { + Debug("bvminisat::search") << OUTPUT_TAG << " only bcp, skipping rest of the problem" << std::endl; return l_True; } @@ -818,9 +837,11 @@ lbool Solver::search(int nof_conflicts, UIP uip) decisions++; next = pickBranchLit(); - if (next == lit_Undef) + if (next == lit_Undef) { + Debug("bvminisat::search") << OUTPUT_TAG << " satisfiable" << std::endl; // Model found: return l_True; + } } // Increase decision level and enqueue 'next' @@ -930,11 +951,16 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { vec<Lit> queue; queue.push(p); - __gnu_cxx::hash_set<Var> visited; + Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl; + + __gnu_cxx::hash_set<Var> visited; visited.insert(var(p)); while(queue.size() > 0) { Lit l = queue.last(); + + Debug("bvminisat::explain") << OUTPUT_TAG << "processing " << l << std::endl; + assert(value(l) == l_True); queue.pop(); if (reason(var(l)) == CRef_Undef) { |