From caa15ea04d555dd494cfe38beb960d6c61716112 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Feb 2019 18:17:07 +0100 Subject: [PATCH] enable cardinality constraints in nla2bv Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 47 +++++++++++++-------------- src/sat/sat_solver.h | 1 + src/tactic/arith/nla2bv_tactic.cpp | 37 ++++++++++++++------- src/tactic/smtlogics/qfnia_tactic.cpp | 18 ++++++---- 4 files changed, 60 insertions(+), 43 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 779cb7aad..2df184c88 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1779,41 +1779,30 @@ namespace sat { } #endif - IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";); - if (!check_clauses(m_model)) { - throw solver_exception("check model failed"); + if (m_clone) { + IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";); + if (!check_clauses(m_model)) { + throw solver_exception("check model failed"); + } } - if (m_config.m_drat) m_drat.check_model(m_model); + if (m_config.m_drat) { + m_drat.check_model(m_model); + } - // m_mc.set_solver(nullptr); m_mc(m_model); - if (!gparams::get_ref().get_bool("model_validate", false)) { - return; - } - if (!check_clauses(m_model)) { + if (m_clone && !check_clauses(m_model)) { IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream())); - //IF_VERBOSE(0, display_units(verbose_stream())); - //IF_VERBOSE(0, display(verbose_stream())); - IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); - + IF_VERBOSE(10, display_model(verbose_stream())); throw solver_exception("check model failed"); } - TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); - - if (m_clone) { - IF_VERBOSE(1, verbose_stream() << "\"checking model (on original set of clauses)\"\n";); - if (!m_clone->check_model(m_model)) { - //IF_VERBOSE(0, display(verbose_stream())); - //IF_VERBOSE(0, display_watches(verbose_stream())); - IF_VERBOSE(1, m_mc.display(verbose_stream())); - IF_VERBOSE(1, display_units(verbose_stream())); - //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); - throw solver_exception("check model failed (for cloned solver)"); - } + if (m_clone && !m_clone->check_model(m_model)) { + IF_VERBOSE(1, m_mc.display(verbose_stream())); + IF_VERBOSE(1, display_units(verbose_stream())); + throw solver_exception("check model failed (for cloned solver)"); } } @@ -3546,6 +3535,14 @@ namespace sat { return true; } + std::ostream& solver::display_model(std::ostream& out) const { + unsigned num = num_vars(); + for (bool_var v = 0; v < num; v++) { + out << v << ": " << m_model[v] << "\n"; + } + return out; +} + void solver::display_binary(std::ostream & out) const { unsigned sz = m_watches.size(); for (unsigned l_idx = 0; l_idx < sz; l_idx++) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 89b161c9f..53c3062a8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -668,6 +668,7 @@ namespace sat { void display_watches(std::ostream & out) const; void display_watches(std::ostream & out, literal lit) const; void display_dimacs(std::ostream & out) const override; + std::ostream& display_model(std::ostream& out) const; void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_assignment(std::ostream & out) const; std::ostream& display_justification(std::ostream & out, justification const& j) const; diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 06150e18b..0a58740d1 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/tactical.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "ast/pb_decl_plugin.h" #include "ast/for_each_expr.h" #include "ast/rewriter/expr_replacer.h" #include "util/optional.h" @@ -85,13 +86,18 @@ class nla2bv_tactic : public tactic { TRACE("nla2bv", g.display(tout); tout << "Muls: " << count_mul(g) << "\n"; ); + tactic_report report("nla->bv", g); m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); m_bounds(g); collect_power2(g); - if(!collect_vars(g)) { + switch (collect_vars(g)) { + case has_num: + break; + case not_supported: throw tactic_exception("goal is not in the fragment supported by nla2bv"); + case is_bool: + return; } - tactic_report report("nla->bv", g); substitute_vars(g); TRACE("nla2bv", g.display(tout << "substitute vars\n");); reduce_bv2int(g); @@ -308,27 +314,30 @@ class nla2bv_tactic : public tactic { class get_uninterp_proc { imp& m_imp; + arith_util& a; + ast_manager& m; + pb_util pb; ptr_vector m_vars; bool m_in_supported_fragment; public: - get_uninterp_proc(imp& s): m_imp(s), m_in_supported_fragment(true) {} + get_uninterp_proc(imp& s): m_imp(s), a(s.m_arith), m(a.get_manager()), pb(m), m_in_supported_fragment(true) {} ptr_vector const& vars() { return m_vars; } void operator()(var * n) { m_in_supported_fragment = false; } void operator()(app* n) { - arith_util& a = m_imp.m_arith; - ast_manager& m = a.get_manager(); - if (a.is_int(n) && - is_uninterp_const(n)) { + if (a.is_int(n) && is_uninterp_const(n)) { + TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_vars.push_back(n); } - else if (a.is_real(n) && - is_uninterp_const(n)) { + else if (a.is_real(n) && is_uninterp_const(n)) { m_vars.push_back(n); } else if (m.is_bool(n) && is_uninterp_const(n)) { + } + else if (m.is_bool(n) && n->get_decl()->get_family_id() == pb.get_family_id()) { + } else if (!(a.is_mul(n) || a.is_add(n) || @@ -342,7 +351,7 @@ class nla2bv_tactic : public tactic { m_imp.m_bv2real.is_pos_le(n) || m_imp.m_bv2real.is_pos_lt(n) || n->get_family_id() == a.get_manager().get_basic_family_id())) { - TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, a.get_manager()) << "\n";); + TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_in_supported_fragment = false; } m_imp.update_num_bits(n); @@ -353,13 +362,17 @@ class nla2bv_tactic : public tactic { bool is_supported() const { return m_in_supported_fragment; } }; - bool collect_vars(goal const & g) { + enum collect_t { has_num, not_supported, is_bool }; + + collect_t collect_vars(goal const & g) { get_uninterp_proc fe_var(*this); for_each_expr_at(fe_var, g); for (unsigned i = 0; i < fe_var.vars().size(); ++i) { add_var(fe_var.vars()[i]); } - return fe_var.is_supported() && !fe_var.vars().empty(); + if (!fe_var.is_supported()) return not_supported; + if (!fe_var.vars().empty()) return is_bool; + return has_num; } class count_mul_proc { diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index d28034a1d..528a6c048 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include "sat/tactic/sat_tactic.h" #include "tactic/arith/nla2bv_tactic.h" #include "tactic/arith/lia2card_tactic.h" +#include "tactic/arith/card2bv_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" #include "tactic/core/cofactor_term_ite_tactic.h" #include "nlsat/tactic/qfnra_nlsat_tactic.h" @@ -73,7 +74,8 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p), mk_elim_uncnstr_tactic(m), - mk_lia2card_tactic(m), + mk_lia2card_tactic(m), + mk_card2bv_tactic(m, p_ref), skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p))); } @@ -105,7 +107,9 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { params_ref simp_p = p; simp_p.set_bool("som", true); // expand into sums of monomials - return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic(m)); + return and_then( + using_params(mk_simplify_tactic(m), simp_p), + mk_smt_tactic(m)); } tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { @@ -113,9 +117,11 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_qfnia_premable(m, p), - or_else(mk_qfnia_sat_solver(m, p), - try_for(mk_qfnia_smt_solver(m, p), 2000), - mk_qfnia_nlsat_solver(m, p), - mk_qfnia_smt_solver(m, p)) + mk_qfnia_sat_solver(m, p) + +// or_else(mk_qfnia_sat_solver(m, p), +// try_for(mk_qfnia_smt_solver(m, p), 2000), +// mk_qfnia_nlsat_solver(m, p), +// mk_qfnia_smt_solver(m, p)) ); }