From 72d407a49f146d45ca591a0652cf60876f83240c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Oct 2020 15:48:40 -0700 Subject: [PATCH] mbp (#4741) * adding dt-solver Signed-off-by: Nikolaj Bjorner * dt Signed-off-by: Nikolaj Bjorner * move mbp to self-contained module Signed-off-by: Nikolaj Bjorner * files Signed-off-by: Nikolaj Bjorner * Create CMakeLists.txt * dt Signed-off-by: Nikolaj Bjorner * rename to bool_var2expr to indicate type class * mbp * na * add projection * na * na * na * na * na Signed-off-by: Nikolaj Bjorner * deps Signed-off-by: Nikolaj Bjorner * testing arith/q * na * newline for model printing Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 5 +- src/CMakeLists.txt | 2 +- src/ast/ast.cpp | 5 +- src/ast/ast.h | 3 +- src/ast/normal_forms/CMakeLists.txt | 1 + .../normal_forms}/elim_term_ite.cpp | 2 +- src/{smt => ast/normal_forms}/elim_term_ite.h | 0 src/ast/rewriter/expr_safe_replace.cpp | 2 +- src/ast/rewriter/pb2bv_rewriter.cpp | 53 +++- src/cmd_context/cmd_context.cpp | 2 +- src/math/lp/lp_api.h | 12 +- src/model/model_v2_pp.cpp | 6 +- src/qe/mbp/mbp_arith.cpp | 35 +-- src/qe/mbp/mbp_plugin.cpp | 255 +++++++++++++----- src/qe/mbp/mbp_plugin.h | 40 ++- src/qe/qe_mbp.cpp | 3 +- src/sat/sat_extension.h | 8 + src/sat/sat_solver.cpp | 1 - src/sat/sat_solver/inc_sat_solver.cpp | 30 ++- src/sat/smt/CMakeLists.txt | 2 +- src/sat/smt/arith_axioms.cpp | 48 ++-- src/sat/smt/arith_internalize.cpp | 90 +++++-- src/sat/smt/arith_solver.cpp | 115 ++++---- src/sat/smt/arith_solver.h | 30 ++- src/sat/smt/array_axioms.cpp | 20 +- src/sat/smt/atom2bool_var.cpp | 4 +- src/sat/smt/atom2bool_var.h | 2 +- src/sat/smt/bv_delay_internalize.cpp | 37 +-- src/sat/smt/bv_internalize.cpp | 6 +- src/sat/smt/dt_solver.cpp | 6 +- src/sat/smt/euf_internalize.cpp | 5 + src/sat/smt/euf_model.cpp | 15 +- src/sat/smt/euf_relevancy.cpp | 1 + src/sat/smt/euf_solver.h | 1 + src/sat/smt/fpa_solver.cpp | 26 +- src/sat/smt/q_mbi.cpp | 230 +++++++++------- src/sat/smt/q_mbi.h | 22 +- src/sat/smt/q_model_finder.cpp | 43 --- src/sat/smt/q_model_finder.h | 60 ----- src/sat/smt/q_model_fixer.cpp | 59 +++- src/sat/smt/q_model_fixer.h | 29 +- src/sat/smt/q_solver.cpp | 15 +- src/sat/smt/sat_th.cpp | 16 +- src/sat/smt/sat_th.h | 11 +- src/sat/tactic/goal2sat.cpp | 20 +- src/sat/tactic/goal2sat.h | 6 +- src/smt/CMakeLists.txt | 1 - src/smt/asserted_formulas.h | 2 +- src/smt/theory_lra.cpp | 130 ++++----- src/smt/theory_seq.cpp | 2 +- src/util/ref_vector.h | 2 + 51 files changed, 903 insertions(+), 618 deletions(-) rename src/{smt => ast/normal_forms}/elim_term_ite.cpp (95%) rename src/{smt => ast/normal_forms}/elim_term_ite.h (100%) delete mode 100644 src/sat/smt/q_model_finder.cpp delete mode 100644 src/sat/smt/q_model_finder.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 8a74e7310..5590e7237 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -48,8 +48,8 @@ def init_project_def(): add_lib('smt_params', ['ast', 'params'], 'smt/params') add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') - - add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'normal_forms', 'lp'], 'sat/smt') + add_lib('mbp', ['model', 'simplex'], 'qe/mbp') + add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp'], 'sat/smt') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') @@ -61,7 +61,6 @@ def init_project_def(): add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('mbp', ['model', 'simplex'], 'qe/mbp') add_lib('qe', ['smt', 'mbp', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') add_lib('fd_solver', ['core_tactics', 'arith_tactics', 'sat_solver', 'smt'], 'tactic/fd_solver') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bd3ee4cf0..a453fcb3b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -68,6 +68,7 @@ add_subdirectory(parsers/smt2) add_subdirectory(ast/pattern) add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(smt/params) +add_subdirectory(qe/mbp) add_subdirectory(sat/smt) add_subdirectory(sat/tactic) add_subdirectory(nlsat/tactic) @@ -79,7 +80,6 @@ add_subdirectory(smt) add_subdirectory(tactic/bv) add_subdirectory(smt/tactic) add_subdirectory(tactic/sls) -add_subdirectory(qe/mbp) add_subdirectory(qe) add_subdirectory(muz/base) add_subdirectory(muz/dataflow) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4f4d1be6e..5fba63442 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1794,6 +1794,7 @@ static void track_id(ast_manager& m, ast* n, unsigned id) { if (n->get_id() != id) return; ++s_count; TRACE("ast", tout << s_count << "\n";); +// SASSERT(s_count != 5); } #endif @@ -1827,7 +1828,7 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); -// track_id(*this, n, 3); +// track_id(*this, n, 77); // TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); @@ -1912,10 +1913,10 @@ ast * ast_manager::register_node_core(ast * n) { default: break; } - return n; } + void ast_manager::delete_node(ast * n) { TRACE("delete_node_bug", tout << mk_ll_pp(n, *this) << "\n";); diff --git a/src/ast/ast.h b/src/ast/ast.h index 9baf7660f..8ca59ffb3 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1680,9 +1680,8 @@ public: void debug_ref_count() { m_debug_ref_count = true; } void inc_ref(ast* n) { - if (n) { + if (n) n->inc_ref(); - } } void dec_ref(ast* n) { diff --git a/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt index 69288d92b..9b927ef16 100644 --- a/src/ast/normal_forms/CMakeLists.txt +++ b/src/ast/normal_forms/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(normal_forms SOURCES defined_names.cpp + elim_term_ite.cpp name_exprs.cpp nnf.cpp pull_quant.cpp diff --git a/src/smt/elim_term_ite.cpp b/src/ast/normal_forms/elim_term_ite.cpp similarity index 95% rename from src/smt/elim_term_ite.cpp rename to src/ast/normal_forms/elim_term_ite.cpp index e8b70fc59..3376e9dda 100644 --- a/src/smt/elim_term_ite.cpp +++ b/src/ast/normal_forms/elim_term_ite.cpp @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#include "smt/elim_term_ite.h" +#include "ast/normal_forms/elim_term_ite.h" #include "ast/ast_smt2_pp.h" br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) { diff --git a/src/smt/elim_term_ite.h b/src/ast/normal_forms/elim_term_ite.h similarity index 100% rename from src/smt/elim_term_ite.h rename to src/ast/normal_forms/elim_term_ite.h diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index c2efb520d..1adca1648 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -33,7 +33,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) { void expr_safe_replace::operator()(expr_ref_vector& es) { expr_ref val(m); for (unsigned i = 0; i < es.size(); ++i) { - (*this)(es[i].get(), val); + (*this)(es.get(i), val); es[i] = val; } } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 9571b9743..a7c273bba 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -17,16 +17,19 @@ Notes: --*/ -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" #include "util/statistics.h" -#include "ast/rewriter/pb2bv_rewriter.h" -#include "util/sorting_network.h" -#include "ast/ast_util.h" -#include "ast/ast_pp.h" #include "util/lbool.h" #include "util/uint_set.h" #include "util/gparams.h" +#include "util/debug.h" + +#include "ast/rewriter/rewriter.h" +#include "ast/rewriter/rewriter_def.h" +#include "ast/rewriter/pb2bv_rewriter.h" +#include "ast/ast_util.h" +#include "ast/ast_pp.h" +#include "util/sorting_network.h" + static const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17}; @@ -90,7 +93,7 @@ struct pb2bv_rewriter::imp { void sort_args() { vector cas; for (unsigned i = 0; i < m_args.size(); ++i) { - cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m))); + cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m))); } std::sort(cas.begin(), cas.end(), compare_coeffs()); m_coeffs.reset(); @@ -101,6 +104,38 @@ struct pb2bv_rewriter::imp { } } + template + void gcd_reduce(vector& coeffs, rational & k) { + rational g(0); + for (rational const& c : coeffs) { + if (!c.is_int()) + return; + g = gcd(g, c); + if (g.is_one()) + return; + } + switch (is_le) { + case l_undef: + if (!k.is_int()) + return; + g = gcd(k, g); + if (g.is_one() || g.is_zero()) + return; + k /= g; + break; + case l_true: + k /= g; + k = floor(k); + break; + case l_false: + k /= g; + k = ceil(k); + break; + } + for (rational& c : coeffs) + c /= g; + } + // // create a circuit of size sz*log(k) // by forming a binary tree adding pairs of values that are assumed <= k, @@ -114,8 +149,10 @@ struct pb2bv_rewriter::imp { // is_le = l_false - >= // template - expr_ref mk_le_ge(rational const & k) { + expr_ref mk_le_ge(rational const & _k) { + rational k(_k); //sort_args(); + gcd_reduce(m_coeffs, k); unsigned sz = m_args.size(); expr * const* args = m_args.c_ptr(); TRACE("pb", diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 49b577bf9..e41b7310c 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1660,7 +1660,7 @@ void cmd_context::display_model(model_ref& mdl) { model_v2_pp(buffer, *mdl, false); regular_stream() << '"' << escaped(buffer.str(), true) << '"' << std::endl; } else { - regular_stream() << "(model " << std::endl; + regular_stream() << "(" << std::endl; model_smt2_pp(regular_stream(), *this, *mdl, 2); regular_stream() << ")" << std::endl; } diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index dfccd855b..f8c655b08 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -27,9 +27,10 @@ namespace lp_api { return out; } + template class bound { - bool_var m_bv; - theory_var m_var; + Literal m_bv; + theory_var m_var; lp::lpvar m_vi; bool m_is_int; rational m_value; @@ -37,7 +38,7 @@ namespace lp_api { lp::constraint_index m_constraints[2]; public: - bound(bool_var bv, theory_var v, lp::lpvar vi, bool is_int, rational const& val, bound_kind k, lp::constraint_index ct, lp::constraint_index cf) : + bound(Literal bv, theory_var v, lp::lpvar vi, bool is_int, rational const& val, bound_kind k, lp::constraint_index ct, lp::constraint_index cf) : m_bv(bv), m_var(v), m_vi(vi), @@ -54,7 +55,7 @@ namespace lp_api { lp::tv tv() const { return lp::tv::raw(m_vi); } - bool_var get_bv() const { return m_bv; } + Literal get_lit() const { return m_bv; } bound_kind get_bound_kind() const { return m_bound_kind; } @@ -82,7 +83,8 @@ namespace lp_api { } }; - inline std::ostream& operator<<(std::ostream& out, bound const& b) { + template + inline std::ostream& operator<<(std::ostream& out, bound const& b) { return b.display(out); } diff --git a/src/model/model_v2_pp.cpp b/src/model/model_v2_pp.cpp index dae9b2104..556ecb35d 100644 --- a/src/model/model_v2_pp.cpp +++ b/src/model/model_v2_pp.cpp @@ -56,10 +56,8 @@ static void display_function(std::ostream & out, model_core const & md, func_dec static void display_functions(std::ostream & out, model_core const & md, bool partial) { unsigned sz = md.get_num_functions(); - for (unsigned i = 0; i < sz; i++) { - func_decl * f = md.get_function(i); - display_function(out, md, f, partial); - } + for (unsigned i = 0; i < sz; i++) + display_function(out, md, md.get_function(i), partial); } static void display_constants(std::ostream & out, model_core const & md) { diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 42b20cfe3..0cbae132c 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -168,28 +168,23 @@ namespace mbp { expr* t1, *t2, *t3; rational mul1; expr_ref val(m); - if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1)) { - linearize(mbo, eval, mul* mul1, t2, c, fmls, ts, tids); - } - else if (a.is_mul(t, t1, t2) && is_numeral(t2, mul1)) { - linearize(mbo, eval, mul* mul1, t1, c, fmls, ts, tids); - } + if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1)) + linearize(mbo, eval, mul* mul1, t2, c, fmls, ts, tids); + else if (a.is_mul(t, t1, t2) && is_numeral(t2, mul1)) + linearize(mbo, eval, mul* mul1, t1, c, fmls, ts, tids); + else if (a.is_uminus(t, t1)) + linearize(mbo, eval, -mul, t1, c, fmls, ts, tids); + else if (a.is_numeral(t, mul1)) + c += mul * mul1; else if (a.is_add(t)) { - app* ap = to_app(t); - for (expr* arg : *ap) { - linearize(mbo, eval, mul, arg, c, fmls, ts, tids); - } + for (expr* arg : *to_app(t)) + linearize(mbo, eval, mul, arg, c, fmls, ts, tids); } else if (a.is_sub(t, t1, t2)) { linearize(mbo, eval, mul, t1, c, fmls, ts, tids); linearize(mbo, eval, -mul, t2, c, fmls, ts, tids); - } - else if (a.is_uminus(t, t1)) { - linearize(mbo, eval, -mul, t1, c, fmls, ts, tids); - } - else if (a.is_numeral(t, mul1)) { - c += mul*mul1; - } + } + else if (m.is_ite(t, t1, t2, t3)) { val = eval(t1); SASSERT(m.is_true(val) || m.is_false(val)); @@ -269,9 +264,8 @@ namespace mbp { vector project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, bool compute_def) { bool has_arith = false; - for (expr* v : vars) { - has_arith |= is_arith(v); - } + for (expr* v : vars) + has_arith |= is_arith(v); if (!has_arith) return vector(); model_evaluator eval(model); @@ -517,7 +511,6 @@ namespace mbp { expr_ref val = eval(v); if (!a.is_numeral(val, r)) { TRACE("qe", tout << eval.get_model() << "\n";); - throw default_exception("mbp evaluation was only partial"); } id = mbo.add_var(r, a.is_int(v)); diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index ed4ab5252..be43f1f0c 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -3,19 +3,18 @@ Copyright (c) 2015 Microsoft Corporation Module Name: - qe_mbp.cpp + + mpb_plugin.cpp Abstract: - Model-based projection utilities + Model-based projection plugin utilities + Author: Nikolaj Bjorner (nbjorner) 2015-5-29 -Revision History: - - --*/ #include "ast/rewriter/expr_safe_replace.h" @@ -58,9 +57,9 @@ namespace mbp { expr_ref_vector vals(m); obj_map val2expr; app* alit = to_app(t); - if (alit->get_num_args() == 2) { - return expr_ref(m.mk_eq(alit->get_arg(0), alit->get_arg(1)), m); - } + SASSERT(alit->get_num_args() > 1); + if (alit->get_num_args() == 2) + return expr_ref(m.mk_eq(alit->get_arg(0), alit->get_arg(1)), m); for (expr* e1 : *alit) { expr* e2; val = model(e1); @@ -97,6 +96,7 @@ namespace mbp { } void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) { + m_cache.reset(); m_bool_visited.reset(); expr_ref val(m); model_evaluator eval(model); @@ -106,7 +106,7 @@ namespace mbp { expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3; SASSERT(m.is_bool(fml)); if (m.is_not(fml, nfml) && m.is_distinct(nfml)) - fmls[i--] = mbp::project_plugin::pick_equality(m, model, nfml); + fmls[i--] = pick_equality(m, model, nfml); else if (m.is_or(fml)) { for (expr* arg : *to_app(fml)) { val = eval(arg); @@ -119,7 +119,7 @@ namespace mbp { } else if (m.is_and(fml)) { fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { val = eval(f1); @@ -150,11 +150,11 @@ namespace mbp { push_back(fmls, mk_not(m, f1)); push_back(fmls, f3); } - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) { push_back(fmls, nfml); - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if (m.is_not(fml, nfml) && m.is_and(nfml)) { for (expr* arg : *to_app(nfml)) { @@ -168,24 +168,22 @@ namespace mbp { else if (m.is_not(fml, nfml) && m.is_or(nfml)) { for (expr* arg : *to_app(nfml)) push_back(fmls, mk_not(m, arg)); - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { val = eval(f1); - if (m.is_true(val)) { - f2 = mk_not(m, f2); - } - else { - f1 = mk_not(m, f1); - } + if (m.is_true(val)) + f2 = mk_not(m, f2); + else + f1 = mk_not(m, f1); push_back(fmls, f1); push_back(fmls, f2); - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) { push_back(fmls, f1); push_back(fmls, mk_not(m, f2)); - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { val = eval(f1); @@ -197,66 +195,187 @@ namespace mbp { push_back(fmls, mk_not(m, f1)); push_back(fmls, mk_not(m, f3)); } - mbp::project_plugin::erase(fmls, i); + erase(fmls, i); } - else if (m.is_not(fml, nfml)) { - if (extract_bools(eval, fmls, nfml)) { - mbp::project_plugin::erase(fmls, i); - } - } - else if (extract_bools(eval, fmls, fml)) - mbp::project_plugin::erase(fmls, i); + else if (m.is_not(fml, nfml)) + extract_bools(eval, fmls, i, nfml, false); + else + extract_bools(eval, fmls, i, fml, true); } TRACE("qe", tout << fmls << "\n";); } - bool project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) { + void project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned idx, expr* fml, bool is_true) { TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";); - ptr_vector todo; - expr_safe_replace sub(m); - m_visited.reset(); - bool found_bool = false; - if (is_app(fml)) { - todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); + if (!is_app(fml)) + return; + m_to_visit.reset(); + m_to_visit.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); + while (!m_to_visit.empty()) { + if (!m.inc()) + return; + expr* e = m_to_visit.back(); + if (m_cache.get(e->get_id(), nullptr)) { + m_to_visit.pop_back(); + } + else if (!is_app(e)) { + m_cache.setx(e->get_id(), e); + m_to_visit.pop_back(); + } + else if (visit_ite(eval, e, fmls)) + continue; + else if (visit_bool(eval, e, fmls)) + continue; + else + visit_app(e); } - while (!todo.empty() && m.inc()) { - expr* e = todo.back(); - todo.pop_back(); - if (m_visited.is_marked(e)) { + + SASSERT(m_to_visit.empty()); + m_to_visit.push_back(fml); + visit_app(fml); + SASSERT(m_to_visit.empty()); + expr* new_fml = m_cache.get(fml->get_id(), nullptr); + SASSERT(new_fml); + if (new_fml != fml) + fmls[idx] = is_true ? new_fml : mk_not(m, new_fml); + } + + bool project_plugin::is_true(model_evaluator& eval, expr* e) { + expr_ref val = eval(e); + bool tt = m.is_true(val); + if (!tt && !m.is_false(val) && contains_uninterpreted(val)) + throw default_exception("could not evaluate Boolean in model"); + SASSERT(tt || m.is_false(val)); + return tt; + } + + bool project_plugin::visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls) { + expr* c = nullptr, * th = nullptr, * el = nullptr; + if (m.is_ite(e, c, th, el)) { + bool tt = is_true(eval, c); + if (!m_bool_visited.is_marked(c)) + fmls.push_back(tt ? c : mk_not(m, c)); + m_bool_visited.mark(c); + expr* s = tt ? th : el; + expr* t = m_cache.get(s->get_id(), nullptr); + if (t) { + m_to_visit.pop_back(); + m_cache.setx(e->get_id(), t); + } + else + m_to_visit.push_back(s); + return true; + } + else + return false; + } + + bool project_plugin::visit_bool(model_evaluator& eval, expr* e, expr_ref_vector& fmls) { + if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) { + bool tt = is_true(eval, e); + if (!m_bool_visited.is_marked(e)) + fmls.push_back(tt ? e : mk_not(m, e)); + m_bool_visited.mark(e); + m_cache.setx(e->get_id(), m.mk_bool_val(tt)); + m_to_visit.pop_back(); + return true; + } + else + return false; + } + + void project_plugin::visit_app(expr* e) { + unsigned sz = m_to_visit.size(); + m_args.reset(); + bool diff = false; + for (expr* arg : *to_app(e)) { + expr* new_arg = m_cache.get(arg->get_id(), nullptr); + diff |= new_arg != arg; + if (new_arg == nullptr) + m_to_visit.push_back(arg); + else + m_args.push_back(new_arg); + } + if (sz == m_to_visit.size()) { + m_cache.setx(e->get_id(), diff ? m.mk_app(to_app(e)->get_decl(), m_args) : e); + m_to_visit.pop_back(); + } + } + + void project_plugin::mark_non_ground(expr* e) { + m_to_visit.push_back(e); + while (!m_to_visit.empty()) { + expr* e = m_to_visit.back(); + if (!is_app(e)) { + m_visited.mark(e); + m_to_visit.pop_back(); continue; } - m_visited.mark(e); - if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) { - expr_ref val = eval(e); - TRACE("qe", tout << "found: " << mk_pp(e, m) << " " << val << "\n";); - if (!m.inc()) - continue; - if (!m.is_true(val) && !m.is_false(val) && contains_uninterpreted(val)) - throw default_exception("could not evaluate Boolean in model"); - SASSERT(m.is_true(val) || m.is_false(val)); + unsigned n = m_to_visit.size(); + for (expr* arg : *to_app(e)) { + if (!m_visited.is_marked(arg)) + m_to_visit.push_back(arg); + else if (m_non_ground.is_marked(arg)) + m_non_ground.mark(e); + } + if (m_to_visit.size() == n) { + m_visited.mark(e); + m_to_visit.pop_back(); + } + } + } - if (!m_bool_visited.is_marked(e)) - fmls.push_back(m.is_true(val) ? e : mk_not(m, e)); - sub.insert(e, val); - m_bool_visited.mark(e); - found_bool = true; - } - else if (is_app(e)) { - todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - else { - TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";); + void project_plugin::purify(euf_inverter& inv, model& mdl, app_ref_vector const& vars, expr_ref_vector& lits) { + TRACE("mbp", tout << lits << "\n" << mdl << "\n";); + extract_literals(mdl, vars, lits); + if (!m.inc()) + return; + model_evaluator eval(mdl); + eval.set_expand_array_equalities(true); + m_non_ground.reset(); + m_to_visit.reset(); + m_visited.reset(); + m_cache.reset(); + m_pure_eqs.reset(); + for (expr* v : vars) + m_non_ground.mark(v); + for (unsigned i = 0; m.inc() && i < lits.size(); ++i) + lits[i] = purify(inv, eval, lits.get(i), lits); + lits.append(m_pure_eqs); + TRACE("mbp", tout << lits << "\n";); + } + + expr* project_plugin::purify(euf_inverter& inv, model_evaluator& eval, expr* e, expr_ref_vector& lits) { + mark_non_ground(e); + m_to_visit.push_back(e); + while (!m_to_visit.empty()) { + expr* t = m_to_visit.back(); + if (m_cache.get(t->get_id(), nullptr)) + m_to_visit.pop_back(); + else if (!is_app(t) || !m_non_ground.is_marked(t)) { + m_cache.setx(t->get_id(), t); + m_to_visit.pop_back(); } + else + purify_app(inv, eval, to_app(t), lits); } - if (found_bool) { - expr_ref tmp(m); - sub(fml, tmp); - expr_ref val = eval(tmp); - if (!m.is_true(val) && !m.is_false(val)) - return false; - fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp)); + return m_cache.get(e->get_id()); + } + + void project_plugin::purify_app(euf_inverter& inv, model_evaluator& eval, app* t, expr_ref_vector& lits) { + if (is_uninterp(t) && t->get_num_args() > 0) { + expr_ref t_value = eval(t); + expr* s = inv.invert_app(t, t_value); + m_cache.setx(t->get_id(), s); + if (s != t) + m_pure_eqs.push_back(m.mk_eq(t, s)); + unsigned i = 0; + for (expr* arg : *t) + push_back(lits, inv.invert_arg(t, i++, eval(arg))); + m_to_visit.pop_back(); } - return found_bool; + else + visit_app(t); } } diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index efb8728f0..f339aa07a 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -35,18 +35,43 @@ namespace mbp { def(const expr_ref& v, expr_ref& t): var(v), term(t) {} }; - class project_plugin { - ast_manager& m; - expr_mark m_visited; - expr_mark m_bool_visited; + /*** + * An EUF inverter provides two services: + * 1. It inverts an uninterpreted function application f(s1,s2) with 'value' to a ground term evaluating to the same + * 2. It adds constraints for arguments to s_i with 'value' to be within the bounds of the model value. + */ + class euf_inverter { + public: + virtual expr* invert_app(app* t, expr* value) = 0; + virtual expr* invert_arg(app* t, unsigned i, expr* value) = 0; + }; + + class project_plugin { + ast_manager& m; + expr_mark m_visited; + ptr_vector m_to_visit; + expr_mark m_bool_visited; + expr_mark m_non_ground; + expr_ref_vector m_cache, m_args, m_pure_eqs; + + void extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned i, expr* fml, bool is_true); + void visit_app(expr* e); + bool visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls); + bool visit_bool(model_evaluator& eval, expr* e, expr_ref_vector& fmls); + bool is_true(model_evaluator& eval, expr* e); - bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml); // over-approximation bool contains_uninterpreted(expr* v) { return true; } void push_back(expr_ref_vector& lits, expr* lit); + + void mark_non_ground(expr* e); + + expr* purify(euf_inverter& inv, model_evaluator& eval, expr* e, expr_ref_vector& lits); + void purify_app(euf_inverter& inv, model_evaluator& eval, app* t, expr_ref_vector& lits); + public: - project_plugin(ast_manager& m) :m(m) {} + project_plugin(ast_manager& m) :m(m), m_cache(m), m_args(m), m_pure_eqs(m) {} virtual ~project_plugin() {} virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; } /** @@ -81,7 +106,8 @@ namespace mbp { /* * Purify literals into linear inequalities or constraints without arithmetic variables. */ - void purify(model& model, app_ref_vector const& vars, expr_ref_vector& fmls); + + void purify(euf_inverter& inv, model& model, app_ref_vector const& vars, expr_ref_vector& fmls); static expr_ref pick_equality(ast_manager& m, model& model, expr* t); static void erase(expr_ref_vector& lits, unsigned& i); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 1e1b60d56..a1436fd44 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -290,9 +290,8 @@ public: app_ref_vector new_vars(m); progress = false; for (mbp::project_plugin* p : m_plugins) { - if (p) { + if (p) (*p)(model, vars, fmls); - } } while (!vars.empty() && !fmls.empty() && m.limit().inc()) { var = vars.back(); diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 736024781..24e22d312 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -29,6 +29,14 @@ namespace sat { CR_DONE, CR_CONTINUE, CR_GIVEUP }; + inline std::ostream& operator<<(std::ostream& out, check_result const& r) { + switch (r) { + case check_result::CR_DONE: return out << "done"; + case check_result::CR_CONTINUE: return out << "continue"; + default: return out << "giveup"; + } + } + class literal_occs_fun { public: virtual double operator()(literal l) = 0; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 24e072b2b..791973661 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2338,7 +2338,6 @@ namespace sat { lbool solver::resolve_conflict_core() { - TRACE("sat", tout << "**************************\n";); m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 57e968b45..6d4579225 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -282,8 +282,6 @@ public: m_num_scopes -= n; // ? m_internalized_converted = false; m_has_uninterpreted.pop(n); - if (get_euf()) - get_euf()->user_pop(n); while (n > 0) { m_mcs.pop_back(); m_fmls_head = m_fmls_head_lim.back(); @@ -605,15 +603,21 @@ public: params_ref simp2_p = m_params; simp2_p.set_bool("flat", false); - m_preprocess = - and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_card2bv_tactic(m, m_params), // updates model converter - using_params(mk_simplify_tactic(m), simp1_p), - mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, m_bb_rewriter.get()), - using_params(mk_simplify_tactic(m), simp2_p) - ); + sat_params sp(m_params); + if (sp.euf()) + m_preprocess = + and_then(mk_simplify_tactic(m), + mk_propagate_values_tactic(m)); + else + m_preprocess = + and_then(mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + mk_card2bv_tactic(m, m_params), // updates model converter + using_params(mk_simplify_tactic(m), simp1_p), + mk_max_bv_sharing_tactic(m), + mk_bit_blaster_tactic(m, m_bb_rewriter.get()), + using_params(mk_simplify_tactic(m), simp2_p) + ); while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); } @@ -982,11 +986,11 @@ private: if (m_sat_mc) { (*m_sat_mc)(ll_m); } - app_ref_vector var2expr(m); + expr_ref_vector var2expr(m); m_map.mk_var_inv(var2expr); for (unsigned v = 0; v < var2expr.size(); ++v) { - app * n = var2expr.get(v); + expr * n = var2expr.get(v); if (!n || !is_uninterp_const(n)) { continue; } diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 197fe9aaf..6eb4f429d 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -30,7 +30,6 @@ z3_add_component(sat_smt euf_solver.cpp fpa_solver.cpp q_mbi.cpp - q_model_finder.cpp q_model_fixer.cpp q_solver.cpp sat_dual_solver.cpp @@ -41,6 +40,7 @@ z3_add_component(sat_smt sat ast euf + mbp smt_params ) diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 317f3c1a4..e8e609db9 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -42,8 +42,8 @@ namespace arith { expr_ref to_r(a.mk_to_real(n), m); expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m); expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); - literal llo = b_internalize(lo); - literal lhi = b_internalize(hi); + literal llo = mk_literal(lo); + literal lhi = mk_literal(hi); add_clause(llo); add_clause(~lhi); } @@ -160,19 +160,19 @@ namespace arith { add_clause(dgez, neg); } - void solver::mk_bound_axioms(lp_api::bound& b) { + void solver::mk_bound_axioms(api_bound& b) { theory_var v = b.get_var(); lp_api::bound_kind kind1 = b.get_bound_kind(); rational const& k1 = b.get_value(); lp_bounds& bounds = m_bounds[v]; - lp_api::bound* end = nullptr; - lp_api::bound* lo_inf = end, * lo_sup = end; - lp_api::bound* hi_inf = end, * hi_sup = end; + api_bound* end = nullptr; + api_bound* lo_inf = end, * lo_sup = end; + api_bound* hi_inf = end, * hi_sup = end; - for (lp_api::bound* other : bounds) { + for (api_bound* other : bounds) { if (other == &b) continue; - if (b.get_bv() == other->get_bv()) continue; + if (b.get_lit() == other->get_lit()) continue; lp_api::bound_kind kind2 = other->get_bound_kind(); rational const& k2 = other->get_value(); if (k1 == k2 && kind1 == kind2) { @@ -206,9 +206,9 @@ namespace arith { if (hi_sup != end) mk_bound_axiom(b, *hi_sup); } - void solver::mk_bound_axiom(lp_api::bound& b1, lp_api::bound& b2) { - literal l1(b1.get_bv(), false); - literal l2(b2.get_bv(), false); + void solver::mk_bound_axiom(api_bound& b1, api_bound& b2) { + literal l1(b1.get_lit()); + literal l2(b2.get_lit()); rational const& k1 = b1.get_value(); rational const& k2 = b2.get_value(); lp_api::bound_kind kind1 = b1.get_bound_kind(); @@ -259,7 +259,7 @@ namespace arith { } } - lp_api::bound* solver::mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) { + api_bound* solver::mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound) { scoped_internalize_state st(*this); st.vars().push_back(v); st.coeffs().push_back(rational::one()); @@ -279,10 +279,10 @@ namespace arith { else { cF = lp().mk_var_bound(vi, kF, bound); } - add_ineq_constraint(cT, literal(bv, false)); - add_ineq_constraint(cF, literal(bv, true)); + add_ineq_constraint(cT, lit); + add_ineq_constraint(cF, ~lit); - return alloc(lp_api::bound, bv, v, vi, v_is_int, bound, bk, cT, cF); + return alloc(api_bound, lit, v, vi, v_is_int, bound, bk, cT, cF); } lp::lconstraint_kind solver::bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true) { @@ -297,11 +297,25 @@ namespace arith { } void solver::mk_eq_axiom(theory_var v1, theory_var v2) { + if (is_bool(v1)) + return; expr* e1 = var2expr(v1); expr* e2 = var2expr(v2); - literal le = b_internalize(a.mk_le(e1, e2)); - literal ge = b_internalize(a.mk_le(e2, e1)); + literal le, ge; literal eq = eq_internalize(e1, e2); + if (a.is_numeral(e1)) + std::swap(e1, e2); + if (a.is_numeral(e2)) { + le = mk_literal(a.mk_le(e1, e2)); + ge = mk_literal(a.mk_ge(e1, e2)); + } + else { + expr_ref diff(a.mk_sub(e1, e2), m); + expr_ref zero(a.mk_numeral(rational(0), a.is_int(e1)), m); + rewrite(diff); + le = mk_literal(a.mk_le(diff, zero)); + ge = mk_literal(a.mk_ge(diff, zero)); + } add_clause(~eq, le); add_clause(~eq, ge); add_clause(~le, ~ge, eq); diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 52bcd5bd3..974bd03c9 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -31,7 +31,10 @@ namespace arith { void solver::internalize(expr* e, bool redundant) { flet _is_learned(m_is_redundant, redundant); - internalize_term(e); + if (m.is_bool(e)) + internalize_atom(e); + else + internalize_term(e); } lpvar solver::get_one(bool is_int) { @@ -284,30 +287,61 @@ namespace arith { bool solver::internalize_atom(expr* atom) { TRACE("arith", tout << mk_pp(atom, m) << "\n";); SASSERT(!ctx.get_enode(atom)); - expr* n1, * n2; + expr* n1, *n2; rational r; lp_api::bound_kind k; theory_var v = euf::null_theory_var; bool_var bv = ctx.get_si().add_bool_var(atom); m_bool_var2bound.erase(bv); - ctx.attach_lit(literal(bv, false), atom); + literal lit(bv, false); + ctx.attach_lit(lit, atom); - if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) { - v = internalize_def(to_app(n1)); + if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n2, r)) { + v = internalize_def(n1); k = lp_api::upper_t; } - else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) { - v = internalize_def(to_app(n1)); + else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n2, r)) { + v = internalize_def(n1); k = lp_api::lower_t; } - else if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) { - v = internalize_def(to_app(n2)); + else if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n1, r)) { + v = internalize_def(n2); k = lp_api::lower_t; } - else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) { - v = internalize_def(to_app(n2)); + else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n1, r)) { + v = internalize_def(n2); k = lp_api::upper_t; } + else if (a.is_le(atom, n1, n2)) { + expr_ref n3(a.mk_sub(n1, n2), m); + rewrite(n3); + v = internalize_def(n3); + k = lp_api::upper_t; + r = 0; + } + else if (a.is_ge(atom, n1, n2)) { + expr_ref n3(a.mk_sub(n1, n2), m); + rewrite(n3); + v = internalize_def(n3); + k = lp_api::lower_t; + r = 0; + } + else if (a.is_lt(atom, n1, n2)) { + expr_ref n3(a.mk_sub(n1, n2), m); + rewrite(n3); + v = internalize_def(n3); + k = lp_api::lower_t; + r = 0; + lit.neg(); + } + else if (a.is_gt(atom, n1, n2)) { + expr_ref n3(a.mk_sub(n1, n2), m); + rewrite(n3); + v = internalize_def(n3); + k = lp_api::upper_t; + r = 0; + lit.neg(); + } else if (a.is_is_int(atom)) { mk_is_int_axiom(atom); return true; @@ -317,13 +351,14 @@ namespace arith { found_unsupported(atom); return true; } - enode* n = ctx.get_enode(atom); - ctx.attach_th_var(n, this, v); - if (is_int(v) && !r.is_int()) { - r = (k == lp_api::upper_t) ? floor(r) : ceil(r); - } - lp_api::bound* b = mk_var_bound(bv, v, k, r); + enode* n = ctx.get_enode(atom); + theory_var w = mk_var(n); + ctx.attach_th_var(n, this, w); + ctx.get_egraph().set_merge_enabled(n, false); + if (is_int(v) && !r.is_int()) + r = (k == lp_api::upper_t) ? floor(r) : ceil(r); + api_bound* b = mk_var_bound(lit, v, k, r); m_bounds[v].push_back(b); updt_unassigned_bounds(v, +1); m_bounds_trail.push_back(v); @@ -366,6 +401,8 @@ namespace arith { } void solver::internalize_args(app* t, bool force) { + SASSERT(!m.is_bool(t)); + TRACE("arith", tout << mk_pp(t, m) << " " << force << " " << reflect(t) << "\n";); if (!force && !reflect(t)) return; for (expr* arg : *t) @@ -570,18 +607,17 @@ namespace arith { } /** - \brief We must redefine this method, because theory of arithmetic contains - underspecified operators such as division by 0. - (/ a b) is essentially an uninterpreted function when b = 0. - Thus, 'a' must be considered a shared var if it is the child of an underspecified operator. + \brief We must redefine this method, because theory of arithmetic contains + underspecified operators such as division by 0. + (/ a b) is essentially an uninterpreted function when b = 0. + Thus, 'a' must be considered a shared var if it is the child of an underspecified operator. - if merge(a / b, x + y) and a / b is root, then x + y become shared and all z + u in equivalence class of x + y. + if merge(a / b, x + y) and a / b is root, then x + y become shared and all z + u in equivalence class of x + y. - - TBD: when the set of underspecified subterms is small, compute the shared variables below it. - Recompute the set if there are merges that invalidate it. - Use the set to determine if a variable is shared. -*/ + TBD: when the set of underspecified subterms is small, compute the shared variables below it. + Recompute the set if there are merges that invalidate it. + Use the set to determine if a variable is shared. + */ bool solver::is_shared(theory_var v) const { if (m_underspecified.empty()) { return false; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 0105089c0..44023c085 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -55,9 +55,13 @@ namespace arith { m_lia = alloc(lp::int_solver, *m_solver.get()); } - solver::~solver() {} + solver::~solver() { + del_bounds(0); + std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc()); + } void solver::asserted(literal l) { + force_push(); m_asserted.push_back(l); } @@ -70,11 +74,11 @@ namespace arith { result->m_bounds.resize(m_bounds.size()); for (auto const& bounds : m_bounds) { for (auto* b : bounds) { - auto* b2 = result->mk_var_bound(b->get_bv(), v, b->get_bound_kind(), b->get_value()); + auto* b2 = result->mk_var_bound(b->get_lit(), v, b->get_bound_kind(), b->get_value()); result->m_bounds[v].push_back(b2); result->m_bounds_trail.push_back(v); result->updt_unassigned_bounds(v, +1); - result->m_bool_var2bound.insert(b->get_bv(), b2); + result->m_bool_var2bound.insert(b->get_lit().var(), b2); result->m_new_bounds.push_back(b2); } ++v; @@ -95,11 +99,10 @@ namespace arith { unsigned qhead = m_asserted_qhead; while (m_asserted_qhead < m_asserted.size() && !s().inconsistent() && m.inc()) { literal lit = m_asserted[m_asserted_qhead]; - lp_api::bound* b = nullptr; - TRACE("arith", tout << "propagate: " << lit << "\n";); + api_bound* b = nullptr; CTRACE("arith", !m_bool_var2bound.contains(lit.var()), tout << "not found " << lit << "\n";); if (m_bool_var2bound.find(lit.var(), b)) - assert_bound(!lit.sign(), *b); + assert_bound(lit.sign() == b->get_lit().sign(), *b); ++m_asserted_qhead; } if (s().inconsistent()) @@ -125,7 +128,7 @@ namespace arith { } void solver::propagate_basic_bounds(unsigned qhead) { - lp_api::bound* b = nullptr; + api_bound* b = nullptr; for (; qhead < m_asserted_qhead && !s().inconsistent(); ++qhead) { literal lit = m_asserted[qhead]; if (m_bool_var2bound.find(lit.var(), b)) @@ -140,7 +143,7 @@ namespace arith { // x <= hi -> x <= hi' // x <= hi -> ~(x >= hi') - void solver::propagate_bound(literal lit1, lp_api::bound& b) { + void solver::propagate_bound(literal lit1, api_bound& b) { if (bound_prop_mode::BP_NONE == propagation_mode()) return; @@ -158,8 +161,8 @@ namespace arith { TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";); if (find_glb) { rational glb; - lp_api::bound* lb = nullptr; - for (lp_api::bound* b2 : bounds) { + api_bound* lb = nullptr; + for (api_bound* b2 : bounds) { if (b2 == &b) continue; rational const& val2 = b2->get_value(); if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) { @@ -169,12 +172,14 @@ namespace arith { } if (!lb) return; bool sign = lb->get_bound_kind() != lp_api::lower_t; - lit2 = literal(lb->get_bv(), sign); + lit2 = lb->get_lit(); + if (sign) + lit2.neg(); } else { rational lub; - lp_api::bound* ub = nullptr; - for (lp_api::bound* b2 : bounds) { + api_bound* ub = nullptr; + for (api_bound* b2 : bounds) { if (b2 == &b) continue; rational const& val2 = b2->get_value(); if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) { @@ -184,7 +189,9 @@ namespace arith { } if (!ub) return; bool sign = ub->get_bound_kind() != lp_api::upper_t; - lit2 = literal(ub->get_bv(), sign); + lit2 = ub->get_lit(); + if (sign) + lit2.neg(); } updt_unassigned_bounds(v, -1); ++m_stats.m_bound_propagations2; @@ -233,8 +240,8 @@ namespace arith { lp_bounds const& bounds = m_bounds[v]; bool first = true; for (unsigned i = 0; i < bounds.size(); ++i) { - lp_api::bound* b = bounds[i]; - if (s().value(b->get_bv()) != l_undef) { + api_bound* b = bounds[i]; + if (s().value(b->get_lit()) != l_undef) { continue; } literal lit = is_bound_implied(be.kind(), be.m_bound, *b); @@ -252,7 +259,8 @@ namespace arith { } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1); - DEBUG_CODE(for (auto& lit : m_core) { VERIFY(s().value(lit) == l_true); }); + TRACE("arith", for (auto lit : m_core) tout << lit << ": " << s().value(lit) << "\n";); + DEBUG_CODE(for (auto lit : m_core) { VERIFY(s().value(lit) == l_true); }); ++m_stats.m_bound_propagations1; assign(lit, m_core, m_eqs, m_params); } @@ -261,30 +269,30 @@ namespace arith { refine_bound(v, be); } - literal solver::is_bound_implied(lp::lconstraint_kind k, rational const& value, lp_api::bound const& b) const { + literal solver::is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const { if ((k == lp::LE || k == lp::LT) && b.get_bound_kind() == lp_api::upper_t && value <= b.get_value()) { TRACE("arith", tout << "v <= value <= b.get_value() => v <= b.get_value() \n";); - return literal(b.get_bv(), false); + return b.get_lit(); } if ((k == lp::GE || k == lp::GT) && b.get_bound_kind() == lp_api::lower_t && b.get_value() <= value) { TRACE("arith", tout << "b.get_value() <= value <= v => b.get_value() <= v \n";); - return literal(b.get_bv(), false); + return b.get_lit(); } if (k == lp::LE && b.get_bound_kind() == lp_api::lower_t && value < b.get_value()) { TRACE("arith", tout << "v <= value < b.get_value() => v < b.get_value()\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::LT && b.get_bound_kind() == lp_api::lower_t && value <= b.get_value()) { TRACE("arith", tout << "v < value <= b.get_value() => v < b.get_value()\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::GE && b.get_bound_kind() == lp_api::upper_t && b.get_value() < value) { TRACE("arith", tout << "b.get_value() < value <= v => b.get_value() < v\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::GT && b.get_bound_kind() == lp_api::upper_t && b.get_value() <= value) { TRACE("arith", tout << "b.get_value() <= value < v => b.get_value() < v\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } return sat::null_literal; } @@ -324,8 +332,8 @@ namespace arith { if (m_bounds.size() <= static_cast(v) || m_unassigned_bounds[v] == 0) return false; - for (lp_api::bound* b : m_bounds[v]) - if (s().value(b->get_bv()) == l_undef && sat::null_literal != is_bound_implied(kind, bval, *b)) + for (api_bound* b : m_bounds[v]) + if (s().value(b->get_lit()) == l_undef && sat::null_literal != is_bound_implied(kind, bval, *b)) return true; return false; @@ -368,7 +376,7 @@ namespace arith { } - void solver::assert_bound(bool is_true, lp_api::bound& b) { + void solver::assert_bound(bool is_true, api_bound& b) { TRACE("arith", tout << b << "\n";); lp::constraint_index ci = b.get_constraint(is_true); lp().activate(ci); @@ -393,7 +401,7 @@ namespace arith { } - void solver::propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) { + void solver::propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value) { if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) { fixed_var_eh(b.get_var(), value); } @@ -421,7 +429,6 @@ namespace arith { return true; } else { - TRACE("arith", tout << "not a term " << tv.to_string() << "\n";); // m_solver already tracks bounds on proper variables, but not on terms. bool is_strict = false; rational b; @@ -468,9 +475,9 @@ namespace arith { iterator lo_inf = begin1, lo_sup = begin1; iterator hi_inf = begin2, hi_sup = begin2; bool flo_inf, fhi_inf, flo_sup, fhi_sup; - ptr_addr_hashtable visited; + ptr_addr_hashtable visited; for (unsigned i = 0; i < atoms.size(); ++i) { - lp_api::bound* a1 = atoms[i]; + api_bound* a1 = atoms[i]; iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf); iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf); iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup); @@ -497,14 +504,14 @@ namespace arith { iterator it, iterator end) { for (; it != end; ++it) { - lp_api::bound* a = *it; + api_bound* a = *it; if (a->get_bound_kind() == kind) return it; } return end; } lp_bounds::iterator solver::next_inf( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, @@ -513,7 +520,7 @@ namespace arith { iterator result = end; found_compatible = false; for (; it != end; ++it) { - lp_api::bound* a2 = *it; + api_bound* a2 = *it; if (a1 == a2) continue; if (a2->get_bound_kind() != kind) continue; rational const& k2(a2->get_value()); @@ -529,7 +536,7 @@ namespace arith { } lp_bounds::iterator solver::next_sup( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, @@ -537,7 +544,7 @@ namespace arith { rational const& k1(a1->get_value()); found_compatible = false; for (; it != end; ++it) { - lp_api::bound* a2 = *it; + api_bound* a2 = *it; if (a1 == a2) continue; if (a2->get_bound_kind() != kind) continue; rational const& k2(a2->get_value()); @@ -549,6 +556,10 @@ namespace arith { return end; } + void solver::init_model() { + init_variable_values(); + } + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { theory_var v = n->get_th_var(get_id()); expr* o = n->get_expr(); @@ -584,11 +595,12 @@ namespace arith { lp().push(); if (m_nla) m_nla->push(); - + th_euf_solver::push_core(); } void solver::pop_core(unsigned num_scopes) { TRACE("arith", tout << "pop " << num_scopes << "\n";); + th_euf_solver::pop_core(num_scopes); unsigned old_size = m_scopes.size() - num_scopes; del_bounds(m_scopes[old_size].m_bounds_lim); m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim); @@ -607,7 +619,7 @@ namespace arith { void solver::del_bounds(unsigned old_size) { for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) { unsigned v = m_bounds_trail[i]; - lp_api::bound* b = m_bounds[v].back(); + api_bound* b = m_bounds[v].back(); // del_use_lists(b); dealloc(b); m_bounds[v].pop_back(); @@ -690,7 +702,7 @@ namespace arith { } void solver::updt_unassigned_bounds(theory_var v, int inc) { - TRACE("arith", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";); + TRACE("arith_verbose", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";); ctx.push(vector_value_trail(m_unassigned_bounds, v)); m_unassigned_bounds[v] += inc; } @@ -728,7 +740,7 @@ namespace arith { } lbool solver::get_phase(bool_var v) { - lp_api::bound* b; + api_bound* b; if (!m_bool_var2bound.find(v, b)) { return l_undef; } @@ -763,6 +775,7 @@ namespace arith { } void solver::ensure_column(theory_var v) { + SASSERT(!is_bool(v)); if (!lp().external_is_used(v)) register_theory_var_in_lar_solver(v); } @@ -835,12 +848,15 @@ namespace arith { void solver::random_update() { if (m_nla) return; + TRACE("arith", tout << s().scope_lvl() << "\n"; tout.flush();); m_tmp_var_set.clear(); m_tmp_var_set.resize(get_num_vars()); m_model_eqs.reset(); svector vars; theory_var sz = static_cast(get_num_vars()); for (theory_var v = 0; v < sz; ++v) { + if (is_bool(v)) + continue; ensure_column(v); lp::column_index vj = lp().to_column_index(v); SASSERT(!vj.is_null()); @@ -870,6 +886,8 @@ namespace arith { int start = s().rand()(); for (theory_var i = 0; i < sz; ++i) { theory_var v = (i + start) % sz; + if (is_bool(v)) + continue; enode* n1 = var2enode(v); ensure_column(v); if (!can_get_ivalue(v)) @@ -933,6 +951,7 @@ namespace arith { } sat::check_result solver::check() { + force_push(); flet _is_learned(m_is_redundant, true); reset_variable_values(); IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); @@ -944,7 +963,7 @@ namespace arith { get_infeasibility_explanation_and_set_conflict(); return sat::check_result::CR_CONTINUE; case l_undef: - TRACE("arith", tout << "check feasiable is undef\n";); + TRACE("arith", tout << "check feasible is undef\n";); return m.inc() ? sat::check_result::CR_CONTINUE : sat::check_result::CR_GIVEUP; case l_true: break; @@ -989,7 +1008,7 @@ namespace arith { } if (m_not_handled != nullptr) { TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); - st = sat::check_result::CR_GIVEUP; + return sat::check_result::CR_GIVEUP; } return st; } @@ -1280,16 +1299,14 @@ namespace arith { app_ref atom(m); t = coeffs2app(coeffs, rational::zero(), is_int); - if (lower_bound) { - atom = a.mk_ge(t, a.mk_numeral(offset, is_int)); - } - else { - atom = a.mk_le(t, a.mk_numeral(offset, is_int)); - } + if (lower_bound) + atom = a.mk_ge(t, a.mk_numeral(offset, is_int)); + else + atom = a.mk_le(t, a.mk_numeral(offset, is_int)); TRACE("arith", tout << t << ": " << atom << "\n"; lp().print_term(term, tout << "bound atom: ") << (lower_bound ? " >= " : " <= ") << k << "\n";); - b_internalize(atom); + mk_literal(atom); return atom; } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 7190c7407..dcd856831 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -36,7 +36,7 @@ namespace euf { namespace arith { - typedef ptr_vector lp_bounds; + typedef ptr_vector> lp_bounds; typedef lp::var_index lpvar; typedef euf::theory_var theory_var; typedef euf::theory_id theory_id; @@ -45,6 +45,7 @@ namespace arith { typedef sat::literal literal; typedef sat::bool_var bool_var; typedef sat::literal_vector literal_vector; + typedef lp_api::bound api_bound; class solver : public euf::th_euf_solver { @@ -168,10 +169,10 @@ namespace arith { expr* m_not_handled{ nullptr }; ptr_vector m_underspecified; ptr_vector m_idiv_terms; - vector > m_use_list; // bounds where variables are used. + vector > m_use_list; // bounds where variables are used. // attributes for incremental version: - u_map m_bool_var2bound; + u_map m_bool_var2bound; vector m_bounds; unsigned_vector m_unassigned_bounds; unsigned_vector m_bounds_trail; @@ -215,6 +216,8 @@ namespace arith { bool is_int(euf::enode* n) const { return a.is_int(n->get_expr()); } bool is_real(theory_var v) const { return is_real(var2enode(v)); } bool is_real(euf::enode* n) const { return a.is_real(n->get_expr()); } + bool is_bool(theory_var v) const { return is_bool(var2enode(v)); } + bool is_bool(euf::enode* n) const { return m.is_bool(n->get_expr()); } // internalize @@ -262,13 +265,13 @@ namespace arith { void mk_is_int_axiom(expr* n); void mk_idiv_mod_axioms(expr* p, expr* q); void mk_rem_axiom(expr* dividend, expr* divisor); - void mk_bound_axioms(lp_api::bound& b); - void mk_bound_axiom(lp_api::bound& b1, lp_api::bound& b2); + void mk_bound_axioms(api_bound& b); + void mk_bound_axiom(api_bound& b1, api_bound& b2); void flush_bound_axioms(); // bounds struct compare_bounds { - bool operator()(lp_api::bound* a1, lp_api::bound* a2) const { return a1->get_value() < a2->get_value(); } + bool operator()(api_bound* a1, api_bound* a2) const { return a1->get_value() < a2->get_value(); } }; typedef lp_bounds::iterator iterator; @@ -279,30 +282,30 @@ namespace arith { iterator end); lp_bounds::iterator next_inf( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, bool& found_compatible); lp_bounds::iterator next_sup( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, bool& found_compatible); - void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value); + void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value); void propagate_basic_bounds(unsigned qhead); void propagate_bounds_with_lp_solver(); - void propagate_bound(literal lit, lp_api::bound& b); + void propagate_bound(literal lit, api_bound& b); void propagate_lp_solver_bound(const lp::implied_bound& be); void refine_bound(theory_var v, const lp::implied_bound& be); - literal is_bound_implied(lp::lconstraint_kind k, rational const& value, lp_api::bound const& b) const; - void assert_bound(bool is_true, lp_api::bound& b); + literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const; + void assert_bound(bool is_true, api_bound& b); void mk_eq_axiom(theory_var v1, theory_var v2); void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r); - lp_api::bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound); + api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound); lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true); void fixed_var_eh(theory_var v1, rational const& bound) {} bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } @@ -423,6 +426,7 @@ namespace arith { void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(eq.v1(), eq.v2()); } void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(de.v1(), de.v2()); } bool unit_propagate() override; + void init_model() override; void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void internalize(expr* e, bool redundant) override; diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 157a3b79a..69b589330 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -165,7 +165,7 @@ namespace array { euf::enode* s2 = e_internalize(sel2); if (s1->get_root() == s2->get_root()) return false; - sat::literal sel_eq = b_internalize(sel_eq_e); + sat::literal sel_eq = mk_literal(sel_eq_e); if (s().value(sel_eq) == l_true) return false; @@ -182,7 +182,7 @@ namespace array { add_clause(sel_eq); break; } - sat::literal idx_eq = b_internalize(m.mk_eq(idx1, idx2)); + sat::literal idx_eq = eq_internalize(idx1, idx2); if (add_clause(idx_eq, sel_eq)) new_prop = true; } @@ -225,10 +225,8 @@ namespace array { } expr_ref sel1(a.mk_select(args1), m); expr_ref sel2(a.mk_select(args2), m); - expr_ref n1_eq_n2(m.mk_eq(e1, e2), m); - expr_ref sel1_eq_sel2(m.mk_eq(sel1, sel2), m); - literal lit1 = b_internalize(n1_eq_n2); - literal lit2 = b_internalize(sel1_eq_sel2); + literal lit1 = eq_internalize(e1, e2); + literal lit2 = eq_internalize(sel1, sel2); return add_clause(lit1, ~lit2); } @@ -401,7 +399,6 @@ namespace array { ++m_stats.m_num_congruence_axiom; sort* srt = m.get_sort(e1); unsigned dimension = get_array_arity(srt); - expr_ref n1_eq_n2(m.mk_eq(e1, e2), m); expr_ref_vector args1(m), args2(m); args1.push_back(e1); args2.push_back(e2); @@ -420,9 +417,7 @@ namespace array { expr * eq = m.mk_eq(sel1, sel2); expr_ref q(m.mk_forall(dimension, sorts.c_ptr(), names.c_ptr(), eq), m); rewrite(q); - sat::literal fa_eq = b_internalize(q); - sat::literal neq = b_internalize(n1_eq_n2); - return add_clause(~neq, fa_eq); + return add_clause(~eq_internalize(e1, e2), mk_literal(q)); } bool solver::has_unitary_domain(app* array_term) { @@ -511,9 +506,8 @@ namespace array { if (have_different_model_values(v1, v2)) continue; if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) - continue; - expr_ref eq(m.mk_eq(e1, e2), m); - sat::literal lit = b_internalize(eq); + continue; + sat::literal lit = eq_internalize(e1, e2); if (s().value(lit) == l_undef) prop = true; } diff --git a/src/sat/smt/atom2bool_var.cpp b/src/sat/smt/atom2bool_var.cpp index 1fa3688a8..65c91ed79 100644 --- a/src/sat/smt/atom2bool_var.cpp +++ b/src/sat/smt/atom2bool_var.cpp @@ -31,10 +31,10 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const { } } -void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const { +void atom2bool_var::mk_var_inv(expr_ref_vector & var2expr) const { for (auto const& kv : m_mapping) { var2expr.reserve(kv.m_value + 1); - var2expr.set(kv.m_value, to_app(kv.m_key)); + var2expr.set(kv.m_value, kv.m_key); } } diff --git a/src/sat/smt/atom2bool_var.h b/src/sat/smt/atom2bool_var.h index f0244cbfd..794429701 100644 --- a/src/sat/smt/atom2bool_var.h +++ b/src/sat/smt/atom2bool_var.h @@ -30,7 +30,7 @@ public: void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); } sat::bool_var to_bool_var(expr * n) const; void mk_inv(expr_ref_vector & lit2expr) const; - void mk_var_inv(app_ref_vector & var2expr) const; + void mk_var_inv(expr_ref_vector & var2expr) const; // return true if the mapping contains uninterpreted atoms. bool interpreted_atoms() const { return expr2var::interpreted_vars(); } }; diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 0b6ff6838..a10104a80 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -131,7 +131,7 @@ namespace bv { bool solver::check_mul_invertibility(app* n, expr_ref_vector const& arg_values, expr* value) { - expr_ref inv(m), eq(m); + expr_ref inv(m); auto invert = [&](expr* s, expr* t) { return bv.mk_bv_and(bv.mk_bv_or(s, bv.mk_bv_neg(s)), t); @@ -143,9 +143,8 @@ namespace bv { }; auto add_inv = [&](expr* s) { inv = invert(s, n); - expr_ref eq(m.mk_eq(inv, n), m); - TRACE("bv", tout << "enforce " << eq << "\n";); - add_unit(b_internalize(eq)); + TRACE("bv", tout << "enforce " << inv << "\n";); + add_unit(eq_internalize(inv, n)); }; bool ok = true; for (unsigned i = 0; i < arg_values.size(); ++i) { @@ -177,10 +176,9 @@ namespace bv { args[i] = arg_value; expr_ref r(m.mk_app(n->get_decl(), args), m); set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier. - expr_ref eq(m.mk_eq(r, arg_value), m); args[i] = n->get_arg(i); - std::cout << eq << "@" << s().scope_lvl() << "\n"; - add_unit(b_internalize(eq)); + std::cout << "@" << s().scope_lvl() << "\n"; + add_unit(eq_internalize(r, arg_value)); } return false; } @@ -218,17 +216,15 @@ namespace bv { if (bv.is_one(arg_values[0])) { expr_ref mul1(m.mk_app(n->get_decl(), arg_values[0], n->get_arg(1)), m); set_delay_internalize(mul1, internalize_mode::init_bits_only_i); - expr_ref eq(m.mk_eq(mul1, n->get_arg(1)), m); - add_unit(b_internalize(eq)); - TRACE("bv", tout << eq << "\n";); + add_unit(eq_internalize(mul1, n->get_arg(1))); + TRACE("bv", tout << mul1 << "\n";); return false; } if (bv.is_one(arg_values[1])) { expr_ref mul1(m.mk_app(n->get_decl(), n->get_arg(0), arg_values[1]), m); set_delay_internalize(mul1, internalize_mode::init_bits_only_i); - expr_ref eq(m.mk_eq(mul1, n->get_arg(0)), m); - add_unit(b_internalize(eq)); - TRACE("bv", tout << eq << "\n";); + add_unit(eq_internalize(mul1, n->get_arg(0))); + TRACE("bv", tout << mul1 << "\n";); return false; } return true; @@ -296,9 +292,8 @@ namespace bv { expr_ref lhs(extract_low_bits(n), m); expr_ref rhs(m.mk_app(n->get_decl(), args), m); set_delay_internalize(rhs, internalize_mode::no_delay_i); - expr_ref eq(m.mk_eq(lhs, rhs), m); - add_unit(b_internalize(eq)); - TRACE("bv", tout << "low-bits: " << eq << "\n";); + add_unit(eq_internalize(lhs, rhs)); + TRACE("bv", tout << "low-bits: " << mk_pp(lhs,m) << " " << mk_pp(rhs, m) << "\n";); std::cout << "low bits\n"; return false; } @@ -320,10 +315,6 @@ namespace bv { }; /** -<<<<<<< HEAD - -======= ->>>>>>> 055902df2... bv * The i'th bit in xs is 1 if the least significant bit of x is i or lower. */ void solver::encode_lsb_tail(expr* x, expr_ref_vector& xs) { @@ -361,8 +352,8 @@ namespace bv { encode_msb_tail(n->get_arg(0), xs); encode_msb_tail(n->get_arg(1), ys); for (unsigned i = 1; i <= sz; ++i) { - sat::literal bit0 = b_internalize(xs.get(i - 1)); - sat::literal bit1 = b_internalize(ys.get(sz - i)); + sat::literal bit0 = mk_literal(xs.get(i - 1)); + sat::literal bit1 = mk_literal(ys.get(sz - i)); add_clause(~no_overflow, ~bit0, ~bit1); } return false; @@ -374,7 +365,7 @@ namespace bv { lits.push_back(expr2literal(n)); for (unsigned i = 1; i < sz; ++i) { expr_ref msb_ge_sz(m.mk_and(xs.get(i - 1), ys.get(sz - i - 1)), m); - lits.push_back(b_internalize(msb_ge_sz)); + lits.push_back(mk_literal(msb_ge_sz)); } add_clause(lits); return false; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 0690e6f06..9e39a1ffa 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -519,16 +519,14 @@ namespace bv { expr* arg1 = n->get_arg(0); expr* arg2 = n->get_arg(1); if (p.hi_div0()) { - expr_ref eq(m.mk_eq(n, bv.mk_bv_udiv_i(arg1, arg2)), m); - add_unit(b_internalize(eq)); + add_unit(eq_internalize(n, bv.mk_bv_udiv_i(arg1, arg2))); return; } unsigned sz = bv.get_bv_size(n); expr_ref zero(bv.mk_numeral(0, sz), m); expr_ref eq(m.mk_eq(arg2, zero), m); expr_ref udiv(m.mk_ite(eq, bv.mk_bv_udiv0(arg1), bv.mk_bv_udiv_i(arg1, arg2)), m); - expr_ref eq2(m.mk_eq(n, udiv), m); - add_unit(b_internalize(eq2)); + add_unit(eq_internalize(n, udiv)); } void solver::internalize_unary(app* n, std::function& fn) { diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index ba36af1ec..3739b87c6 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -187,7 +187,7 @@ namespace dt { ptr_vector const& accessors = *dt.get_constructor_accessors(con); app_ref rec_app(m.mk_app(rec, arg1), m); app_ref acc_app(m); - literal is_con = b_internalize(rec_app); + literal is_con = mk_literal(rec_app); for (func_decl* acc1 : accessors) { enode* arg; if (acc1 == acc) { @@ -278,7 +278,7 @@ namespace dt { SASSERT(r != nullptr); app_ref r_app(m.mk_app(r, n->get_expr()), m); TRACE("dt", tout << "creating split: " << mk_pp(r_app, m) << "\n";); - b_internalize(r_app); + mk_literal(r_app); } void solver::apply_sort_cnstr(enode* n, sort* s) { @@ -433,7 +433,7 @@ namespace dt { ptr_vector const& constructors = *dt.get_datatype_constructors(srt); func_decl* rec = dt.get_constructor_is(constructors[unassigned_idx]); app_ref rec_app(m.mk_app(rec, n->get_expr()), m); - consequent = b_internalize(rec_app); + consequent = mk_literal(rec_app); } else consequent = ctx.enode2literal(r); diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 2a1670cc7..eab04ff42 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -33,6 +33,11 @@ namespace euf { SASSERT(m_egraph.find(e)); } + sat::literal solver::mk_literal(expr* e) { + expr_ref _e(e, m); + return internalize(e, false, false, m_is_redundant); + } + sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { euf::enode* n = get_enode(e); if (n) { diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 0be72a4df..422cd746e 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -23,8 +23,11 @@ Author: namespace euf { void solver::update_model(model_ref& mdl) { + for (auto* mb : m_solvers) + mb->init_model(); deps_t deps; m_values.reset(); + m_values2root.reset(); collect_dependencies(deps); deps.topological_sort(); dependencies2values(deps, mdl); @@ -117,7 +120,7 @@ namespace euf { } if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id()) continue; - sat::bool_var v = si.to_bool_var(e); + sat::bool_var v = get_enode(e)->bool_var(); SASSERT(v != sat::null_bool_var); switch (s().value(v)) { case l_true: @@ -131,7 +134,6 @@ namespace euf { } continue; } - TRACE("euf", tout << "value for " << mk_bounded_pp(e, m) << "\n";); sort* srt = m.get_sort(e); if (m.is_uninterp(srt)) user_sort.add(id, srt); @@ -186,11 +188,12 @@ namespace euf { // TODO } - obj_map const& solver::values2root() { - m_values2root.reset(); + obj_map const& solver::values2root() { + if (!m_values2root.empty()) + return m_values2root; for (enode* n : m_egraph.nodes()) - if (n->is_root()) - m_values2root.insert(m_values.get(n->get_root_id()), n); + if (n->is_root() && m_values.get(n->get_expr_id())) + m_values2root.insert(m_values.get(n->get_expr_id()), n); return m_values2root; } diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index 77590346b..2ffaa7827 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -79,6 +79,7 @@ namespace euf { continue; expr* c = nullptr, *th = nullptr, *el = nullptr; if (m.is_ite(e, c, th, el)) { + std::cout << mk_pp(c, m) << "\n"; sat::literal lit = expr2literal(c); todo.push_back(c); switch (s().value(lit)) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 2c8d46be3..2ab0b6d78 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -296,6 +296,7 @@ namespace euf { // internalize sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void internalize(expr* e, bool learned) override; + sat::literal mk_literal(expr* e); void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); } void attach_node(euf::enode* n); expr_ref mk_eq(expr* e1, expr* e2); diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 63a9ba2a1..01d7e286d 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -75,7 +75,7 @@ namespace fpa { for (expr* arg : m_converter.m_extra_assertions) { ctx.get_rewriter()(arg, t); m_th_rw(t); - conds.push_back(b_internalize(t)); + conds.push_back(mk_literal(t)); } m_converter.m_extra_assertions.reset(); return conds; @@ -125,7 +125,7 @@ namespace fpa { if (m.is_bool(e)) { sat::literal atom(ctx.get_si().add_bool_var(e), false); atom = ctx.attach_lit(atom, e); - sat::literal bv_atom = b_internalize(m_rw.convert_atom(m_th_rw, e)); + sat::literal bv_atom = mk_literal(m_rw.convert_atom(m_th_rw, e)); sat::literal_vector conds = mk_side_conditions(); conds.push_back(bv_atom); add_equiv_and(atom, conds); @@ -143,8 +143,7 @@ namespace fpa { case OP_FPA_TO_REAL: case OP_FPA_TO_IEEE_BV: { expr_ref conv = convert(e); - expr_ref eq = ctx.mk_eq(e, conv); - add_unit(b_internalize(eq)); + add_unit(eq_internalize(e, conv)); add_units(mk_side_conditions()); break; } @@ -174,7 +173,7 @@ namespace fpa { expr_ref valid(m), limit(m); limit = m_bv_util.mk_numeral(4, 3); valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit); - add_unit(b_internalize(valid)); + add_unit(mk_literal(valid)); } activate(owner); } @@ -193,21 +192,18 @@ namespace fpa { if (m_fpa_util.is_rm_numeral(n, rm)) { expr_ref rm_num(m); rm_num = m_bv_util.mk_numeral(rm, 3); - add_unit(b_internalize(ctx.mk_eq(wrapped, rm_num))); + add_unit(eq_internalize(wrapped, rm_num)); } else if (m_fpa_util.is_numeral(n, val)) { expr_ref bv_val_e(convert(n), m); VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c)); expr* args[] = { a, b, c }; expr_ref cc_args(m_bv_util.mk_concat(3, args), m); - add_unit(b_internalize(ctx.mk_eq(wrapped, cc_args))); + add_unit(eq_internalize(wrapped, cc_args)); add_units(mk_side_conditions()); } - else { - expr_ref wu = ctx.mk_eq(m_converter.unwrap(wrapped, m.get_sort(n)), n); - TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;); - add_unit(b_internalize(wu)); - } + else + add_unit(eq_internalize(m_converter.unwrap(wrapped, m.get_sort(n)), n)); } } else if (is_app(n) && to_app(n)->get_family_id() == get_id()) { @@ -252,8 +248,8 @@ namespace fpa { m_th_rw(c); - sat::literal eq1 = b_internalize(ctx.mk_eq(e_x, e_y)); - sat::literal eq2 = b_internalize(c); + sat::literal eq1 = eq_internalize(xe, ye); + sat::literal eq2 = mk_literal(c); add_equiv(eq1, eq2); add_units(mk_side_conditions()); } @@ -271,7 +267,7 @@ namespace fpa { TRACE("t_fpa", tout << "assign_eh for: " << l << "\n" << mk_ismt2_pp(e, m) << "\n";); - sat::literal c = b_internalize(convert(e)); + sat::literal c = mk_literal(convert(e)); sat::literal_vector conds = mk_side_conditions(); conds.push_back(c); if (l.sign()) { diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index f007fce83..f9c5d9e93 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -16,7 +16,12 @@ Author: --*/ #include "ast/ast_trail.h" +#include "ast/ast_util.h" #include "ast/rewriter/var_subst.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "qe/mbp/mbp_arith.h" +#include "qe/mbp/mbp_arrays.h" +#include "qe/mbp/mbp_datatypes.h" #include "sat/smt/sat_th.h" #include "sat/smt/q_mbi.h" #include "sat/smt/q_solver.h" @@ -25,21 +30,25 @@ Author: namespace q { - mbqi::mbqi(euf::solver& ctx, solver& s): - ctx(ctx), - qs(s), - m(s.get_manager()), - m_model_fixer(ctx, qs), - m_model_finder(ctx), - m_fresh_trail(m) - {} + mbqi::mbqi(euf::solver& ctx, solver& s) : + ctx(ctx), + m_qs(s), + m(s.get_manager()), + m_model_fixer(ctx, m_qs), + m_fresh_trail(m) + { + auto* ap = alloc(mbp::arith_project_plugin, m); + ap->set_check_purified(false); + add_plugin(ap); + add_plugin(alloc(mbp::datatype_project_plugin, m)); + add_plugin(alloc(mbp::array_project_plugin, m)); + } - void mbqi::restrict_to_universe(expr * sk, ptr_vector const & universe) { + void mbqi::restrict_to_universe(expr* sk, ptr_vector const& universe) { SASSERT(!universe.empty()); expr_ref_vector eqs(m); - for (expr * e : universe) { + for (expr* e : universe) eqs.push_back(m.mk_eq(sk, e)); - } expr_ref fml(m.mk_or(eqs), m); m_solver->assert_expr(fml); } @@ -53,10 +62,8 @@ namespace q { m_values.push_back(values); } if (!values->contains(e)) { - for (expr* b : *values) { - expr_ref eq = ctx.mk_eq(e, b); - qs.add_unit(~qs.b_internalize(eq)); - } + for (expr* b : *values) + m_qs.add_unit(~m_qs.eq_internalize(e, b)); values->insert(e); m_fresh_trail.push_back(e); } @@ -66,15 +73,14 @@ namespace q { // for fixed value return expr // new fixed value is distinct from other expr expr_ref mbqi::replace_model_value(expr* e) { - if (m.is_model_value(e)) { + if (m.is_model_value(e)) { register_value(e); return expr_ref(e, m); } if (is_app(e) && to_app(e)->get_num_args() > 0) { expr_ref_vector args(m); - for (expr* arg : *to_app(e)) { + for (expr* arg : *to_app(e)) args.push_back(replace_model_value(arg)); - } return expr_ref(m.mk_app(to_app(e)->get_decl(), args), m); } return expr_ref(e, m); @@ -84,114 +90,146 @@ namespace q { unsigned sz = r->class_size(); unsigned start = ctx.s().rand()() % sz; unsigned i = 0; - for (euf::enode* n : euf::enode_class(r)) + for (euf::enode* n : euf::enode_class(r)) if (i++ >= start) return expr_ref(n->get_expr(), m); return expr_ref(nullptr, m); } - + lbool mbqi::check_forall(quantifier* q) { + + quantifier* q_flat = m_qs.flatten(q); + auto* qb = specialize(q_flat); + if (!qb) + return l_undef; + if (m.is_false(qb->mbody)) + return l_true; init_solver(); ::solver::scoped_push _sp(*m_solver); - expr_ref_vector vars(m); - quantifier* q_flat = qs.flatten(q); - expr_ref body = specialize(q_flat, vars); - m_solver->assert_expr(body); + m_solver->assert_expr(qb->mbody); lbool r = m_solver->check_sat(0, nullptr); if (r == l_undef) return r; if (r == l_false) return l_true; - model_ref mdl0, mdl1; - m_solver->get_model(mdl0); - expr_ref proj(m); - auto add_projection = [&](model& mdl, bool inv) { - proj = project(mdl, q_flat, vars, inv); - if (!proj) - return; - if (is_forall(q)) - qs.add_clause(~ctx.expr2literal(q), ctx.b_internalize(proj)); - else - qs.add_clause(ctx.expr2literal(q), ~ctx.b_internalize(proj)); - }; - bool added = false; -#if 0 - m_model_finder.restrict_instantiations(*m_solver, *mdl0, q_flat, vars); - for (unsigned i = 0; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) { - m_solver->get_model(mdl1); - add_projection(*mdl1, true); - if (!proj) - break; - added = true; - m_solver->assert_expr(m.mk_not(proj)); - } -#endif - if (!added) { - add_projection(*mdl0, false); - added = proj; - } - return added ? l_false : l_undef; + model_ref mdl0; + m_solver->get_model(mdl0); + expr_ref proj = solver_project(*mdl0, *qb); + if (!proj) + return l_undef; + sat::literal qlit = ctx.expr2literal(q); + if (is_exists(q)) + qlit.neg(); + ctx.get_rewriter()(proj); + TRACE("q", tout << proj << "\n";); + // TODO: add as top-level clause for relevancy + m_qs.add_clause(~qlit, ~ctx.mk_literal(proj)); + return l_false; } - expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) { - expr_ref body(m); - unsigned sz = q->get_num_decls(); - if (!m_model->eval_expr(q->get_expr(), body, true)) - return expr_ref(m); - vars.resize(sz, nullptr); - for (unsigned i = 0; i < sz; ++i) { - sort* s = q->get_decl_sort(i); - vars[i] = m.mk_fresh_const(q->get_decl_name(i), s, false); - if (m_model->has_uninterpreted_sort(s)) - restrict_to_universe(vars.get(i), m_model->get_universe(s)); - } + mbqi::q_body* mbqi::specialize(quantifier* q) { + mbqi::q_body* result = nullptr; var_subst subst(m); - body = subst(body, vars); - if (is_forall(q)) - body = m.mk_not(body); - return body; + if (!m_q2body.find(q, result)) { + unsigned sz = q->get_num_decls(); + result = alloc(q_body, m); + m_q2body.insert(q, result); + ctx.push(new_obj_trail(result)); + ctx.push(insert_obj_map(m_q2body, q)); + app_ref_vector& vars = result->vars; + vars.resize(sz, nullptr); + for (unsigned i = 0; i < sz; ++i) { + sort* s = q->get_decl_sort(i); + vars[i] = m.mk_fresh_const(q->get_decl_name(i), s, false); + if (m_model->has_uninterpreted_sort(s)) + restrict_to_universe(vars.get(i), m_model->get_universe(s)); + } + expr_ref fml = subst(q->get_expr(), vars); + if (is_forall(q)) + fml = m.mk_not(fml); + flatten_and(fml, result->vbody); + } + expr_ref& mbody = result->mbody; + unsigned sz = q->get_num_decls(); + if (!m_model->eval_expr(q->get_expr(), mbody, true)) + return nullptr; + + mbody = subst(mbody, result->vars); + if (is_forall(q)) + mbody = mk_not(m, mbody); + return result; } /** * A most rudimentary projection operator that only tries to find proxy terms from the set of existing terms. * Refinements: - * - grammar based from MBQI paper + * - grammar based from MBQI paper * - quantifier elimination based on projection operators defined in qe. - * + * * - eliminate as-array terms, use lambda - * - have mode with inv-term from model-finder */ - expr_ref mbqi::project(model& mdl, quantifier* q, expr_ref_vector& vars, bool inv) { + expr_ref mbqi::basic_project(model& mdl, quantifier* q, app_ref_vector& vars) { unsigned sz = q->get_num_decls(); unsigned max_generation = 0; expr_ref_vector vals(m); vals.resize(sz, nullptr); - auto const& v2r = ctx.values2root(); for (unsigned i = 0; i < sz; ++i) { - app* v = to_app(vars.get(i)); - func_decl* f = v->get_decl(); - expr_ref val(mdl.get_some_const_interp(f), m); - if (!val) - return expr_ref(m); - val = mdl.unfold_as_array(val); - if (!val) - return expr_ref(m); - if (inv) - vals[i] = m_model_finder.inv_term(mdl, q, i, val, max_generation); - euf::enode* r = nullptr; - if (!vals.get(i) && v2r.find(val, r)) - vals[i] = choose_term(r); + app* v = vars.get(i); + vals[i] = assign_value(mdl, v); if (!vals.get(i)) - vals[i] = replace_model_value(val); + return expr_ref(m); } var_subst subst(m); - return subst(q->get_expr(), vals); + return subst(q->get_expr(), vals); + } + + expr_ref mbqi::solver_project(model& mdl, q_body& qb) { + for (app* v : qb.vars) + m_model->register_decl(v->get_decl(), mdl(v)); + expr_ref_vector fmls(qb.vbody); + app_ref_vector vars(qb.vars); + mbp::project_plugin proj(m); + proj.purify(m_model_fixer, *m_model, vars, fmls); + for (unsigned i = 0; i < vars.size(); ++i) { + app* v = vars.get(i); + auto* p = get_plugin(v); + if (p) + (*p)(*m_model, vars, fmls); + } + if (!vars.empty()) { + expr_safe_replace esubst(m); + for (app* v : vars) { + expr_ref val = assign_value(*m_model, v); + if (!val) + return expr_ref(m); + esubst.insert(v, val); + } + esubst(fmls); + } + return mk_and(fmls); + } + + expr_ref mbqi::assign_value(model& mdl, app* v) { + func_decl* f = v->get_decl(); + expr_ref val(mdl.get_some_const_interp(f), m); + if (!val) + return expr_ref(m); + val = mdl.unfold_as_array(val); + if (!val) + return expr_ref(m); + euf::enode* r = nullptr; + auto const& v2r = ctx.values2root(); + if (v2r.find(val, r)) + val = choose_term(r); + else + val = replace_model_value(val); + return val; } lbool mbqi::operator()() { lbool result = l_true; m_model = nullptr; - for (sat::literal lit : qs.m_universal) { + for (sat::literal lit : m_qs.m_universal) { quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); if (!ctx.is_relevant(q)) continue; @@ -232,4 +270,16 @@ namespace q { m_model_fixer(mdl); } + mbp::project_plugin* mbqi::get_plugin(app* var) { + family_id fid = m.get_sort(var)->get_family_id(); + return m_plugins.get(fid, nullptr); + } + + void mbqi::add_plugin(mbp::project_plugin* p) { + family_id fid = p->get_family_id(); + m_plugins.reserve(fid + 1); + SASSERT(!m_plugins.get(fid, nullptr)); + m_plugins.set(fid, p); + } + } diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index 541de3fa5..52544e5aa 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -17,8 +17,8 @@ Author: #pragma once #include "solver/solver.h" +#include "qe/mbp/mbp_plugin.h" #include "sat/smt/sat_th.h" -#include "sat/smt/q_model_finder.h" #include "sat/smt/q_model_fixer.h" namespace euf { @@ -30,16 +30,24 @@ namespace q { class solver; class mbqi { + struct q_body { + app_ref_vector vars; + expr_ref mbody; // body specialized with respect to model + expr_ref_vector vbody; // (negation of) body specialized with respect to vars + q_body(ast_manager& m) : vars(m), mbody(m), vbody(m) {} + }; + euf::solver& ctx; - solver& qs; + solver& m_qs; ast_manager& m; model_fixer m_model_fixer; - model_finder m_model_finder; model_ref m_model; ref<::solver> m_solver; obj_map*> m_fresh; scoped_ptr_vector> m_values; expr_ref_vector m_fresh_trail; + scoped_ptr_vector m_plugins; + obj_map m_q2body; unsigned m_max_cex{ 1 }; void restrict_to_universe(expr * sk, ptr_vector const & universe); @@ -47,10 +55,14 @@ namespace q { expr_ref replace_model_value(expr* e); expr_ref choose_term(euf::enode* r); lbool check_forall(quantifier* q); - expr_ref specialize(quantifier* q, expr_ref_vector& vars); - expr_ref project(model& mdl, quantifier* q, expr_ref_vector& vars, bool inv); + q_body* specialize(quantifier* q); + expr_ref basic_project(model& mdl, quantifier* q, app_ref_vector& vars); + expr_ref solver_project(model& mdl, q_body& qb); + expr_ref assign_value(model& mdl, app* v); void init_model(); void init_solver(); + mbp::project_plugin* get_plugin(app* var); + void add_plugin(mbp::project_plugin* p); public: diff --git a/src/sat/smt/q_model_finder.cpp b/src/sat/smt/q_model_finder.cpp deleted file mode 100644 index 6077aaaa9..000000000 --- a/src/sat/smt/q_model_finder.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - q_model_finder.cpp - -Abstract: - - Model-based quantifier instantiation model-finder plugin - -Author: - - Nikolaj Bjorner (nbjorner) 2020-09-29 - -Notes: - - Derives from smt/smt_model_finder.cpp - ---*/ - -#include "sat/smt/q_model_finder.h" -#include "sat/smt/euf_solver.h" - - -namespace q { - - model_finder::model_finder(euf::solver& ctx): - ctx(ctx), m(ctx.get_manager()) {} - - expr_ref model_finder::inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation) { - return expr_ref(value, m); - } - - void model_finder::restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars) { - - } - - void model_finder::adjust_model(model& mdl) { - - } - -} diff --git a/src/sat/smt/q_model_finder.h b/src/sat/smt/q_model_finder.h deleted file mode 100644 index f9ac8bdc0..000000000 --- a/src/sat/smt/q_model_finder.h +++ /dev/null @@ -1,60 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - q_model_finder.h - -Abstract: - - Model-based quantifier instantiation model-finder plugin - -Author: - - Nikolaj Bjorner (nbjorner) 2020-09-29 - -Notes: - - Derives from smt/smt_model_finder.cpp - ---*/ -#pragma once - -#include "sat/smt/sat_th.h" -#include "solver/solver.h" - -namespace euf { - class solver; -} - -namespace q { - - class model_finder { - euf::solver& ctx; - ast_manager& m; - - public: - - model_finder(euf::solver& ctx); - - /** - * Compute an instantiation terms for the i'th bound variable in quantifier q. - */ - expr_ref inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation); - - /** - * Pre-restrict instantiations of vars, by adding constraints to solver s - */ - void restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars); - - /** - * Update model in order to best satisfy quantifiers. - * For the array property fragment, update the model - * such that the range of functions behaves monotonically - * based on regions over the inputs. - */ - void adjust_model(model& mdl); - - }; - -} diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index db79e598f..4b02e324b 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -41,20 +41,18 @@ namespace q { } class arith_projection : public projection_function { - ast_manager& m; arith_util a; public: - arith_projection(ast_manager& m): m(m), a(m) {} + arith_projection(ast_manager& m): projection_function(m), a(m) {} ~arith_projection() override {} bool operator()(expr* e1, expr* e2) const override { return lt(a, e1, e2); } expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); } }; class ubv_projection : public projection_function { - ast_manager& m; bv_util bvu; public: - ubv_projection(ast_manager& m): m(m), bvu(m) {} + ubv_projection(ast_manager& m): projection_function(m), bvu(m) {} ~ubv_projection() override {} bool operator()(expr* e1, expr* e2) const override { return lt(bvu, e1, e2); } expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); } @@ -113,6 +111,7 @@ namespace q { void model_fixer::add_projection_functions(model& mdl, func_decl* f) { // update interpretation of f so that the graph of f is fully determined by the // ground values of its arguments. + TRACE("q", tout << mdl << "\n";); func_interp* fi = mdl.get_func_interp(f); if (!fi) return; @@ -133,6 +132,7 @@ namespace q { new_fi->set_else(m.mk_app(f_new, args)); mdl.update_func_interp(f, new_fi); mdl.register_decl(f_new, fi); + TRACE("q", tout << mdl << "\n";); } expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) { @@ -209,4 +209,55 @@ namespace q { fns.insert(to_app(t)->get_decl()); } } + + expr* model_fixer::invert_app(app* t, expr* value) { + euf::enode* r = nullptr; + TRACE("q", + tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n"; + if (ctx.values2root().find(value, r)) + tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";); + if (ctx.values2root().find(value, r)) + return r->get_expr(); + return value; + } + + expr* model_fixer::invert_arg(app* t, unsigned i, expr* value) { + TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";); + auto const* md = get_projection_data(t->get_decl(), i); + if (!md) + return m.mk_true(); + auto* proj = get_projection(t->get_decl()->get_domain(i)); + if (!proj) + return m.mk_true(); + + unsigned sz = md->values.size(); + if (sz <= 1) + return m.mk_true(); + + // + // md->values are sorted + // v1, v2, v3 + // x < v2 => f(x) = f(v1), so x < t2, where M(v2) = t2 + // v2 <= x < v3 => f(x) = f(v2), so t2 <= x < t3, where M(v3) = t3 + // v3 <= x => f(x) = f(v3) + // + auto is_lt = [&](expr* val) { + return (*proj)(value, val); + }; + + auto term = [&](unsigned j) { + return md->v2t[md->values[j]]; + }; + + expr* arg = t->get_arg(i); + + if (is_lt(md->values[1])) + return proj->mk_lt(arg, term(1)); + + for (unsigned j = 2; j < sz; ++j) + if (is_lt(md->values[j])) + return m.mk_and(proj->mk_le(term(j-1), arg), proj->mk_lt(arg, term(j))); + + return proj->mk_le(term(sz-1), arg); + } } diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index d14e5b351..aae50a6f0 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -26,6 +26,7 @@ Notes: #include "sat/smt/sat_th.h" #include "solver/solver.h" #include "model/model_macro_solver.h" +#include "qe/mbp/mbp_plugin.h" namespace euf { class solver; @@ -38,9 +39,13 @@ namespace q { typedef obj_hashtable func_decl_set; class projection_function { + protected: + ast_manager& m; public: + projection_function(ast_manager& m) : m(m) {} virtual ~projection_function() {} virtual expr* mk_lt(expr* a, expr* b) = 0; + expr* mk_le(expr* a, expr* b) { return m.mk_not(mk_lt(b, a)); } virtual bool operator()(expr* a, expr* b) const = 0; }; @@ -65,10 +70,10 @@ namespace q { struct eq { bool operator()(indexed_decl const& a, indexed_decl const& b) const { return a.idx == b.idx && a.f == b.f; } }; }; - class model_fixer : public quantifier2macro_infos { - euf::solver& ctx; - solver& m_qs; - ast_manager& m; + class model_fixer : public quantifier2macro_infos, public mbp::euf_inverter { + euf::solver& ctx; + solver& m_qs; + ast_manager& m; obj_map m_q2info; func_decl_dependencies m_dependencies; obj_map m_projections; @@ -81,6 +86,12 @@ namespace q { void collect_partial_functions(ptr_vector const& qs, func_decl_set& fns); projection_function* get_projection(sort* srt); + projection_meta_data* get_projection_data(func_decl* f, unsigned idx) const { + projection_meta_data* r = nullptr; + m_projection_data.find(indexed_decl(f, idx), r); + return r; + } + public: model_fixer(euf::solver& ctx, solver& qs); @@ -89,19 +100,15 @@ namespace q { /** * Update model in order to best satisfy quantifiers. * For the array property fragment, update the model - * such that the range of functions behaves monotonically + * such that the range of functions behaves monotonically * based on regions over the inputs. */ void operator()(model& mdl); quantifier_macro_info* operator()(quantifier* q) override; - projection_meta_data* operator()(func_decl* f, unsigned idx) const { - projection_meta_data* r = nullptr; - m_projection_data.find(indexed_decl(f, idx), r); - return r; - } - + expr* invert_app(app* t, expr* value) override; + expr* invert_arg(app* t, unsigned i, expr* value) override; }; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 2cc4d84ec..a31ac5f78 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -27,14 +27,15 @@ namespace q { solver::solver(euf::solver& ctx, family_id fid) : th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid), m_mbqi(ctx, *this) - {} + { + } void solver::asserted(sat::literal l) { expr* e = bool_var2expr(l.var()); - SASSERT(is_forall(e) || is_exists(e)); - if (l.sign() == is_forall(e)) { + if (!is_forall(e) && !is_exists(e)) + return; + if (l.sign() == is_forall(e)) add_clause(~l, skolemize(to_quantifier(e))); - } else { add_clause(~l, specialize(to_quantifier(e))); ctx.push_vec(m_universal, l); @@ -45,7 +46,7 @@ namespace q { sat::check_result solver::check() { if (ctx.get_config().m_mbqi) { switch (m_mbqi()) { - case l_true: return sat::check_result::CR_DONE; + case l_true: return sat::check_result::CR_DONE; case l_false: return sat::check_result::CR_CONTINUE; case l_undef: return sat::check_result::CR_GIVEUP; } @@ -95,8 +96,8 @@ namespace q { vars[i] = mk_var(q_flat, i); var_subst subst(m); expr_ref body = subst(q_flat->get_expr(), vars); - ctx.get_rewriter()(body); - return b_internalize(body); + rewrite(body); + return mk_literal(body); } sat::literal solver::skolemize(quantifier* q) { diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 07b9e3323..686a898d5 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -200,9 +200,21 @@ namespace euf { return ctx.mk_eq(e1, e2); } + sat::literal th_euf_solver::mk_literal(expr* e) const { + return ctx.mk_literal(e); + } + sat::literal th_euf_solver::eq_internalize(expr* a, expr* b) { - expr_ref eq(ctx.mk_eq(a, b), m); - return b_internalize(eq); + return mk_literal(ctx.mk_eq(a, b)); + } + + euf::enode* th_euf_solver::e_internalize(expr* e) { + euf::enode* n = expr2enode(e); + if (!n) { + ctx.internalize(e, m_is_redundant); + n = expr2enode(e); + } + return n; } unsigned th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) { diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index e0e99bb08..83ae823c4 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -45,9 +45,6 @@ namespace euf { virtual void internalize(expr* e, bool redundant) = 0; - sat::literal b_internalize(expr* e) { return internalize(e, false, false, m_is_redundant); } - - sat::literal mk_literal(expr* e) { return b_internalize(e); } /** \brief Apply (interpreted) sort constraints on the given enode. @@ -89,6 +86,11 @@ namespace euf { */ virtual bool include_func_interp(func_decl* f) const { return false; } + /** + \brief initialize model building + */ + virtual void init_model() {} + /** \brief conclude model building */ @@ -149,7 +151,7 @@ namespace euf { sat::literal eq_internalize(expr* a, expr* b); - euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); } + euf::enode* e_internalize(expr* e); euf::enode* mk_enode(expr* e, bool suppress_args = false); expr_ref mk_eq(expr* e1, expr* e2); expr_ref mk_var_eq(theory_var v1, theory_var v2) { return mk_eq(var2expr(v1), var2expr(v2)); } @@ -176,6 +178,7 @@ namespace euf { expr* bool_var2expr(sat::bool_var v) const; enode* bool_var2enode(sat::bool_var v) const { expr* e = bool_var2expr(v); return e ? expr2enode(e) : nullptr; } expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); } + sat::literal mk_literal(expr* e) const; theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); } theory_var get_th_var(expr* e) const; trail_stack& get_trail_stack(); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7cabedf25..131adabc3 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -277,17 +277,17 @@ struct goal2sat::imp : public sat::sat_internalizer { else if (m.is_false(t)) { l = sign ? mk_true() : ~mk_true(); } - else if (!is_app(t)) { - std::ostringstream strm; - strm << mk_ismt2_pp(t, m); - throw_op_not_handled(strm.str()); - } else { if (!is_uninterp_const(t)) { if (m_euf) { convert_euf(t, root, sign); return; } + else if (!is_app(t)) { + std::ostringstream strm; + strm << mk_ismt2_pp(t, m); + throw_op_not_handled(strm.str()); + } else m_unhandled_funs.push_back(to_app(t)->get_decl()); } @@ -1054,7 +1054,7 @@ model_converter* sat2goal::mc::translate(ast_translation& translator) { mc* result = alloc(mc, translator.to()); result->m_smc.copy(m_smc); result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; - for (app* e : m_var2expr) { + for (expr* e : m_var2expr) { result->m_var2expr.push_back(translator(e)); } return result; @@ -1093,15 +1093,15 @@ void sat2goal::mc::operator()(expr_ref& fml) { if (m_gmc) (*m_gmc)(fml); } -void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { +void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) { SASSERT(!m_var2expr.get(v, nullptr)); m_var2expr.reserve(v + 1); m_var2expr.set(v, atom); if (aux) { - SASSERT(is_uninterp_const(atom)); SASSERT(m.is_bool(atom)); if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - m_gmc->hide(atom->get_decl()); + if (is_uninterp_const(atom)) + m_gmc->hide(to_app(atom)->get_decl()); } TRACE("sat_mc", tout << "insert " << v << "\n";); } @@ -1151,7 +1151,7 @@ struct sat2goal::imp { expr * lit2expr(ref& mc, sat::literal l) { if (!m_lit2expr.get(l.index())) { SASSERT(m_lit2expr.get((~l).index()) == 0); - app* aux = mc ? mc->var2expr(l.var()) : nullptr; + expr* aux = mc ? mc->var2expr(l.var()) : nullptr; if (!aux) { aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); if (mc) { diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 298e9dc36..e55b856ab 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -82,7 +82,7 @@ public: ast_manager& m; sat::model_converter m_smc; generic_model_converter_ref m_gmc; - app_ref_vector m_var2expr; + expr_ref_vector m_var2expr; // flushes from m_smc to m_gmc; void flush_gmc(); @@ -99,9 +99,9 @@ public: void set_env(ast_pp_util* visitor) override; void display(std::ostream& out) override; void get_units(obj_map& units) override; - app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } + expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } expr_ref lit2expr(sat::literal l); - void insert(sat::bool_var v, app * atom, bool aux); + void insert(sat::bool_var v, expr * atom, bool aux); }; sat2goal(); diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index f797a7f40..d502aaac9 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(smt cached_var_subst.cpp cost_evaluator.cpp dyn_ack.cpp - elim_term_ite.cpp expr_context_simplifier.cpp fingerprints.cpp mam.cpp diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index d4fdc428c..570d0ffde 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -34,9 +34,9 @@ Revision History: #include "ast/macros/macro_finder.h" #include "ast/normal_forms/defined_names.h" #include "ast/normal_forms/pull_quant.h" +#include "ast/normal_forms/elim_term_ite.h" #include "ast/pattern/pattern_inference.h" #include "smt/params/smt_params.h" -#include "smt/elim_term_ite.h" class asserted_formulas { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e4999d6c2..0421c5f46 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -54,7 +54,9 @@ typedef lp::var_index lpvar; namespace smt { -typedef ptr_vector lp_bounds; + typedef lp_api::bound api_bound; + + typedef ptr_vector lp_bounds; class theory_lra::imp { @@ -163,10 +165,10 @@ class theory_lra::imp { expr* m_not_handled; ptr_vector m_underspecified; ptr_vector m_idiv_terms; - vector > m_use_list; // bounds where variables are used. + vector > m_use_list; // bounds where variables are used. // attributes for incremental version: - u_map m_bool_var2bound; + u_map m_bool_var2bound; vector m_bounds; unsigned_vector m_unassigned_bounds; unsigned_vector m_bounds_trail; @@ -721,7 +723,7 @@ class theory_lra::imp { void del_bounds(unsigned old_size) { for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) { unsigned v = m_bounds_trail[i]; - lp_api::bound* b = m_bounds[v].back(); + api_bound* b = m_bounds[v].back(); // del_use_lists(b); dealloc(b); m_bounds[v].pop_back(); @@ -939,7 +941,7 @@ public: if (is_int(v) && !r.is_int()) { r = (k == lp_api::upper_t) ? floor(r) : ceil(r); } - lp_api::bound* b = mk_var_bound(bv, v, k, r); + api_bound* b = mk_var_bound(bv, v, k, r); m_bounds[v].push_back(b); updt_unassigned_bounds(v, +1); m_bounds_trail.push_back(v); @@ -1000,7 +1002,7 @@ public: } lbool get_phase(bool_var v) { - lp_api::bound* b; + api_bound* b; if (!m_bool_var2bound.find(v, b)) { return l_undef; } @@ -2154,7 +2156,7 @@ public: bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv; bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true; m_to_check.push_back(bv); - lp_api::bound* b = nullptr; + api_bound* b = nullptr; TRACE("arith", tout << "propagate: " << bv << "\n";); if (m_bool_var2bound.find(bv, b)) { assert_bound(bv, is_true, *b); @@ -2236,8 +2238,8 @@ public: if (m_bounds.size() <= static_cast(v) || m_unassigned_bounds[v] == 0) return false; - for (lp_api::bound* b : m_bounds[v]) { - if (ctx().get_assignment(b->get_bv()) == l_undef && + for (api_bound* b : m_bounds[v]) { + if (ctx().get_assignment(b->get_lit()) == l_undef && null_literal != is_bound_implied(kind, bval, *b)) { return true; } @@ -2263,8 +2265,8 @@ public: lp_bounds const& bounds = m_bounds[v]; bool first = true; for (unsigned i = 0; i < bounds.size(); ++i) { - lp_api::bound* b = bounds[i]; - if (ctx().get_assignment(b->get_bv()) != l_undef) { + api_bound* b = bounds[i]; + if (ctx().get_assignment(b->get_lit()) != l_undef) { continue; } literal lit = is_bound_implied(be.kind(), be.m_bound, *b); @@ -2387,36 +2389,36 @@ public: } } - literal is_bound_implied(lp::lconstraint_kind k, rational const& value, lp_api::bound const& b) const { + literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const { if ((k == lp::LE || k == lp::LT) && b.get_bound_kind() == lp_api::upper_t && value <= b.get_value()) { TRACE("arith", tout << "v <= value <= b.get_value() => v <= b.get_value() \n";); - return literal(b.get_bv(), false); + return b.get_lit(); } if ((k == lp::GE || k == lp::GT) && b.get_bound_kind() == lp_api::lower_t && b.get_value() <= value) { TRACE("arith", tout << "b.get_value() <= value <= v => b.get_value() <= v \n";); - return literal(b.get_bv(), false); + return b.get_lit(); } if (k == lp::LE && b.get_bound_kind() == lp_api::lower_t && value < b.get_value()) { TRACE("arith", tout << "v <= value < b.get_value() => v < b.get_value()\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::LT && b.get_bound_kind() == lp_api::lower_t && value <= b.get_value()) { TRACE("arith", tout << "v < value <= b.get_value() => v < b.get_value()\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::GE && b.get_bound_kind() == lp_api::upper_t && b.get_value() < value) { TRACE("arith", tout << "b.get_value() < value <= v => b.get_value() < v\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } if (k == lp::GT && b.get_bound_kind() == lp_api::upper_t && b.get_value() <= value) { TRACE("arith", tout << "b.get_value() <= value < v => b.get_value() < v\n";); - return literal(b.get_bv(), true); + return ~b.get_lit(); } return null_literal; } - void mk_bound_axioms(lp_api::bound& b) { + void mk_bound_axioms(api_bound& b) { if (!ctx().is_searching()) { // // NB. We make an assumption that user push calls propagation @@ -2431,13 +2433,13 @@ public: rational const& k1 = b.get_value(); lp_bounds & bounds = m_bounds[v]; - lp_api::bound* end = nullptr; - lp_api::bound* lo_inf = end, *lo_sup = end; - lp_api::bound* hi_inf = end, *hi_sup = end; + api_bound* end = nullptr; + api_bound* lo_inf = end, *lo_sup = end; + api_bound* hi_inf = end, *hi_sup = end; - for (lp_api::bound* other : bounds) { + for (api_bound* other : bounds) { if (other == &b) continue; - if (b.get_bv() == other->get_bv()) continue; + if (b.get_lit() == other->get_lit()) continue; lp_api::bound_kind kind2 = other->get_bound_kind(); rational const& k2 = other->get_value(); if (k1 == k2 && kind1 == kind2) { @@ -2472,9 +2474,9 @@ public: } - void mk_bound_axiom(lp_api::bound& b1, lp_api::bound& b2) { - literal l1(b1.get_bv()); - literal l2(b2.get_bv()); + void mk_bound_axiom(api_bound& b1, api_bound& b2) { + literal l1 = b1.get_lit(); + literal l2 = b2.get_lit(); rational const& k1 = b1.get_value(); rational const& k2 = b2.get_value(); lp_api::bound_kind kind1 = b1.get_bound_kind(); @@ -2572,9 +2574,9 @@ public: iterator lo_inf = begin1, lo_sup = begin1; iterator hi_inf = begin2, hi_sup = begin2; bool flo_inf, fhi_inf, flo_sup, fhi_sup; - ptr_addr_hashtable visited; + ptr_addr_hashtable visited; for (unsigned i = 0; i < atoms.size(); ++i) { - lp_api::bound* a1 = atoms[i]; + api_bound* a1 = atoms[i]; iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf); iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf); iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup); @@ -2597,7 +2599,7 @@ public: } struct compare_bounds { - bool operator()(lp_api::bound* a1, lp_api::bound* a2) const { return a1->get_value() < a2->get_value(); } + bool operator()(api_bound* a1, api_bound* a2) const { return a1->get_value() < a2->get_value(); } }; @@ -2606,14 +2608,14 @@ public: iterator it, iterator end) { for (; it != end; ++it) { - lp_api::bound* a = *it; + api_bound* a = *it; if (a->get_bound_kind() == kind) return it; } return end; } lp_bounds::iterator next_inf( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, @@ -2622,7 +2624,7 @@ public: iterator result = end; found_compatible = false; for (; it != end; ++it) { - lp_api::bound * a2 = *it; + api_bound * a2 = *it; if (a1 == a2) continue; if (a2->get_bound_kind() != kind) continue; rational const & k2(a2->get_value()); @@ -2638,7 +2640,7 @@ public: } lp_bounds::iterator next_sup( - lp_api::bound* a1, + api_bound* a1, lp_api::bound_kind kind, iterator it, iterator end, @@ -2646,7 +2648,7 @@ public: rational const & k1(a1->get_value()); found_compatible = false; for (; it != end; ++it) { - lp_api::bound * a2 = *it; + api_bound * a2 = *it; if (a1 == a2) continue; if (a2->get_bound_kind() != kind) continue; rational const & k2(a2->get_value()); @@ -2660,7 +2662,7 @@ public: void propagate_basic_bounds() { for (auto const& bv : m_to_check) { - lp_api::bound* b = nullptr; + api_bound* b = nullptr; if (m_bool_var2bound.find(bv, b)) { propagate_bound(bv, ctx().get_assignment(bv) == l_true, *b); if (ctx().inconsistent()) break; @@ -2676,7 +2678,7 @@ public: // x <= hi -> x <= hi' // x <= hi -> ~(x >= hi') - void propagate_bound(bool_var bv, bool is_true, lp_api::bound& b) { + void propagate_bound(bool_var bv, bool is_true, api_bound& b) { if (bound_prop_mode::BP_NONE == propagation_mode()) { return; } @@ -2694,8 +2696,8 @@ public: TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";); if (find_glb) { rational glb; - lp_api::bound* lb = nullptr; - for (lp_api::bound* b2 : bounds) { + api_bound* lb = nullptr; + for (api_bound* b2 : bounds) { if (b2 == &b) continue; rational const& val2 = b2->get_value(); if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) { @@ -2705,12 +2707,14 @@ public: } if (!lb) return; bool sign = lb->get_bound_kind() != lp_api::lower_t; - lit2 = literal(lb->get_bv(), sign); + lit2 = lb->get_lit(); + if (sign) + lit2.neg(); } else { rational lub; - lp_api::bound* ub = nullptr; - for (lp_api::bound* b2 : bounds) { + api_bound* ub = nullptr; + for (api_bound* b2 : bounds) { if (b2 == &b) continue; rational const& val2 = b2->get_value(); if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) { @@ -2720,7 +2724,9 @@ public: } if (!ub) return; bool sign = ub->get_bound_kind() != lp_api::upper_t; - lit2 = literal(ub->get_bv(), sign); + lit2 = ub->get_lit(); + if (sign) + lit2.neg(); } TRACE("arith", ctx().display_literal_verbose(tout, lit1); @@ -2739,7 +2745,7 @@ public: svector m_todo_vars; - void add_use_lists(lp_api::bound* b) { + void add_use_lists(api_bound* b) { theory_var v = b->get_var(); lpvar vi = register_theory_var_in_lar_solver(v); if (!lp::tv::is_term(vi)) { @@ -2758,14 +2764,14 @@ public: } else { unsigned w = lp().local_to_external(wi.id()); - m_use_list.reserve(w + 1, ptr_vector()); + m_use_list.reserve(w + 1, ptr_vector()); m_use_list[w].push_back(b); } } } } - void del_use_lists(lp_api::bound* b) { + void del_use_lists(api_bound* b) { theory_var v = b->get_var(); lpvar vi = get_lpvar(v); if (!lp::tv::is_term(vi)) { @@ -2797,14 +2803,14 @@ public: // have been assigned we may know the truth value of the inequality by using simple // bounds propagation. // - void propagate_bound_compound(bool_var bv, bool is_true, lp_api::bound& b) { + void propagate_bound_compound(bool_var bv, bool is_true, api_bound& b) { theory_var v = b.get_var(); TRACE("arith", tout << mk_pp(get_owner(v), m) << "\n";); if (static_cast(v) >= m_use_list.size()) { return; } for (auto const& vb : m_use_list[v]) { - if (ctx().get_assignment(vb->get_bv()) != l_undef) { + if (ctx().get_assignment(vb->get_lit()) != l_undef) { TRACE("arith_verbose", display_bound(tout << "assigned ", *vb) << "\n";); continue; } @@ -2815,18 +2821,18 @@ public: literal lit = null_literal; if (lp_api::lower_t == vb->get_bound_kind()) { if (get_glb(*vb, r) && r >= vb->get_value()) { // vb is assigned true - lit = literal(vb->get_bv(), false); + lit = vb->get_lit(); } else if (get_lub(*vb, r) && r < vb->get_value()) { // vb is assigned false - lit = literal(vb->get_bv(), true); + lit = ~vb->get_lit(); } } else { if (get_glb(*vb, r) && r > vb->get_value()) { // VB <= value < val(VB) - lit = literal(vb->get_bv(), true); + lit = ~vb->get_lit(); } else if (get_lub(*vb, r) && r <= vb->get_value()) { // val(VB) <= value - lit = literal(vb->get_bv(), false); + lit = vb->get_lit(); } } @@ -2846,19 +2852,19 @@ public: } } - bool get_lub(lp_api::bound const& b, inf_rational& lub) { + bool get_lub(api_bound const& b, inf_rational& lub) { return get_bound(b, lub, true); } - bool get_glb(lp_api::bound const& b, inf_rational& glb) { + bool get_glb(api_bound const& b, inf_rational& glb) { return get_bound(b, glb, false); } - std::ostream& display_bound(std::ostream& out, lp_api::bound const& b) { - return out << mk_pp(ctx().bool_var2expr(b.get_bv()), m); + std::ostream& display_bound(std::ostream& out, api_bound const& b) { + return out << mk_pp(ctx().bool_var2expr(b.get_lit().var()), m); } - bool get_bound(lp_api::bound const& b, inf_rational& r, bool is_lub) { + bool get_bound(api_bound const& b, inf_rational& r, bool is_lub) { reset_evidence(); r.reset(); theory_var v = b.get_var(); @@ -2908,7 +2914,7 @@ public: return lp::EQ; } - void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) { + void assert_bound(bool_var bv, bool is_true, api_bound& b) { TRACE("arith", tout << b << "\n";); lp::constraint_index ci = b.get_constraint(is_true); lp().activate(ci); @@ -2932,7 +2938,7 @@ public: #endif } - lp_api::bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) { + api_bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) { scoped_internalize_state st(*this); st.vars().push_back(v); st.coeffs().push_back(rational::one()); @@ -2955,7 +2961,7 @@ public: add_ineq_constraint(cT, literal(bv, false)); add_ineq_constraint(cF, literal(bv, true)); - return alloc(lp_api::bound, bv, v, vi, v_is_int, bound, bk, cT, cF); + return alloc(api_bound, literal(bv, false), v, vi, v_is_int, bound, bk, cT, cF); } // @@ -2969,7 +2975,7 @@ public: vector m_lower_terms; vector m_upper_terms; - void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) { + void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value) { if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) { fixed_var_eh(b.get_var(), value); } @@ -3680,7 +3686,7 @@ public: // ctx().set_enode_flag(bv, true); lp_api::bound_kind bkind = lp_api::bound_kind::lower_t; if (is_strict) bkind = lp_api::bound_kind::upper_t; - lp_api::bound* a = mk_var_bound(bv, v, bkind, r); + api_bound* a = mk_var_bound(bv, v, bkind, r); mk_bound_axioms(*a); updt_unassigned_bounds(v, +1); m_bounds[v].push_back(a); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 17875f80a..2dc7a07a1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2022,7 +2022,7 @@ app* theory_seq::mk_value(app* e) { if (is_var(result)) { SASSERT(m_factory); expr_ref val(m); - val = m_factory->get_some_value(m.get_sort(result)); + val = m_factory->get_fresh_value(m.get_sort(result)); if (val) { result = val; } diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index c52c1618a..3b7a9b3e9 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -315,6 +315,8 @@ public: void set(unsigned idx, T * n) { super::set(idx, n); } + void setx(unsigned idx, T* n) { super::reserve(idx + 1); super::set(idx, n); } + // enable abuse: ref_vector & set(ref_vector const& other) { if (this != &other) {