From 5e482def18b824ca573d5d424f9a4b57a5f95ec1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Feb 2018 07:27:32 -0800 Subject: [PATCH] fix local search encoding bug Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 +- src/sat/ba_solver.h | 2 +- src/sat/sat_local_search.cpp | 67 +++++++++++++++++--------- src/sat/sat_local_search.h | 11 +++-- src/sat/tactic/goal2sat.cpp | 12 +++-- src/shell/opt_frontend.cpp | 28 +++++------ src/tactic/arith/lia2card_tactic.cpp | 2 + src/tactic/generic_model_converter.cpp | 15 ------ 8 files changed, 78 insertions(+), 63 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5c0c09125..f2e98fa59 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -721,8 +721,8 @@ namespace opt { } goal_ref g(alloc(goal, m, true, false)); - for (unsigned i = 0; i < fmls.size(); ++i) { - g->assert_expr(fmls[i].get()); + for (expr* fml : fmls) { + g->assert_expr(fml); } tactic_ref tac0 = and_then(mk_simplify_tactic(m, m_params), diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 63e58d4b6..9e17b0594 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -453,7 +453,6 @@ namespace sat { bool validate_resolvent(); void display(std::ostream& out, ineq& p, bool values = false) const; - void display(std::ostream& out, constraint const& c, bool values) const; void display(std::ostream& out, card const& c, bool values) const; void display(std::ostream& out, pb const& p, bool values) const; void display(std::ostream& out, xr const& c, bool values) const; @@ -500,6 +499,7 @@ namespace sat { virtual bool is_blocked(literal l, ext_constraint_idx idx); ptr_vector const & constraints() const { return m_constraints; } + void display(std::ostream& out, constraint const& c, bool values) const; virtual bool validate(); diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index da9617151..5e5f49eb4 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -104,7 +104,7 @@ namespace sat { coeff_vector& falsep = m_vars[v].m_watch[!is_true]; for (unsigned i = 0; i < falsep.size(); ++i) { constraint& c = m_constraints[falsep[i].m_constraint_id]; - SASSERT(falsep[i].m_coeff == 1); + //SASSERT(falsep[i].m_coeff == 1); // will --slack if (c.m_slack <= 0) { dec_slack_score(v); @@ -113,7 +113,7 @@ namespace sat { } } for (unsigned i = 0; i < truep.size(); ++i) { - SASSERT(truep[i].m_coeff == 1); + //SASSERT(truep[i].m_coeff == 1); constraint& c = m_constraints[truep[i].m_constraint_id]; // will --true_terms_count[c] // will ++slack @@ -139,7 +139,8 @@ namespace sat { void local_search::reinit() { - if (!m_is_pb) { + IF_VERBOSE(10, verbose_stream() << "(sat-local-search reinit)\n";); + if (true || !m_is_pb) { // // the following methods does NOT converge for pseudo-boolean // can try other way to define "worse" and "better" @@ -156,8 +157,7 @@ namespace sat { } } - for (unsigned i = 0; i < m_constraints.size(); ++i) { - constraint& c = m_constraints[i]; + for (constraint & c : m_constraints) { c.m_slack = c.m_k; } @@ -216,31 +216,43 @@ namespace sat { } void local_search::verify_solution() const { - for (unsigned i = 0; i < m_constraints.size(); ++i) { - verify_constraint(m_constraints[i]); - } + for (constraint const& c : m_constraints) + verify_constraint(c); } - void local_search::verify_unsat_stack() const { - for (unsigned i = 0; i < m_unsat_stack.size(); ++i) { - constraint const& c = m_constraints[m_unsat_stack[i]]; + void local_search::verify_unsat_stack() const { + for (unsigned i : m_unsat_stack) { + constraint const& c = m_constraints[i]; SASSERT(c.m_k < constraint_value(c)); } } + unsigned local_search::constraint_coeff(constraint const& c, literal l) const { + for (auto const& pb : m_vars[l.var()].m_watch[is_pos(l)]) { + if (pb.m_constraint_id == c.m_id) return pb.m_coeff; + } + UNREACHABLE(); + return 0; + } + + unsigned local_search::constraint_value(constraint const& c) const { unsigned value = 0; for (unsigned i = 0; i < c.size(); ++i) { - value += is_true(c[i]) ? 1 : 0; + literal t = c[i]; + if (is_true(t)) { + value += constraint_coeff(c, t); + } } return value; } void local_search::verify_constraint(constraint const& c) const { unsigned value = constraint_value(c); + IF_VERBOSE(11, display(verbose_stream() << "verify ", c);); + TRACE("sat", display(verbose_stream() << "verify ", c);); if (c.m_k < value) { - IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c); - verbose_stream() << "value: " << value << "\n";); + IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";); UNREACHABLE(); } } @@ -252,7 +264,7 @@ namespace sat { // ~c <= k void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { unsigned id = m_constraints.size(); - m_constraints.push_back(constraint(k)); + m_constraints.push_back(constraint(k, id)); for (unsigned i = 0; i < sz; ++i) { m_vars.reserve(c[i].var() + 1); literal t(~c[i]); @@ -264,14 +276,15 @@ namespace sat { } } + // c * coeffs <= k void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { unsigned id = m_constraints.size(); - m_constraints.push_back(constraint(k)); + m_constraints.push_back(constraint(k, id)); for (unsigned i = 0; i < sz; ++i) { m_vars.reserve(c[i].var() + 1); - literal t(~c[i]); + literal t(c[i]); m_vars[t.var()].m_watch[is_pos(t)].push_back(pbcoeff(id, coeffs[i])); - m_constraints.back().push(t); // add coefficient to constraint? + m_constraints.back().push(t); } if (sz == 1 && k == 0) { m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100; @@ -359,7 +372,7 @@ namespace sat { lits.reset(); coeffs.reset(); - for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]), coeffs.push_back(1); + for (literal l : c) lits.push_back(~l), coeffs.push_back(1); lits.push_back(c.lit()); coeffs.push_back(k); add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n); } @@ -889,21 +902,27 @@ namespace sat { } } - void local_search::display(std::ostream& out) const { + std::ostream& local_search::display(std::ostream& out) const { for (constraint const& c : m_constraints) { display(out, c); } for (bool_var v = 0; v < num_vars(); ++v) { display(out, v, m_vars[v]); } + return out; } - void local_search::display(std::ostream& out, constraint const& c) const { - out << c.m_literals << " <= " << c.m_k << " lhs value: " << constraint_value(c) << "\n"; + std::ostream& local_search::display(std::ostream& out, constraint const& c) const { + for (literal l : c) { + unsigned coeff = constraint_coeff(c, l); + if (coeff > 1) out << coeff << " * "; + out << l << " "; + } + return out << " <= " << c.m_k << " lhs value: " << constraint_value(c) << "\n"; } - void local_search::display(std::ostream& out, unsigned v, var_info const& vi) const { - out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n"; + std::ostream& local_search::display(std::ostream& out, unsigned v, var_info const& vi) const { + return out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n"; } bool local_search::check_goodvar() { diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 735ff9c65..b0483c5b9 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -99,11 +99,12 @@ namespace sat { }; struct constraint { + unsigned m_id; unsigned m_k; int m_slack; unsigned m_size; literal_vector m_literals; - constraint(unsigned k) : m_k(k), m_slack(0), m_size(0) {} + constraint(unsigned k, unsigned id) : m_id(id), m_k(k), m_slack(0), m_size(0) {} void push(literal l) { m_literals.push_back(l); ++m_size; } unsigned size() const { return m_size; } literal const& operator[](unsigned idx) const { return m_literals[idx]; } @@ -232,6 +233,8 @@ namespace sat { unsigned constraint_value(constraint const& c) const; + unsigned constraint_coeff(constraint const& c, literal l) const; + void print_info(std::ostream& out); void extract_model(); @@ -240,11 +243,11 @@ namespace sat { void add_clause(unsigned sz, literal const* c); - void display(std::ostream& out) const; + std::ostream& display(std::ostream& out) const; - void display(std::ostream& out, constraint const& c) const; + std::ostream& display(std::ostream& out, constraint const& c) const; - void display(std::ostream& out, unsigned v, var_info const& vi) const; + std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const; public: diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index ac97eb3c3..d6d6c0892 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -517,7 +517,10 @@ struct goal2sat::imp { mk_clause(~l1, ~l2, l); m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); m_result_stack.push_back(sign ? ~l : l); - if (root) mk_clause(~l); + if (root) { + m_result_stack.reset(); + mk_clause(~l); + } } } @@ -586,7 +589,10 @@ struct goal2sat::imp { mk_clause(~l1, ~l2, l); m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); m_result_stack.push_back(sign ? ~l : l); - if (root) mk_clause(~l); + if (root) { + mk_clause(~l); + m_result_stack.reset(); + } } } @@ -808,7 +814,7 @@ struct goal2sat::imp { } f = m.mk_or(fmls.size(), fmls.c_ptr()); } - TRACE("goal2sat", tout << mk_pp(f, m) << "\n";); + TRACE("goal2sat", tout << f << "\n";); process(f); skip_dep: ; diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 48efd1148..7dcb761db 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation #include "opt/opt_context.h" #include "ast/ast_util.h" #include "ast/arith_decl_plugin.h" +#include "ast/ast_pp.h" #include "util/gparams.h" #include "util/timeout.h" #include "ast/reg_decl_plugins.h" @@ -99,21 +100,20 @@ static unsigned parse_opt(std::istream& in, opt_format f) { case l_false: std::cout << "unsat\n"; break; case l_undef: std::cout << "unknown\n"; break; } - DEBUG_CODE( - if (false && r == l_true) { - model_ref mdl; - opt.get_model(mdl); - expr_ref_vector hard(m); - opt.get_hard_constraints(hard); - for (unsigned i = 0; i < hard.size(); ++i) { - std::cout << "validate: " << i << "\n"; - expr_ref tmp(m); - VERIFY(mdl->eval(hard[i].get(), tmp)); - if (!m.is_true(tmp)) { - std::cout << tmp << "\n"; - } + + if (r != l_false && gparams::get().get_bool("model_validate", false)) { + model_ref mdl; + opt.get_model(mdl); + expr_ref_vector hard(m); + opt.get_hard_constraints(hard); + for (expr* h : hard) { + expr_ref tmp(m); + VERIFY(mdl->eval(h, tmp)); + if (!m.is_true(tmp)) { + std::cout << mk_pp(h, m) << " " << tmp << "\n"; } - }); + } + } } catch (z3_exception & ex) { std::cerr << ex.msg() << "\n"; diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index bc7e3a4ee..e598b876d 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -213,7 +213,9 @@ public: new_pr = m.mk_rewrite(g->form(i), new_curr); new_pr = m.mk_modus_ponens(g->pr(i), new_pr); } + // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";); g->update(i, new_curr, new_pr, g->dep(i)); + } for (expr* a : axioms) { g->assert_expr(a); diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 2e800da48..485682858 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -53,21 +53,6 @@ void generic_model_converter::operator()(model_ref & md) { break; case instruction::ADD: ev(e.m_def, val); - if (e.m_f->get_name() == symbol("FOX-PIT-17")) { - IF_VERBOSE(0, verbose_stream() << e.m_f->get_name() << " " << e.m_def << " -> " << val << "\n";); - ptr_vector ts; - ts.push_back(e.m_def); - while (!ts.empty()) { - app* t = to_app(ts.back()); - ts.pop_back(); - if (t->get_num_args() > 0) { - ts.append(t->get_num_args(), t->get_args()); - } - expr_ref tmp(m); - ev(t, tmp); - IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " -> " << tmp << "\n";); - } - } TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); arity = e.m_f->get_arity(); reset_ev = false;