diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 9e92195d4..f46f32a1a 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -9,6 +9,7 @@ Version 4.next - polysat - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. + - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. Version 4.12.3 ============== diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 9df3ff001..7a4a03a27 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(ast act_cache.cpp arith_decl_plugin.cpp array_decl_plugin.cpp + array_peq.cpp ast.cpp ast_ll_pp.cpp ast_lt.cpp diff --git a/src/ast/array_peq.cpp b/src/ast/array_peq.cpp new file mode 100644 index 000000000..9f4f1b10d --- /dev/null +++ b/src/ast/array_peq.cpp @@ -0,0 +1,107 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + array_peq.cpp + +Abstract: + + Partial equality for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + Hari Govind V K + +Revision History: + +--*/ +#include "ast/array_peq.h" + +#define PARTIAL_EQ "!partial_eq" +bool is_partial_eq(const func_decl *f) { + SASSERT(f); + return f->get_name() == PARTIAL_EQ; +} + +bool is_partial_eq(const app *a) { + SASSERT(a); + return is_partial_eq(a->get_decl()); +} + +app_ref mk_peq(expr *e0, expr *e1, vector const &indices, + ast_manager &m) { + peq p(e0, e1, indices, m); + return p.mk_peq(); +} + +app_ref peq::mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs) { + if (!m_eq) { + expr_ref lhs(m_lhs, m), rhs(m_rhs, m); + if (!stores_on_rhs) { std::swap(lhs, rhs); } + // lhs = (...(store (store rhs i0 v0) i1 v1)...) + sort *val_sort = get_array_range(lhs->get_sort()); + for (expr_ref_vector const &diff : m_diff_indices) { + ptr_vector store_args; + store_args.push_back(rhs); + store_args.append(diff.size(), diff.data()); + app_ref val(m.mk_fresh_const("diff", val_sort), m); + store_args.push_back(val); + aux_consts.push_back(val); + rhs = m_arr_u.mk_store(store_args); + } + m_eq = m.mk_eq(lhs, rhs); + } + return m_eq; +} + +app_ref peq::mk_peq() { + if (!m_peq) { + ptr_vector args; + args.push_back(m_lhs); + args.push_back(m_rhs); + for (auto const &v : m_diff_indices) { + args.append(v.size(), v.data()); + } + m_peq = m.mk_app(m_decl, args.size(), args.data()); + } + return m_peq; +} + +peq::peq(expr *lhs, expr *rhs, vector const &diff_indices, + ast_manager &m) + : m(m), m_lhs(lhs, m), m_rhs(rhs, m), m_diff_indices(diff_indices), + m_decl(m), m_peq(m), m_eq(m), m_arr_u(m) { + SASSERT(m_arr_u.is_array(lhs)); + SASSERT(m_arr_u.is_array(rhs)); + SASSERT(lhs->get_sort() == rhs->get_sort()); + ptr_vector sorts; + sorts.push_back(m_lhs->get_sort()); + sorts.push_back(m_rhs->get_sort()); + + for (auto const &v : diff_indices) { + SASSERT(v.size() == get_array_arity(m_lhs->get_sort())); + for (expr *e : v) sorts.push_back(e->get_sort()); + } + m_decl = m.mk_func_decl(symbol(PARTIAL_EQ), sorts.size(), sorts.data(), + m.mk_bool_sort()); +} + +peq::peq(app *p, ast_manager &m) + : m(m), m_lhs(p->get_arg(0), m), m_rhs(p->get_arg(1), m), + m_decl(p->get_decl(), m), m_peq(p, m), m_eq(m), m_arr_u(m), + m_name(symbol(PARTIAL_EQ)) { + SASSERT(is_partial_eq(p)); + + SASSERT(m_arr_u.is_array(m_lhs)); + SASSERT(m_arr_u.is_array(m_rhs)); + SASSERT(m_lhs->get_sort() == m_rhs->get_sort()); + unsigned arity = get_array_arity(m_lhs->get_sort()); + for (unsigned i = 2; i < p->get_num_args(); i += arity) { + SASSERT(arity + i <= p->get_num_args()); + expr_ref_vector vec(m); + vec.append(arity, p->get_args() + i); + m_diff_indices.push_back(std::move(vec)); + } +} diff --git a/src/ast/array_peq.h b/src/ast/array_peq.h new file mode 100644 index 000000000..9e71791c1 --- /dev/null +++ b/src/ast/array_peq.h @@ -0,0 +1,91 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + array_peq.h + +Abstract: + + Partial equality for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + Hari Govind V K + +Revision History: + +--*/ +#pragma once + +#include "ast/array_decl_plugin.h" +#include "ast/ast.h" + +/** + * \brief utility class for partial equalities + * + * A partial equality (a ==I b), for two arrays a, b and a finite set of indices + * I holds iff (forall i :: i \not\in I => a[i] == b[i]). In other words, peq is + * a restricted form of the extensionality axiom + * + * Using this class, we denote (a =I b) as f(a,b,i0,i1,...), + * where f is an uninterpreted predicate with the name PARTIAL_EQ and + * I = {i0,i1,...} + */ + +class peq { + ast_manager &m; + expr_ref m_lhs; + expr_ref m_rhs; + vector m_diff_indices; + func_decl_ref m_decl; // the partial equality declaration + app_ref m_peq; // partial equality application + app_ref m_eq; // equivalent std equality using def. of partial eq + array_util m_arr_u; + symbol m_name; + + public: + peq(app *p, ast_manager &m); + + peq(expr *lhs, expr *rhs, vector const &diff_indices, + ast_manager &m); + + expr_ref lhs() { return m_lhs; } + + expr_ref rhs() { return m_rhs; } + + void get_diff_indices(vector &result) { + result.append(m_diff_indices); + } + + /** Convert peq into a peq expression */ + app_ref mk_peq(); + + /** Convert peq into an equality + + For peq of the form (a =I b) returns (a = b[i0 := v0, i1 := v1, ...]) + where i0, i1 \in I, and v0, v1 are fresh skolem constants + + Skolems are returned in aux_consts + + The left and right hand arguments are reversed when stores_on_rhs is + false + */ + app_ref mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs = true); +}; + +/** + * mk (e0 ==indices e1) + * + * result has stores if either e0 or e1 or an index term has stores + */ +app_ref mk_peq(expr *e0, expr *e1, vector const &indices, + ast_manager &m); + +bool is_partial_eq(const func_decl *f); + +bool is_partial_eq(const app *a); + +inline bool is_peq(const func_decl *f) { return is_partial_eq(f); } +inline bool is_peq(const app *a) { return is_partial_eq(a); } diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index e580eb82d..228ba9914 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -24,6 +24,7 @@ Notes: #include "ast/rewriter/var_subst.h" #include "params/array_rewriter_params.hpp" #include "util/util.h" +#include "ast/array_peq.h" void array_rewriter::updt_params(params_ref const & _p) { array_rewriter_params p(_p); @@ -40,8 +41,48 @@ void array_rewriter::get_param_descrs(param_descrs & r) { } br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + br_status st = BR_FAILED; + + // BEGIN: rewrite rules for PEQs + if (is_partial_eq(f)) { + SASSERT(num_args >= 2); + expr *e0, *e1; + e0 = args[0]; + e1 = args[1]; + + expr_ref a(m()), val(m()); + expr_ref_vector vindex(m()); + + if (e0 == e1) { + // t peq t --> true + result = m().mk_true(); + st = BR_DONE; + } + else if (m_util.is_store_ext(e0, a, vindex, val)) { + if (num_args == 2 && a == e1) { + // (a[i := x] peq_{\emptyset} a) ---> a[i] == x + mk_select(vindex.size(), vindex.data(), result); + result = m().mk_eq(result, val); + st = BR_REWRITE_FULL; + } + else if (a == e1 && vindex.size() == num_args + 2) { + // a [i: = x] peq_{i} a -- > true + bool all_eq = true; + for (unsigned i = 0, sz = vindex.size(); all_eq && i < sz; + ++i) { + all_eq &= vindex.get(i) == args[2+i]; + } + if (all_eq) { + result = m().mk_true(); + st = BR_DONE; + } + } + } + return st; + } + // END: rewrite rules for PEQs + SASSERT(f->get_family_id() == get_fid()); - br_status st; switch (f->get_decl_kind()) { case OP_SELECT: st = mk_select_core(num_args, args, result); diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp index ba0155e97..001b697e4 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -21,7 +21,8 @@ Notes: br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); switch(f->get_decl_kind()) { - case OP_DT_CONSTRUCTOR: return BR_FAILED; + case OP_DT_CONSTRUCTOR: + return BR_FAILED; case OP_DT_RECOGNISER: SASSERT(num_args == 1); result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index d4e302a5d..18b335ecb 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -39,6 +39,7 @@ Notes: #include "ast/ast_util.h" #include "ast/well_sorted.h" #include "ast/for_each_expr.h" +#include "ast/array_peq.h" namespace { struct th_rewriter_cfg : public default_rewriter_cfg { @@ -644,6 +645,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg { else st = pull_ite(result); } + if (st == BR_FAILED && f->get_family_id() == null_family_id && is_partial_eq(f)) { + st = m_ar_rw.mk_app_core(f, num, args, result); + } + CTRACE("th_rewriter_step", st != BR_FAILED, tout << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index b18d43528..c8f5deb7d 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -16,6 +16,7 @@ Notes: --*/ #include +#include "ast/ast.h" #include "cmd_context/cmd_context.h" #include "cmd_context/cmd_util.h" #include "ast/rewriter/rewriter.h" @@ -34,7 +35,9 @@ Notes: #include "qe/qe_mbp.h" #include "qe/qe_mbi.h" #include "qe/mbp/mbp_term_graph.h" - +#include "qe/mbp/mbp_qel.h" +#include "qe/lite/qe_lite_tactic.h" +#include "qe/lite/qel.h" BINARY_SYM_CMD(get_quantifier_body_cmd, "dbg-get-qbody", @@ -369,7 +372,7 @@ public: } vars.push_back(to_app(v)); } - qe::mbproj mbp(m); + qe::mbproj mbp(m, gparams::get_module("smt")); expr_ref fml(m_fml, m); mbp.spacer(vars, *mdl.get(), fml); ctx.regular_stream() << fml << "\n"; @@ -572,8 +575,192 @@ public: }; +class mbp_qel_cmd : public cmd { + unsigned m_arg_index; + ptr_vector m_lits; + ptr_vector m_vars; -void install_dbg_cmds(cmd_context & ctx) { + public: + mbp_qel_cmd() : cmd("mbp-qel"){}; + char const *get_usage() const override { return "(exprs) (vars)"; } + char const *get_descr(cmd_context &ctx) const override { + return "Model based projection using e-graphs"; + } + unsigned get_arity() const override { return 2; } + cmd_arg_kind next_arg_kind(cmd_context &ctx) const override { + return CPK_EXPR_LIST; + } + void set_next_arg(cmd_context &ctx, unsigned num, + expr *const *args) override { + if (m_arg_index == 0) { + m_lits.append(num, args); + m_arg_index = 1; + } + else { m_vars.append(num, args); } + } + void prepare(cmd_context &ctx) override { + m_arg_index = 0; + m_lits.reset(); + m_vars.reset(); + } + void execute(cmd_context &ctx) override { + ast_manager &m = ctx.m(); + app_ref_vector vars(m); + expr_ref fml(m); + expr_ref_vector lits(m); + for (expr *v : m_vars) vars.push_back(to_app(v)); + for (expr *e : m_lits) lits.push_back(e); + fml = mk_and(lits); + solver_factory &sf = ctx.get_solver_factory(); + params_ref pa; + solver_ref s = sf(m, pa, false, true, true, symbol::null); + s->assert_expr(fml); + lbool r = s->check_sat(); + if (r != l_true) return; + model_ref mdl; + s->get_model(mdl); + mbp::mbp_qel mbptg(m, pa); + mbptg(vars, fml, *mdl.get()); + + ctx.regular_stream() << "------------------------------ " << std::endl; + ctx.regular_stream() << "Orig tg: " << mk_and(lits) << std::endl; + ctx.regular_stream() << "To elim: "; + for (expr *v : m_vars) { + ctx.regular_stream() << to_app(v)->get_decl()->get_name() << " "; + } + ctx.regular_stream() << std::endl; + ctx.regular_stream() << "output " << fml << std::endl; + } +}; + +class qel_cmd : public cmd { + unsigned m_arg_index; + ptr_vector m_lits; + ptr_vector m_vars; + + public: + qel_cmd() : cmd("qel"){}; + char const *get_usage() const override { return "(lits) (vars)"; } + char const *get_descr(cmd_context &ctx) const override { + return "QE lite over e-graphs"; + } + unsigned get_arity() const override { return 2; } + cmd_arg_kind next_arg_kind(cmd_context &ctx) const override { + if (m_arg_index == 0) return CPK_EXPR_LIST; + return CPK_FUNC_DECL_LIST; + } + void set_next_arg(cmd_context &ctx, unsigned num, + expr *const *args) override { + m_lits.append(num, args); + m_arg_index = 1; + } + void set_next_arg(cmd_context &ctx, unsigned num, + func_decl *const *ts) override { + m_vars.append(num, ts); + } + void prepare(cmd_context &ctx) override { + m_arg_index = 0; + m_lits.reset(); + m_vars.reset(); + } + void execute(cmd_context &ctx) override { + ast_manager &m = ctx.m(); + func_decl_ref_vector vars(m); + app_ref_vector vars_apps(m); + expr_ref_vector lits(m); + + ctx.regular_stream() << "------------------------------ " << std::endl; + + for (func_decl *v : m_vars) { + vars.push_back(v); + vars_apps.push_back(m.mk_const(v)); + } + for (expr *e : m_lits) lits.push_back(e); + + expr_ref fml(m.mk_and(lits), m); + ctx.regular_stream() << "[tg] Before: " << fml << std::endl + << "[tg] Vars: "; + for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " "; + + ctx.regular_stream() << std::endl; + + params_ref pa; + + // the following is the same code as in qe_mbp in spacer + qel qe(m, pa); + qe(vars_apps, fml); + ctx.regular_stream() << "[tg] After: " << fml << std::endl + << "[tg] Vars: "; + for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " "; + + ctx.regular_stream() << std::endl; + } +}; + +class qe_lite_cmd : public cmd { + unsigned m_arg_index; + ptr_vector m_lits; + ptr_vector m_vars; + + public: + qe_lite_cmd() : cmd("qe-lite"){}; + char const *get_usage() const override { return "(lits) (vars)"; } + char const *get_descr(cmd_context &ctx) const override { + return "QE lite over e-graphs"; + } + unsigned get_arity() const override { return 2; } + cmd_arg_kind next_arg_kind(cmd_context &ctx) const override { + if (m_arg_index == 0) return CPK_EXPR_LIST; + return CPK_FUNC_DECL_LIST; + } + void set_next_arg(cmd_context &ctx, unsigned num, + expr *const *args) override { + m_lits.append(num, args); + m_arg_index = 1; + } + void set_next_arg(cmd_context &ctx, unsigned num, + func_decl *const *ts) override { + m_vars.append(num, ts); + } + void prepare(cmd_context &ctx) override { + m_arg_index = 0; + m_lits.reset(); + m_vars.reset(); + } + void execute(cmd_context &ctx) override { + ast_manager &m = ctx.m(); + func_decl_ref_vector vars(m); + app_ref_vector vars_apps(m); + expr_ref_vector lits(m); + + ctx.regular_stream() << "------------------------------ " << std::endl; + + for (func_decl *v : m_vars) { + vars.push_back(v); + vars_apps.push_back(m.mk_const(v)); + } + for (expr *e : m_lits) lits.push_back(e); + + expr_ref fml(m.mk_and(lits), m); + ctx.regular_stream() << "[der] Before: " << fml << std::endl + << "[der] Vars: "; + for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " "; + + ctx.regular_stream() << std::endl; + + params_ref pa; + // the following is the same code as in qe_mbp in spacer + qe_lite qe(m, pa, false); + qe(vars_apps, fml); + ctx.regular_stream() << "[der] After: " << fml << std::endl + << "[der] Vars: "; + for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " "; + + ctx.regular_stream() << std::endl; + } +}; + +void install_dbg_cmds(cmd_context &ctx) { ctx.insert(alloc(print_dimacs_cmd)); ctx.insert(alloc(get_quantifier_body_cmd)); ctx.insert(alloc(set_cmd)); @@ -598,7 +785,10 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(set_next_id)); ctx.insert(alloc(get_interpolant_cmd)); ctx.insert(alloc(mbp_cmd)); + ctx.insert(alloc(mbp_qel_cmd)); ctx.insert(alloc(mbi_cmd)); ctx.insert(alloc(euf_project_cmd)); ctx.insert(alloc(eufi_cmd)); + ctx.insert(alloc(qel_cmd)); + ctx.insert(alloc(qe_lite_cmd)); } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 5523326f4..c0a9d7e6f 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -73,7 +73,7 @@ namespace spacer { // the current step needs to be interpolated: expr* fact = m.get_fact(pf); // if we trust the current step and we are able to use it - if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || spacer::is_literal(m, fact))) { + if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || spacer::is_literal(m, fact)) && !spacer::contains_defaults(fact, m)) { // just add it to the core m_ctx.add_lemma_to_core(fact); } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 4e1da5770..3959bd655 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -34,6 +34,7 @@ Notes: #include "ast/ast_pp.h" #include "ast/bv_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "ast/expr_functors.h" #include "ast/for_each_expr.h" #include "ast/occurs.h" #include "ast/rewriter/bool_rewriter.h" @@ -51,7 +52,7 @@ Notes: #include "model/model_smt2_pp.h" #include "smt/params/smt_params.h" -#include "qe/lite/qe_lite_tactic.h" +#include "qe/lite/qel.h" #include "qe/mbp/mbp_plugin.h" #include "qe/mbp/mbp_term_graph.h" #include "qe/qe_mbp.h" @@ -69,6 +70,21 @@ Notes: namespace spacer { +class contains_def_pred : public i_expr_pred { + array_util m_autil; + public: + contains_def_pred(ast_manager& m): m_autil(m) {} + bool operator()(expr* e) override { + return m_autil.is_default(e); + } +}; + +bool contains_defaults(expr *fml, ast_manager &m) { + contains_def_pred pred(m); + check_pred check(pred, m, false); + return check(fml); +} + bool is_clause(ast_manager &m, expr *n) { if (spacer::is_literal(m, n)) return true; if (m.is_or(n)) { @@ -173,7 +189,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, while (true) { params_ref p; - qe_lite qe(m, p, false); + qel qe(m, p); qe(vars, fml); rw(fml); diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index dbc3083a2..272c6cf30 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -121,6 +121,7 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars); void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml); bool contains_selects(expr *fml, ast_manager &m); +bool contains_defaults(expr *fml, ast_manager &m); void get_select_indices(expr *fml, app_ref_vector &indices); void find_decls(expr *fml, app_ref_vector &decls, std::string &prefix); diff --git a/src/qe/lite/CMakeLists.txt b/src/qe/lite/CMakeLists.txt index fc942d4ae..9b9f5a45a 100644 --- a/src/qe/lite/CMakeLists.txt +++ b/src/qe/lite/CMakeLists.txt @@ -1,9 +1,11 @@ z3_add_component(qe_lite SOURCES qe_lite_tactic.cpp + qel.cpp COMPONENT_DEPENDENCIES tactic mbp TACTIC_HEADERS qe_lite_tactic.h + qel.h ) diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp index 32d11786c..03ebc8c4e 100644 --- a/src/qe/lite/qe_lite_tactic.cpp +++ b/src/qe/lite/qe_lite_tactic.cpp @@ -487,7 +487,7 @@ namespace qel { ptr_vector vs; expr_ref_vector ts(m); expr_ref t(m); - if (is_var_def(is_exists, args[i], vs, ts)) { + if (is_var_def(is_exists, args[i], vs, ts)) { // vs is the variable, ts is the definition for (unsigned j = 0; j < vs.size(); ++j) { var* v = vs[j]; t = ts.get(j); @@ -2376,7 +2376,7 @@ public: m_array_der.set_is_variable_proc(is_var); m_der(fmls); m_fm(fmls); - // AG: disalble m_array_der() since it interferes with other array handling + // AG: disable m_array_der() since it interferes with other array handling if (m_use_array_der) m_array_der(fmls); TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); } @@ -2392,7 +2392,7 @@ qe_lite::~qe_lite() { } void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) { - (*m_impl)(vars, fml); + (*m_impl)(vars, fml); } diff --git a/src/qe/lite/qe_lite_tactic.h b/src/qe/lite/qe_lite_tactic.h index 07ce60f35..e45c6f752 100644 --- a/src/qe/lite/qe_lite_tactic.h +++ b/src/qe/lite/qe_lite_tactic.h @@ -30,6 +30,7 @@ class tactic; class qe_lite { class impl; impl * m_impl; + public: /** use_array_der controls whether equalities over array reads are simplified diff --git a/src/qe/lite/qel.cpp b/src/qe/lite/qel.cpp new file mode 100644 index 000000000..583f51cc9 --- /dev/null +++ b/src/qe/lite/qel.cpp @@ -0,0 +1,54 @@ +/*++ + + Module Name: + + qel.cpp + +Abstract: + Light weight quantifier elimination (QEL) based on term graph. + + The implementation is based on the following paper: + + Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel: + Fast Approximations of Quantifier Elimination. Computer-Aided Verification + (CAV). 2023. URL: https://arxiv.org/abs/2306.10009 + +Author: + + Hari Govind V K (hgvk94) + Isabel Garcia (igcontreras) + +Revision History: + + +--*/ +#include "qe/lite/qel.h" +#include "qe/mbp/mbp_term_graph.h" + +class qel::impl { + private: + ast_manager &m; + + public: + impl(ast_manager &m, params_ref const &p) : m(m) {} + + void operator()(app_ref_vector &vars, expr_ref &fml) { + if (vars.empty()) return; + + mbp::term_graph tg(m); + tg.set_vars(vars); + + expr_ref_vector lits(m); + flatten_and(fml, lits); + tg.add_lits(lits); + tg.qel(vars, fml); + } +}; + +qel::qel(ast_manager &m, params_ref const &p) { m_impl = alloc(impl, m, p); } + +qel::~qel() { dealloc(m_impl); } + +void qel::operator()(app_ref_vector &vars, expr_ref &fml) { + (*m_impl)(vars, fml); +} diff --git a/src/qe/lite/qel.h b/src/qe/lite/qel.h new file mode 100644 index 000000000..9db6a32b4 --- /dev/null +++ b/src/qe/lite/qel.h @@ -0,0 +1,49 @@ +/*++ + + Module Name: + + qel.h + +Abstract: + + Light weight quantifier elimination (QEL) based on term graph. + + The implementation is based on the following paper: + + Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel: + Fast Approximations of Quantifier Elimination. Computer-Aided Verification + (CAV). 2023. URL: https://arxiv.org/abs/2306.10009 + +Author: + + Hari Govind V K (hgvk94) + Isabel Garcia (igcontreras) + +Revision History: + + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "ast/ast_util.h" +#include "util/params.h" +#include "util/uint_set.h" + +class qel { + class impl; + impl *m_impl; + + public: + qel(ast_manager &m, params_ref const &p); + + ~qel(); + + /** + \brief Applies light-weight elimination of `vars` provided as vector + of expressions to the cube `fml`. Returns the updated formula and updated + set of variables that were not eliminated. + */ + void operator()(app_ref_vector &vars, expr_ref &fml); +}; diff --git a/src/qe/mbp/CMakeLists.txt b/src/qe/mbp/CMakeLists.txt index 69d5dfd20..a5c7e7702 100644 --- a/src/qe/mbp/CMakeLists.txt +++ b/src/qe/mbp/CMakeLists.txt @@ -2,7 +2,12 @@ z3_add_component(mbp SOURCES mbp_arith.cpp mbp_arrays.cpp + mbp_arrays_tg.cpp + mbp_basic_tg.cpp mbp_datatypes.cpp + mbp_dt_tg.cpp + mbp_qel.cpp + mbp_qel_util.cpp mbp_plugin.cpp mbp_solve_plugin.cpp mbp_term_graph.cpp diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 0f4c805b7..bf3ad08ed 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -17,7 +17,6 @@ Revision History: --*/ - #include "util/lbool.h" #include "ast/rewriter/rewriter_def.h" #include "ast/expr_functors.h" @@ -26,134 +25,11 @@ Revision History: #include "ast/rewriter/th_rewriter.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" +#include "ast/array_peq.h" #include "model/model_evaluator.h" #include "qe/mbp/mbp_arrays.h" #include "qe/mbp/mbp_term_graph.h" - -namespace { - bool is_partial_eq (app* a); - - /** - * \brief utility class for partial equalities - * - * A partial equality (a ==I b), for two arrays a,b and a finite set of indices I holds - * iff (Forall i. i \not\in I => a[i] == b[i]); in other words, it is a - * restricted form of the extensionality axiom - * - * using this class, we denote (a =I b) as f(a,b,i0,i1,...) - * where f is an uninterpreted predicate with name PARTIAL_EQ and - * I = {i0,i1,...} - */ - - // TBD: make work for arrays with multiple arguments. - class peq { - ast_manager& m; - expr_ref m_lhs; - expr_ref m_rhs; - vector m_diff_indices; - func_decl_ref m_decl; // the partial equality declaration - app_ref m_peq; // partial equality application - app_ref m_eq; // equivalent std equality using def. of partial eq - array_util m_arr_u; - - public: - static const char* PARTIAL_EQ; - - peq (app* p, ast_manager& m): - m (m), - m_lhs (p->get_arg (0), m), - m_rhs (p->get_arg (1), m), - m_decl (p->get_decl (), m), - m_peq (p, m), - m_eq (m), - m_arr_u (m) - { - VERIFY (is_partial_eq (p)); - SASSERT (m_arr_u.is_array (m_lhs) && - m_arr_u.is_array (m_rhs) && - m_lhs->get_sort() == m_rhs->get_sort()); - unsigned arity = get_array_arity(m_lhs->get_sort()); - for (unsigned i = 2; i < p->get_num_args (); i += arity) { - SASSERT(arity + i <= p->get_num_args()); - expr_ref_vector vec(m); - vec.append(arity, p->get_args() + i); - m_diff_indices.push_back (vec); - } - } - - peq (expr* lhs, expr* rhs, vector const& diff_indices, ast_manager& m): - m (m), - m_lhs (lhs, m), - m_rhs (rhs, m), - m_diff_indices (diff_indices), - m_decl (m), - m_peq (m), - m_eq (m), - m_arr_u (m) { - SASSERT (m_arr_u.is_array (lhs) && - m_arr_u.is_array (rhs) && - lhs->get_sort() == rhs->get_sort()); - ptr_vector sorts; - sorts.push_back (m_lhs->get_sort ()); - sorts.push_back (m_rhs->get_sort ()); - for (auto const& v : diff_indices) { - SASSERT(v.size() == get_array_arity(m_lhs->get_sort())); - for (expr* e : v) - sorts.push_back (e->get_sort()); - } - m_decl = m.mk_func_decl (symbol (PARTIAL_EQ), sorts.size (), sorts.data (), m.mk_bool_sort ()); - } - - expr_ref lhs () { return m_lhs; } - - expr_ref rhs () { return m_rhs; } - - void get_diff_indices (vector& result) { result.append(m_diff_indices); } - - app_ref mk_peq () { - if (!m_peq) { - ptr_vector args; - args.push_back (m_lhs); - args.push_back (m_rhs); - for (auto const& v : m_diff_indices) { - args.append (v.size(), v.data()); - } - m_peq = m.mk_app (m_decl, args.size (), args.data ()); - } - return m_peq; - } - - app_ref mk_eq (app_ref_vector& aux_consts, bool stores_on_rhs = true) { - if (!m_eq) { - expr_ref lhs (m_lhs, m), rhs (m_rhs, m); - if (!stores_on_rhs) { - std::swap (lhs, rhs); - } - // lhs = (...(store (store rhs i0 v0) i1 v1)...) - sort* val_sort = get_array_range (lhs->get_sort()); - for (expr_ref_vector const& diff : m_diff_indices) { - ptr_vector store_args; - store_args.push_back (rhs); - store_args.append (diff.size(), diff.data()); - app_ref val(m.mk_fresh_const ("diff", val_sort), m); - store_args.push_back (val); - aux_consts.push_back (val); - rhs = m_arr_u.mk_store (store_args); - } - m_eq = m.mk_eq (lhs, rhs); - } - return m_eq; - } - }; - - const char* peq::PARTIAL_EQ = "!partial_eq"; - - bool is_partial_eq (app* a) { - return a->get_decl ()->get_name () == peq::PARTIAL_EQ; - } -} - namespace mbp { @@ -366,20 +242,10 @@ namespace mbp { } } - /** - * mk (e0 ==indices e1) - * - * result has stores if either e0 or e1 or an index term has stores - */ - app_ref mk_peq (expr* e0, expr* e1, vector const& indices) { - peq p (e0, e1, indices, m); - return p.mk_peq (); - } - void find_subst_term (app* eq) { SASSERT(m.is_eq(eq)); vector empty; - app_ref p_exp = mk_peq (eq->get_arg (0), eq->get_arg (1), empty); + app_ref p_exp = mk_peq (eq->get_arg (0), eq->get_arg (1), empty, m); bool subst_eq_found = false; while (true) { TRACE ("qe", tout << "processing peq:\n" << p_exp << "\n";); @@ -434,7 +300,7 @@ namespace mbp { ); // arr0 ==I arr1 - p_exp = mk_peq (arr0, arr1, I); + p_exp = mk_peq (arr0, arr1, I, m); TRACE ("qe", tout << "new peq:\n"; @@ -445,7 +311,7 @@ namespace mbp { m_idx_lits_v.append (idx_diseq); // arr0 ==I+idx arr1 I.push_back (idxs); - p_exp = mk_peq (arr0, arr1, I); + p_exp = mk_peq (arr0, arr1, I, m); TRACE ("qe", tout << "new peq:\n" << p_exp << "\n"; ); diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp new file mode 100644 index 000000000..8f127819d --- /dev/null +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -0,0 +1,394 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_arrays_tg.cpp + +Abstract: + + Apply rules for model based projection for arrays on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#include "qe/mbp/mbp_arrays_tg.h" +#include "ast/array_decl_plugin.h" +#include "ast/array_peq.h" +#include "qe/mbp/mbp_qel_util.h" +#include "util/obj_hashtable.h" +#include "util/obj_pair_hashtable.h" + +namespace mbp { + +struct mbp_array_tg::impl { + typedef std::pair expr_pair; + ast_manager &m; + array_util m_array_util; + mbp::term_graph &m_tg; + // TODO: cache mdl evaluation eventhough we extend m_mdl + model &m_mdl; + + // set of variables on which to apply MBP rules + obj_hashtable &m_vars_set; + + // variables created in the last iteration of MBP application + app_ref_vector m_new_vars; + + expr_sparse_mark &m_seen; + obj_pair_hashtable m_seenp; + + // apply rules that split on model + bool m_use_mdl; + + // m_has_store.is_marked(t) if t has a subterm store(v) where v is a + // variable to be eliminated + ast_mark m_has_stores; + // variables required for applying rules + vector indices; + expr_ref_vector terms, rdTerms; + + bool has_var(expr *t) { return contains_vars(t, m_vars_set, m); } + + bool has_arr_var(expr *t) { + return contains_vars(t, m_vars_set, m, m_array_util.get_family_id(), + ARRAY_SORT); + } + + bool is_var(expr *t) { return is_uninterp_const(t) && has_var(t); } + + bool is_wr_on_rhs(expr *e) { + return is_app(e) && is_partial_eq(to_app(e)) && + is_wr_on_rhs(to_app(e)->get_arg(0), to_app(e)->get_arg(1)); + } + + bool is_wr_on_rhs(expr *lhs, expr *rhs) { + return (is_arr_write(rhs) && !is_arr_write(lhs)); + } + + bool is_arr_write(expr *t) { + if (!m_array_util.is_store(t)) return false; + return has_var(to_app(t)); + } + + // Returns true if e has a subterm store(v) where v is a variable to be + // eliminated. Assumes that has_store has already been called for + // subexpressions of e + bool has_stores(expr *e) { + if (m_has_stores.is_marked(e)) return true; + if (!is_app(e)) return false; + if (m_array_util.is_store(e) && is_var(to_app(e)->get_arg(0))) { + m_has_stores.mark(e, true); + return true; + } + for (auto c : *(to_app(e))) { + if (m_has_stores.is_marked(c)) { + m_has_stores.mark(e, true); + return true; + } + } + return false; + } + + bool is_rd_wr(expr *t) { + if (!m_array_util.is_select(t)) return false; + return m_array_util.is_store(to_app(t)->get_arg(0)) && + has_stores(to_app(t)->get_arg(0)); + } + + bool is_implicit_peq(expr *e) { + return m.is_eq(e) && + is_implicit_peq(to_app(e)->get_arg(0), to_app(e)->get_arg(1)); + } + + bool is_implicit_peq(expr *lhs, expr *rhs) { + return m_array_util.is_array(lhs) && m_array_util.is_array(rhs) && + (has_var(lhs) || has_var(rhs)); + } + + void mark_seen(expr *t) { m_seen.mark(t); } + bool is_seen(expr *t) { return m_seen.is_marked(t); } + void mark_seen(expr *t1, expr *t2) { m_seenp.insert(expr_pair(t1, t2)); } + bool is_seen(expr *t1, expr *t2) { + return m_seenp.contains(expr_pair(t1, t2)) || + m_seenp.contains(expr_pair(t2, t1)); + } + + impl(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen) + : m(man), m_array_util(m), m_tg(tg), m_mdl(mdl), m_vars_set(vars_set), + m_new_vars(m), m_seen(seen), m_use_mdl(false), terms(m), rdTerms(m) {} + + // create a peq where write terms are preferred on the left hand side + peq mk_wr_peq(expr *e1, expr *e2) { + vector empty; + return mk_wr_peq(e1, e2, empty); + } + + // create a peq where write terms are preferred on the left hand side + peq mk_wr_peq(expr *e1, expr *e2, vector &indices) { + expr *n_lhs = e1, *n_rhs = e2; + if (is_wr_on_rhs(e1, e2)) std::swap(n_lhs, n_rhs); + return peq(n_lhs, n_rhs, indices, m); + } + + // rewrite store(x, j, elem) \peq_{indices} y + // into either j = i && x \peq_{indices} y (for some i in + // indices) or &&_{i \in indices} j \neq i && + // x \peq_{indices, j} y && + // select(y, j) = elem + // rewrite negation !(store(x, j, elem) \peq_{indices} y) into + // into either j = i && !(x \peq_{indices} y) (for some i in + // indices) or &&_{i \in indices} j \neq i && + // !(x \peq_{indices, j} y) && + // or &&_{i \in indices} j \neq i && + // !(select(y, j) = elem) + void elimwreq(peq p, bool is_neg) { + SASSERT(is_arr_write(p.lhs())); + TRACE("mbp_tg", + tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m);); + vector indices; + expr *j = to_app(p.lhs())->get_arg(1); + expr *elem = to_app(p.lhs())->get_arg(2); + bool in = false; + p.get_diff_indices(indices); + expr_ref eq_index(m); + expr_ref_vector deq(m); + for (expr_ref_vector &e : indices) { + for (expr *i : e) { + if (m_mdl.are_equal(j, i)) { + in = true; + // save for later + eq_index = i; + break; + } else + deq.push_back(i); + } + } + if (in) { + SASSERT(m_mdl.are_equal(j, eq_index)); + peq p_new = + mk_wr_peq(to_app(p.lhs())->get_arg(0), p.rhs(), indices); + m_tg.add_eq(j, eq_index); + expr_ref p_new_expr(m); + p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq(); + m_tg.add_lit(p_new_expr); + m_tg.add_eq(p_new_expr, p.mk_peq()); + return; + } + for (expr *d : deq) { m_tg.add_deq(j, d); } + expr_ref_vector setOne(m); + setOne.push_back(j); + indices.push_back(setOne); + peq p_new = mk_wr_peq(to_app(p.lhs())->get_arg(0), p.rhs(), indices); + expr *args[2] = {p.rhs(), j}; + expr_ref rd(m_array_util.mk_select(2, args), m); + if (!is_neg) { + m_tg.add_lit(p_new.mk_peq()); + m_tg.add_eq(rd, elem); + m_tg.add_eq(p.mk_peq(), p_new.mk_peq()); + } else { + SASSERT(m_mdl.is_false(p_new.mk_peq()) || + !m_mdl.are_equal(rd, elem)); + if (m_mdl.is_false(p_new.mk_peq())) { + expr_ref npeq(mk_not(p_new.mk_peq()), m); + m_tg.add_lit(npeq); + m_tg.add_eq(p.mk_peq(), p_new.mk_peq()); + } + if (!m_mdl.are_equal(rd, elem)) { m_tg.add_deq(rd, elem); } + } + } + + // add equality v = rd where v is a fresh variable + void add_rdVar(expr *rd) { + // do not assign new variable if rd is already equal to a value + if (m_tg.has_val_in_class(rd)) return; + TRACE("mbp_tg", tout << "applying add_rdVar on " << expr_ref(rd, m);); + app_ref u = new_var(to_app(rd)->get_sort(), m); + m_new_vars.push_back(u); + m_tg.add_var(u); + m_tg.add_eq(u, rd); + m_mdl.register_decl(u->get_decl(), m_mdl(rd)); + } + + // given a \peq_{indices} t, where a is a variable, merge equivalence class + // of a with store(t, indices, elems) where elems are fresh constants + void elimeq(peq p) { + TRACE("mbp_tg", + tout << "applying elimeq on " << expr_ref(p.mk_peq(), m);); + app_ref_vector aux_consts(m); + expr_ref eq(m); + expr_ref sel(m); + eq = p.mk_eq(aux_consts, true); + vector indices; + p.get_diff_indices(indices); + vector::iterator itr = indices.begin(); + unsigned i = 0; + for (app *a : aux_consts) { + m_new_vars.push_back(a); + m_tg.add_var(a); + auto const &indx = std::next(itr, i); + SASSERT(indx->size() == 1); + expr *args[2] = {to_app(p.lhs()), to_app(indx->get(0))}; + sel = m_array_util.mk_select(2, args); + m_mdl.register_decl(a->get_decl(), m_mdl(sel)); + i++; + } + m_tg.add_lit(eq); + m_tg.add_eq(p.mk_peq(), m.mk_true()); + TRACE("mbp_tg", tout << "added lit " << eq;); + } + + // rewrite select(store(a, i, k), j) into either select(a, j) or k + void elimrdwr(expr *term) { + SASSERT(is_rd_wr(term)); + TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m);); + expr *wr_ind = to_app(to_app(term)->get_arg(0))->get_arg(1); + expr *rd_ind = to_app(term)->get_arg(1); + expr *e; + if (m_mdl.are_equal(wr_ind, rd_ind)) { + m_tg.add_eq(wr_ind, rd_ind); + e = to_app(to_app(term)->get_arg(0))->get_arg(2); + } else { + m_tg.add_deq(wr_ind, rd_ind); + expr *args[2] = {to_app(to_app(term)->get_arg(0))->get_arg(0), + to_app(term)->get_arg(1)}; + e = m_array_util.mk_select(2, args); + } + m_tg.add_eq(term, e); + } + + // iterate through all terms in m_tg and apply all array MBP rules once + // returns true if any rules were applied + bool apply() { + TRACE("mbp_tg", tout << "Iterating over terms of tg";); + indices.reset(); + rdTerms.reset(); + m_new_vars.reset(); + expr_ref e(m), rdEq(m), rdDeq(m); + expr *nt, *term; + bool progress = false, is_neg = false; + + // Not resetting terms because get_terms calls resize on terms + m_tg.get_terms(terms, false); + for (unsigned i = 0; i < terms.size(); i++) { + term = terms.get(i); + SASSERT(!m.is_distinct(term)); + if (m_seen.is_marked(term)) continue; + if (m_tg.is_cgr(term)) continue; + TRACE("mbp_tg", tout << "processing " << expr_ref(term, m);); + if (is_implicit_peq(term)) { + // rewrite array eq as peq + mark_seen(term); + progress = true; + e = mk_wr_peq(to_app(term)->get_arg(0), + to_app(term)->get_arg(1)) + .mk_peq(); + m_tg.add_lit(e); + m_tg.add_eq(term, e); + continue; + } + nt = term; + is_neg = m.is_not(term, nt); + if (is_app(nt) && is_partial_eq(to_app(nt))) { + peq p(to_app(nt), m); + if (m_use_mdl && is_arr_write(p.lhs())) { + mark_seen(nt); + mark_seen(term); + progress = true; + elimwreq(p, is_neg); + continue; + } + if (!m_array_util.is_store(p.lhs()) && has_var(p.lhs())) { + // TODO: don't apply this rule if vars in p.lhs() also + // appear in p.rhs() + mark_seen(p.lhs()); + mark_seen(nt); + mark_seen(term); + progress = true; + elimeq(p); + continue; + } + // eliminate eq when the variable is on the rhs + if (!m_array_util.is_store(p.rhs()) && has_var(p.rhs())) { + mark_seen(p.rhs()); + p.get_diff_indices(indices); + peq p_new = mk_wr_peq(p.rhs(), p.lhs(), indices); + mark_seen(nt); + mark_seen(term); + progress = true; + elimeq(p_new); + continue; + } + } + if (m_use_mdl && is_rd_wr(term)) { + mark_seen(term); + progress = true; + elimrdwr(term); + continue; + } + } + + // iterate over term graph again to collect read terms + // irrespective of whether they have been marked or not + rdTerms.reset(); + for (unsigned i = 0; i < terms.size(); i++) { + term = terms.get(i); + if (m_array_util.is_select(term) && + has_var(to_app(term)->get_arg(0))) { + rdTerms.push_back(term); + if (is_seen(term)) continue; + add_rdVar(term); + mark_seen(term); + } + } + if (!m_use_mdl) return progress; + expr *e1, *e2, *a1, *a2, *i1, *i2; + for (unsigned i = 0; i < rdTerms.size(); i++) { + e1 = rdTerms.get(i); + a1 = to_app(e1)->get_arg(0); + i1 = to_app(e1)->get_arg(1); + for (unsigned j = i + 1; j < rdTerms.size(); j++) { + e2 = rdTerms.get(j); + a2 = to_app(e2)->get_arg(0); + i2 = to_app(e2)->get_arg(1); + if (!is_seen(e1, e2) && a1->get_id() == a2->get_id()) { + mark_seen(e1, e2); + progress = true; + if (m_mdl.are_equal(i1, i2)) { + m_tg.add_eq(i1, i2); + } else { + SASSERT(!m_mdl.are_equal(i1, i2)); + m_tg.add_deq(i1, i2); + } + continue; + } + } + } + return progress; + } +}; + +void mbp_array_tg::use_model() { m_impl->m_use_mdl = true; } +bool mbp_array_tg::apply() { return m_impl->apply(); } +void mbp_array_tg::reset() { + m_impl->m_seen.reset(); + m_impl->m_vars_set.reset(); +} +void mbp_array_tg::get_new_vars(app_ref_vector *&t) { t = &m_impl->m_new_vars; } +family_id mbp_array_tg::get_family_id() const { + return m_impl->m_array_util.get_family_id(); +} +mbp_array_tg::mbp_array_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, + expr_sparse_mark &seen) { + m_impl = alloc(mbp_array_tg::impl, man, tg, mdl, vars_set, seen); +} +mbp_array_tg::~mbp_array_tg() { dealloc(m_impl); } + +} // namespace mbp diff --git a/src/qe/mbp/mbp_arrays_tg.h b/src/qe/mbp/mbp_arrays_tg.h new file mode 100644 index 000000000..0c634bdd0 --- /dev/null +++ b/src/qe/mbp/mbp_arrays_tg.h @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_arrays_tg.h + +Abstract: + + Apply rules for model based projection for arrays on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "qe/mbp/mbp_qel_util.h" +#include "qe/mbp/mbp_term_graph.h" +#include "qe/mbp/mbp_tg_plugins.h" +#include "util/memory_manager.h" +#include "util/obj_hashtable.h" +#include "util/obj_pair_hashtable.h" + +namespace mbp { +class mbp_array_tg : public mbp_tg_plugin { + struct impl; + impl *m_impl; + + public: + mbp_array_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen); + void use_model() override; + void reset(); + // iterate through all terms in m_tg and apply all array MBP rules once + // returns true if any rules were applied + bool apply() override; + ~mbp_array_tg() override; + void get_new_vars(app_ref_vector *&t) override; + family_id get_family_id() const override; +}; +} // namespace mbp diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp new file mode 100644 index 000000000..ee83012a7 --- /dev/null +++ b/src/qe/mbp/mbp_basic_tg.cpp @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_basic_tg.cpp + +Abstract: + + Apply rules for model based projection for basic types, on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#include "qe/mbp/mbp_basic_tg.h" +#include "ast/ast.h" +#include "ast/expr_functors.h" +#include "util/debug.h" +#include "util/memory_manager.h" + +struct mbp_basic_tg::impl { + ast_manager &m; + mbp::term_graph &m_tg; + // TODO: cache mdl evaluation eventhough we extend m_mdl + model &m_mdl; + + // set of variables on which to apply MBP rules + obj_hashtable &m_vars_set; + + // variables created in the last iteration of MBP application + app_ref_vector m_new_vars; + + expr_sparse_mark &m_seen; + + expr_ref_vector terms; + bool m_use_mdl; + + void mark_seen(expr *t) { m_seen.mark(t); } + bool is_seen(expr *t) { return m_seen.is_marked(t); } + + bool apply() { + if (!m_use_mdl) return false; + expr *term, *c, *th, *el; + expr_ref nterm(m); + bool progress = false; + TRACE("mbp_tg", tout << "Iterating over terms of tg";); + // Not resetting terms because get_terms calls resize on terms + m_tg.get_terms(terms, false); + for (unsigned i = 0; i < terms.size(); i++) { + term = terms.get(i); + // Unsupported operators + SASSERT(!m.is_and(term)); + SASSERT(!m.is_or(term)); + SASSERT(!m.is_distinct(term)); + SASSERT(!m.is_implies(term)); + + if (is_seen(term)) continue; + if (m_tg.is_cgr(term)) continue; + if (m.is_ite(term, c, th, el)) { + mark_seen(term); + progress = true; + if (m_mdl.is_true(c)) { + m_tg.add_lit(c); + m_tg.add_eq(term, th); + } else { + if (m.is_not(c)) + nterm = to_app(c)->get_arg(0); + else + nterm = m.mk_not(c); + m_tg.add_lit(nterm); + m_tg.add_eq(term, el); + } + continue; + } + } + return progress; + } + + impl(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen) + : m(man), m_tg(tg), m_mdl(mdl), m_vars_set(vars_set), m_new_vars(m), + m_seen(seen), terms(m), m_use_mdl(false) {} +}; + +bool mbp_basic_tg::apply() { return m_impl->apply(); } +void mbp_basic_tg::use_model() { m_impl->m_use_mdl = true; } +void mbp_basic_tg::get_new_vars(app_ref_vector *&t) { t = &m_impl->m_new_vars; } +family_id mbp_basic_tg::get_family_id() const { + return m_impl->m.get_basic_family_id(); +} +mbp_basic_tg::mbp_basic_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, + expr_sparse_mark &seen) { + m_impl = alloc(mbp_basic_tg::impl, man, tg, mdl, vars_set, seen); +} +mbp_basic_tg::~mbp_basic_tg() { dealloc(m_impl); } diff --git a/src/qe/mbp/mbp_basic_tg.h b/src/qe/mbp/mbp_basic_tg.h new file mode 100644 index 000000000..af7c624c0 --- /dev/null +++ b/src/qe/mbp/mbp_basic_tg.h @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_basic_tg.h + +Abstract: + + Apply rules for model based projection for basic types, on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ +#pragma once + +#include "qe/mbp/mbp_qel_util.h" +#include "qe/mbp/mbp_term_graph.h" +#include "qe/mbp/mbp_tg_plugins.h" +#include "util/obj_hashtable.h" + +class mbp_basic_tg : public mbp_tg_plugin { + struct impl; + impl *m_impl; + + public: + mbp_basic_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen); + // iterate through all terms in m_tg and apply all basic MBP rules once + // returns true if any rules were applied + bool apply() override; + ~mbp_basic_tg() override; + void use_model() override; + void get_new_vars(app_ref_vector *&t) override; + family_id get_family_id() const override; +}; diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp new file mode 100644 index 000000000..b3b24617d --- /dev/null +++ b/src/qe/mbp/mbp_dt_tg.cpp @@ -0,0 +1,202 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_dt_tg.cpp + +Abstract: + + Apply rules for model based projection for datatypes on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ +#include "qe/mbp/mbp_dt_tg.h" +#include "qe/mbp/mbp_qel_util.h" +#include "util/memory_manager.h" + +namespace mbp { + +struct mbp_dt_tg::impl { + ast_manager &m; + datatype_util m_dt_util; + mbp::term_graph &m_tg; + // TODO: cache mdl evaluation eventhough we extend m_mdl + model &m_mdl; + + // set of variables on which to apply MBP rules + obj_hashtable &m_vars_set; + + // variables created in the last iteration of MBP application + app_ref_vector m_new_vars; + + expr_sparse_mark &m_seen; + + expr_ref_vector terms; + bool m_use_mdl; + + void mark_seen(expr *t) { m_seen.mark(t); } + bool is_seen(expr *t) { return m_seen.is_marked(t); } + + bool is_var(expr *t) { return is_uninterp_const(t) && has_var(t); } + + bool has_var(expr *t) { return contains_vars(t, m_vars_set, m); } + + bool is_constructor(expr *t) { + return is_app(t) && m_dt_util.is_constructor(to_app(t)->get_decl()) && + has_var(t); + } + + bool is_constructor_app(expr *e, expr *&cons, expr *&rhs) { + if (!m.is_eq(e, cons, rhs)) return false; + // TODO: does it matter whether vars in cons appear in rhs? + if (is_constructor(cons)) { + return true; + } else if (is_constructor(rhs)) { + cons = rhs; + rhs = to_app(e)->get_arg(0); + return true; + } + return false; + } + + impl(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen) + : m(man), m_dt_util(m), m_tg(tg), m_mdl(mdl), m_vars_set(vars_set), + m_new_vars(m), m_seen(seen), terms(m), m_use_mdl(false) {} + + // rewrite head(x) with y + // and x with list(y, z) + void rm_select(expr *term) { + SASSERT(is_app(term) && + m_dt_util.is_accessor(to_app(term)->get_decl()) && + is_var(to_app(term)->get_arg(0))); + TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m);); + expr *v = to_app(term)->get_arg(0); + expr_ref sel(m); + app_ref u(m); + app_ref_vector new_vars(m); + func_decl *cons = + m_dt_util.get_accessor_constructor(to_app(term)->get_decl()); + ptr_vector const *accessors = + m_dt_util.get_constructor_accessors(cons); + for (unsigned i = 0; i < accessors->size(); i++) { + func_decl *d = accessors->get(i); + sel = m.mk_app(d, v); + u = m_tg.get_const_in_class(sel); + if (u) { + new_vars.push_back(u); + continue; + } + u = new_var(d->get_range(), m); + m_new_vars.push_back(u); + m_tg.add_var(u); + new_vars.push_back(u); + m_tg.add_eq(sel, u); + m_mdl.register_decl(u->get_decl(), m_mdl(sel)); + } + expr_ref new_cons(m.mk_app(cons, new_vars), m); + m_tg.add_eq(v, new_cons); + } + + // rewrite cons(v, u) = x with v = head(x) and u = tail(x) + // where u or v contain variables + void deconstruct_eq(expr *cons, expr *rhs) { + TRACE("mbp_tg", + tout << "applying deconstruct_eq on " << expr_ref(cons, m);); + ptr_vector const *accessors = + m_dt_util.get_constructor_accessors(to_app(cons)->get_decl()); + for (unsigned i = 0; i < accessors->size(); i++) { + expr_ref a(m.mk_app(accessors->get(i), rhs), m); + expr *newRhs = to_app(cons)->get_arg(i); + m_tg.add_eq(a, newRhs); + } + func_decl *is_cons = + m_dt_util.get_constructor_recognizer(to_app(cons)->get_decl()); + expr_ref is(m.mk_app(is_cons, rhs), m); + m_tg.add_lit(is); + } + + // rewrite cons(v, u) != x into one of !cons(x) or v != head(x) or u != + // tail(x) where u or v contain variables + void deconstruct_neq(expr *cons, expr *rhs) { + TRACE("mbp_tg", + tout << "applying deconstruct_neq on " << expr_ref(cons, m);); + ptr_vector const *accessors = + m_dt_util.get_constructor_accessors(to_app(cons)->get_decl()); + func_decl *is_cons = + m_dt_util.get_constructor_recognizer(to_app(cons)->get_decl()); + expr_ref a(m.mk_app(is_cons, rhs), m); + if (m_mdl.is_false(a)) { + expr_ref not_cons(m.mk_not(a), m); + m_tg.add_lit(not_cons); + return; + } + m_tg.add_lit(a); + + for (unsigned i = 0; i < accessors->size(); i++) { + expr_ref a(m.mk_app(accessors->get(i), rhs), m); + expr *newRhs = to_app(cons)->get_arg(i); + if (!m_mdl.are_equal(a, newRhs)) { + m_tg.add_deq(a, newRhs); + break; + } + } + } + + bool apply() { + expr *cons, *rhs, *f, *term; + bool progress = false; + m_new_vars.reset(); + TRACE("mbp_tg", tout << "Iterating over terms of tg";); + // Not resetting terms because get_terms calls resize on terms + m_tg.get_terms(terms, false); + for (unsigned i = 0; i < terms.size(); i++) { + term = terms.get(i); + SASSERT(!m.is_distinct(term)); + if (is_seen(term)) continue; + if (m_tg.is_cgr(term)) continue; + if (is_app(term) && + m_dt_util.is_accessor(to_app(term)->get_decl()) && + is_var(to_app(term)->get_arg(0))) { + mark_seen(term); + progress = true; + rm_select(term); + continue; + } + if (is_constructor_app(term, cons, rhs)) { + mark_seen(term); + progress = true; + deconstruct_eq(cons, rhs); + continue; + } + if (m_use_mdl && m.is_not(term, f) && + is_constructor_app(f, cons, rhs)) { + mark_seen(term); + progress = true; + deconstruct_neq(cons, rhs); + continue; + } + } + return progress; + } +}; + +bool mbp_dt_tg::apply() { return m_impl->apply(); } +mbp_dt_tg::mbp_dt_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen) { + m_impl = alloc(mbp_dt_tg::impl, man, tg, mdl, vars_set, seen); +} +void mbp_dt_tg::use_model() { m_impl->m_use_mdl = true; } +void mbp_dt_tg::get_new_vars(app_ref_vector *&t) { t = &m_impl->m_new_vars; } +family_id mbp_dt_tg::get_family_id() const { + return m_impl->m_dt_util.get_family_id(); +} +mbp_dt_tg::~mbp_dt_tg() { dealloc(m_impl); } + +} // namespace mbp diff --git a/src/qe/mbp/mbp_dt_tg.h b/src/qe/mbp/mbp_dt_tg.h new file mode 100644 index 000000000..8ea0d8e48 --- /dev/null +++ b/src/qe/mbp/mbp_dt_tg.h @@ -0,0 +1,44 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_dt_tg.h + +Abstract: + + Apply rules for model based projection for datatypes on a term graph + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#pragma once + +#include "ast/datatype_decl_plugin.h" +#include "qe/mbp/mbp_qel_util.h" +#include "qe/mbp/mbp_term_graph.h" +#include "qe/mbp/mbp_tg_plugins.h" +#include "util/obj_hashtable.h" + +namespace mbp { +class mbp_dt_tg : public mbp_tg_plugin { + struct impl; + impl *m_impl; + + public: + mbp_dt_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, + obj_hashtable &vars_set, expr_sparse_mark &seen); + // iterate through all terms in m_tg and apply all datatype MBP rules once + // returns true if any rules were applied + bool apply() override; + ~mbp_dt_tg() override; + void use_model() override; + void get_new_vars(app_ref_vector *&t) override; + family_id get_family_id() const override; +}; +} // namespace mbp diff --git a/src/qe/mbp/mbp_qel.cpp b/src/qe/mbp/mbp_qel.cpp new file mode 100644 index 000000000..d50a8c1f6 --- /dev/null +++ b/src/qe/mbp/mbp_qel.cpp @@ -0,0 +1,226 @@ +/*++ + + Module Name: + + mbp_qel.cpp + +Abstract: + + Model Based Projection based on term graph + +Author: + + Hari Govind V K (hgvk94) 2022-07-12 + +Revision History: + + +--*/ +#include "qe/mbp/mbp_qel.h" +#include "ast/array_decl_plugin.h" +#include "ast/array_peq.h" +#include "ast/datatype_decl_plugin.h" +#include "model/model.h" +#include "qe/mbp/mbp_arrays.h" +#include "qe/mbp/mbp_arrays_tg.h" +#include "qe/mbp/mbp_basic_tg.h" +#include "qe/mbp/mbp_dt_tg.h" +#include "qe/mbp/mbp_term_graph.h" +#include "qe/mbp/mbp_tg_plugins.h" +#include "util/obj_hashtable.h" + +namespace mbp { + +class mbp_qel::impl { + private: + ast_manager &m; + array_util m_array_util; + datatype_util m_dt_util; + params_ref m_params; + mbp::term_graph m_tg; + + ptr_vector m_plugins; + + // set of non_basic variables to be projected. MBP rules are applied to + // terms containing these variables + obj_hashtable m_non_basic_vars; + + // Utilities to keep track of which terms have been processed + expr_sparse_mark m_seen; + void mark_seen(expr *t) { m_seen.mark(t); } + bool is_seen(expr *t) { return m_seen.is_marked(t); } + + bool is_non_basic(app *v) { + return m_dt_util.is_datatype(v->get_sort()) || m_array_util.is_array(v); + } + + void add_vars(mbp_tg_plugin *p, app_ref_vector &vars) { + app_ref_vector *new_vars; + p->get_new_vars(new_vars); + for (auto v : *new_vars) { + if (is_non_basic(v)) m_non_basic_vars.insert(v); + vars.push_back(v); + } + } + + // apply all plugins till saturation + void saturate(app_ref_vector &vars) { + bool progress; + do { + progress = false; + for (auto *p : m_plugins) { + if (p->apply()) { + progress = true; + add_vars(p, vars); + } + } + } + while (progress); + } + + void init(app_ref_vector &vars, expr_ref &fml, model &mdl) { + // variables to apply projection rules on + for (auto v : vars) + if (is_non_basic(v)) m_non_basic_vars.insert(v); + + // mark vars as non-ground. + m_tg.add_vars(vars); + // treat eq literals as term in the egraph + m_tg.set_explicit_eq(); + + expr_ref_vector fmls(m); + flatten_and(fml, fmls); + m_tg.add_lits(fmls); + + add_plugin(alloc(mbp_array_tg, m, m_tg, mdl, m_non_basic_vars, m_seen)); + add_plugin(alloc(mbp_dt_tg, m, m_tg, mdl, m_non_basic_vars, m_seen)); + add_plugin(alloc(mbp_basic_tg, m, m_tg, mdl, m_non_basic_vars, m_seen)); + } + + void add_plugin(mbp_tg_plugin *p) { m_plugins.push_back(p); } + + void enable_model_splitting() { + for (auto p : m_plugins) p->use_model(); + } + + mbp_tg_plugin *get_plugin(family_id fid) { + for (auto p : m_plugins) + if (p->get_family_id() == fid) return p; + return nullptr; + } + + public: + impl(ast_manager &m, params_ref const &p) + : m(m), m_array_util(m), m_dt_util(m), m_params(p), m_tg(m) {} + + ~impl() { + std::for_each(m_plugins.begin(), m_plugins.end(), + delete_proc()); + } + + void operator()(app_ref_vector &vars, expr_ref &fml, model &mdl) { + if (vars.empty()) return; + + init(vars, fml, mdl); + // Apply MBP rules till saturation + + // First, apply rules without splitting on model + saturate(vars); + + enable_model_splitting(); + + // Do complete mbp + saturate(vars); + + TRACE("mbp_tg", + tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars;); + TRACE("mbp_tg_verbose", obj_hashtable vars_tmp; + collect_uninterp_consts(mk_and(m_tg.get_lits()), vars_tmp); + for (auto a + : vars_tmp) tout + << mk_pp(a->get_decl(), m) << "\n"; + for (auto b + : m_tg.get_lits()) tout + << expr_ref(b, m) << "\n"; + for (auto a + : vars) tout + << expr_ref(a, m) << " ";); + + // 1. Apply qe_lite to remove all c-ground variables + // 2. Collect all core variables in the output (variables used as array + // indices/values) + // 3. Re-apply qe_lite to remove non-core variables + + // Step 1. + m_tg.qel(vars, fml); + + // Step 2. + // Variables that appear as array indices or values cannot be + // eliminated if they are not c-ground. They are core variables All + // other Array/ADT variables can be eliminated, they are redundant. + obj_hashtable core_vars; + collect_selstore_vars(fml, core_vars, m); + + std::function is_red = [&](app *v) { + if (!m_dt_util.is_datatype(v->get_sort()) && + !m_array_util.is_array(v)) + return false; + return !core_vars.contains(v); + }; + expr_sparse_mark red_vars; + for (auto v : vars) + if (is_red(v)) red_vars.mark(v); + CTRACE("mbp_tg", !core_vars.empty(), tout << "vars not redundant "; + for (auto v + : core_vars) tout + << " " << app_ref(v, m); + tout << "\n";); + + std::function non_core = [&](expr *e) { + if (is_app(e) && is_partial_eq(to_app(e))) return true; + if (m.is_ite(e)) return true; + return red_vars.is_marked(e); + }; + + // Step 3. + m_tg.qel(vars, fml, &non_core); + + CTRACE("mbp_tg", !vars.empty(), + tout << "before substitution " << fml << "\n";); + // for all remaining non-cgr bool, dt, array variables, add v = mdl(v) + expr_sparse_mark s_vars; + for (auto v : vars) { + if (m_dt_util.is_datatype(v->get_sort()) || + m_array_util.is_array(v) || m.is_bool(v)) { + CTRACE("mbp_tg", + m_array_util.is_array(v) || + m_dt_util.is_datatype(v->get_sort()), + tout << "Could not eliminate " << v->get_name() + << "\n";); + s_vars.mark(v); + m_tg.add_eq(v, mdl(v)); + } + } + + std::function substituted = [&](expr *e) { + if (is_app(e) && is_partial_eq(to_app(e))) return true; + if (m.is_ite(e)) return true; + return red_vars.is_marked(e) || s_vars.is_marked(e); + }; + + // remove all substituted variables + m_tg.qel(vars, fml, &substituted); + } +}; + +mbp_qel::mbp_qel(ast_manager &m, params_ref const &p) { + m_impl = alloc(impl, m, p); +} + +mbp_qel::~mbp_qel() { dealloc(m_impl); } + +void mbp_qel::operator()(app_ref_vector &vars, expr_ref &fml, model &mdl) { + (*m_impl)(vars, fml, mdl); +} + +} // namespace mbp diff --git a/src/qe/mbp/mbp_qel.h b/src/qe/mbp/mbp_qel.h new file mode 100644 index 000000000..6246ec01f --- /dev/null +++ b/src/qe/mbp/mbp_qel.h @@ -0,0 +1,41 @@ +/*++ + + Module Name: + + mbp_qel.h + +Abstract: + + Model Based Projection based on term graph + +Author: + + Hari Govind V K (hgvk94) 2022-07-12 + +Revision History: + + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "model/model.h" +#include "util/params.h" + +namespace mbp { +class mbp_qel { + class impl; + impl *m_impl; + + public: + mbp_qel(ast_manager &m, params_ref const &p); + + ~mbp_qel(); + + /** + Do model based projection + */ + void operator()(app_ref_vector &vars, expr_ref &fml, model &mdl); +}; +} // namespace mbp diff --git a/src/qe/mbp/mbp_qel_util.cpp b/src/qe/mbp/mbp_qel_util.cpp new file mode 100644 index 000000000..e6537a1d0 --- /dev/null +++ b/src/qe/mbp/mbp_qel_util.cpp @@ -0,0 +1,110 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_qel_util.h + +Abstract: + + Utility methods for mbp_qel + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#include "qe/mbp/mbp_qel_util.h" +#include "ast/array_decl_plugin.h" +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/expr_functors.h" +#include "ast/for_each_expr.h" +#include "ast/pp.h" + +class check_uninterp_consts : public i_expr_pred { + obj_hashtable const &m_vars; + family_id m_fid; + decl_kind m_decl_kind; + + public: + check_uninterp_consts(obj_hashtable const &vars, ast_manager &man, + family_id fid = null_family_id, + decl_kind dk = null_decl_kind) + : m_vars(vars), m_fid(fid), m_decl_kind(dk) {} + bool operator()(expr *n) override { + return (is_app(n) && is_uninterp_const(n) && + m_vars.contains(to_app(n))) && + ((m_fid == null_family_id || m_decl_kind == null_decl_kind) || + (is_sort_of(to_app(n)->get_sort(), m_fid, m_decl_kind))); + } +}; + +// check if e contains any apps from vars +// if fid and dk are not null, check if the variable is of desired sort +bool contains_vars(expr *e, obj_hashtable const &vars, ast_manager &man, + family_id fid, decl_kind dk) { + check_uninterp_consts pred(vars, man, fid, dk); + check_pred check(pred, man, false); + return check(e); +} + +app_ref new_var(sort *s, ast_manager &m) { + return app_ref(m.mk_fresh_const("mbptg", s), m); +} + +namespace collect_uninterp_consts_ns { +struct proc { + obj_hashtable &m_out; + proc(obj_hashtable &out) : m_out(out) {} + void operator()(expr *n) const {} + void operator()(app *n) { + if (is_uninterp_const(n)) m_out.insert(n); + } +}; +} // namespace collect_uninterp_consts_ns + +// Return all uninterpreted constants of \p q +void collect_uninterp_consts(expr *e, obj_hashtable &out) { + collect_uninterp_consts_ns::proc proc(out); + for_each_expr(proc, e); +} + +namespace collect_selstore_vars_ns { +struct proc { + ast_manager &m; + obj_hashtable &m_vars; + array_util m_array_util; + datatype_util m_dt_util; + proc(obj_hashtable &vars, ast_manager &man) + : m(man), m_vars(vars), m_array_util(m), m_dt_util(m) {} + void operator()(expr *n) const {} + void operator()(app *n) { + if (m_array_util.is_select(n)) { + expr *idx = n->get_arg(1); + if (is_app(idx) && m_dt_util.is_accessor(to_app(idx)->get_decl())) + return; + collect_uninterp_consts(idx, m_vars); + } else if (m_array_util.is_store(n)) { + expr *idx = n->get_arg(1), *elem = n->get_arg(2); + if (!(is_app(idx) && + m_dt_util.is_accessor(to_app(idx)->get_decl()))) + collect_uninterp_consts(idx, m_vars); + if (!(is_app(elem) && + m_dt_util.is_accessor(to_app(elem)->get_decl()))) + collect_uninterp_consts(elem, m_vars); + } + } +}; +} // namespace collect_selstore_vars_ns + +// collect all uninterpreted consts used as array indices or values +void collect_selstore_vars(expr *fml, obj_hashtable &vars, + ast_manager &man) { + collect_selstore_vars_ns::proc proc(vars, man); + quick_for_each_expr(proc, fml); +} diff --git a/src/qe/mbp/mbp_qel_util.h b/src/qe/mbp/mbp_qel_util.h new file mode 100644 index 000000000..dd1a7795a --- /dev/null +++ b/src/qe/mbp/mbp_qel_util.h @@ -0,0 +1,41 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + mbp_qel_util.h + +Abstract: + + Utility methods for mbp_qel + +Author: + + Hari Govind V K (hgvk94) 2023-03-07 + +Revision History: + +--*/ + +#pragma once + +#include "ast/array_decl_plugin.h" +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "ast/pp.h" + +// check if e contains any apps from vars +// if fid and dk are not null, check if the variable is of desired sort +bool contains_vars(expr *e, obj_hashtable const &vars, ast_manager &man, + family_id fid = null_family_id, + decl_kind dk = null_decl_kind); + +app_ref new_var(sort *s, ast_manager &m); + +// Return all uninterpreted constants of \p q +void collect_uninterp_consts(expr *e, obj_hashtable &out); +// collect all uninterpreted consts used as array indices or values +void collect_selstore_vars(expr *fml, obj_hashtable &vars, + ast_manager &man); diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp index d80a3665d..d46a09284 100644 --- a/src/qe/mbp/mbp_solve_plugin.cpp +++ b/src/qe/mbp/mbp_solve_plugin.cpp @@ -248,30 +248,80 @@ namespace mbp { return false; } + // returns `true` if a rewritting happened + bool try_int_mul_solve(expr *atom, bool is_pos, expr_ref &res) { + + if (!is_pos) + return false; // negation of multiplication is not a cube for + // integers + + // we want k*y == x -----> y = x div k && x mod k == 0 + expr *lhs = nullptr, *rhs = nullptr; + if (!m.is_eq(atom, lhs, rhs)) return false; + + if (!a.is_int(lhs)) { return false; } + + if (!a.is_mul(rhs)) { + if (a.is_mul(lhs)) + std::swap(lhs, rhs); + else + return false; // no muls + } + + // of the form v = k*expr + expr *first = nullptr, *second = nullptr; + if (!a.is_mul(rhs, first, second)) return false; + + if (!(is_app(first) && a.plugin().is_value(to_app(first)))) { + if (is_app(second) && a.plugin().is_value(to_app(second))) { + std::swap(first, second); + } else { + return false; + } + } + + if (a.is_zero(first)) { + // SASSERT(a.is_int(lhs)); + res = m.mk_eq(lhs, a.mk_int(0)); + return true; + }; + + // `first` is a value, different from 0 + res = m.mk_and(m.mk_eq(second, a.mk_idiv(lhs, first)), + m.mk_eq(a.mk_int(0), a.mk_mod(lhs, first))); + + return true; + } + expr_ref solve(expr* atom, bool is_pos) override { - expr *e1, *e2; - expr_ref res(atom, m); - if (m.is_eq (atom, e1, e2)) { - expr_ref v(m), t(m); - v = e1; t = e2; - // -- attempt to solve using arithmetic - solve(e1, e2, v, t); - // -- normalize equality - res = mk_eq_core(v, t); - } - else if (a.is_le(atom, e1, e2)) { - mk_le_core(e1, e2, res); - } - else if (a.is_ge(atom, e1, e2)) { - mk_ge_core(e1, e2, res); - } + expr_ref res(atom, m); - // restore negation - if (!is_pos) { - res = mk_not(m, res); - } - return res; + if (try_int_mul_solve(atom, is_pos, res)) return res; + + expr *e1, *e2; + + if (m.is_eq(atom, e1, e2)) { + expr_ref v(m), t(m); + v = e1; + t = e2; + // -- attempt to solve using arithmetic + solve(e1, e2, v, t); + // -- normalize equality + res = mk_eq_core(v, t); + } + else if (a.is_le(atom, e1, e2)) { + mk_le_core(e1, e2, res); + } + else if (a.is_ge(atom, e1, e2)) { + mk_ge_core(e1, e2, res); + } + + // restore negation + if (!is_pos) { + res = mk_not(m, res); + } + return res; } }; diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 624febffd..ee371bdfa 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -12,1291 +12,1811 @@ Abstract: Author: Arie Gurfinkel + Hari Govind V K (hgvk94) + Isabel Garcia (igcontreras) + +Revision History: + + Added implementation of qe_lite using term graph Notes: --*/ -#include "util/util.h" -#include "util/uint_set.h" -#include "util/obj_pair_hashtable.h" +#include "qe/mbp/mbp_term_graph.h" +#include "ast/array_peq.h" +#include "ast/ast.h" #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/for_each_expr.h" #include "ast/occurs.h" #include "ast/rewriter/th_rewriter.h" #include "model/model_evaluator.h" -#include "qe/mbp/mbp_term_graph.h" +#include "qe/mbp/mbp_arrays.h" +#include "util/bit_vector.h" +#include "util/obj_pair_hashtable.h" +#include "util/uint_set.h" +#include "util/util.h" namespace mbp { - static expr_ref mk_neq(ast_manager &m, expr *e1, expr *e2) { - expr *t = nullptr; - // x != !x == true - if ((m.is_not(e1, t) && t == e2) || (m.is_not(e2, t) && t == e1)) - return expr_ref(m.mk_true(), m); - else if (m.are_distinct(e1, e2)) - return expr_ref(m.mk_true(), m); - return expr_ref(m.mk_not(m.mk_eq(e1, e2)), m); - } +static expr_ref mk_neq(ast_manager &m, expr *e1, expr *e2) { + expr *t = nullptr; + // x != !x == true + if ((m.is_not(e1, t) && t == e2) || (m.is_not(e2, t) && t == e1)) + return expr_ref(m.mk_true(), m); + else if (m.are_distinct(e1, e2)) + return expr_ref(m.mk_true(), m); + return expr_ref(m.mk_not(m.mk_eq(e1, e2)), m); +} - namespace { - struct sort_lt_proc { - bool operator()(const expr* a, const expr *b) const { - return a->get_sort()->get_id() < b->get_sort()->get_id(); - } - }; +namespace { +struct sort_lt_proc { // for representatives in model_complete + bool operator()(const expr *a, const expr *b) const { + return a->get_sort()->get_id() < b->get_sort()->get_id(); } +}; +struct mark_all_sub_expr { + expr_sparse_mark &m_mark; + mark_all_sub_expr(expr_sparse_mark &mark) : m_mark(mark) {} + void operator()(var *n) const {} + void operator()(app *n) const { m_mark.mark(n); } + void operator()(quantifier *n) const {} +}; +} // namespace - namespace is_pure_ns { - struct found{}; - struct proc { - is_variable_proc &m_is_var; - proc(is_variable_proc &is_var) : m_is_var(is_var) {} - void operator()(var *n) const {if (m_is_var(n)) throw found();} - void operator()(app const *n) const {if (m_is_var(n)) throw found();} - void operator()(quantifier *n) const {} - }; +namespace is_pure_ns { +struct found {}; +struct proc { + is_variable_proc &m_is_var; + proc(is_variable_proc &is_var) : m_is_var(is_var) {} + void operator()(var *n) const { + if (m_is_var(n)) throw found(); } - - bool is_pure(is_variable_proc &is_var, expr *e) { - try { - is_pure_ns::proc v(is_var); - quick_for_each_expr(v, e); - } - catch (const is_pure_ns::found &) { - return false; - } - return true; + void operator()(app const *n) const { + if (m_is_var(n)) throw found(); } + void operator()(quantifier *n) const {} +}; +} // namespace is_pure_ns - class term { - // -- an app represented by this term - expr_ref m_expr; // NSB: to make usable with exprs - // -- root of the equivalence class - term* m_root; - // -- next element in the equivalence class (cyclic linked list) - term* m_next; +bool is_pure(is_variable_proc &is_var, expr *e) { + try { + is_pure_ns::proc v(is_var); + quick_for_each_expr(v, e); + } catch (const is_pure_ns::found &) { return false; } + return true; +} + +bool term_graph::is_ground(expr *e) { + try { + is_ground_ns::proc v(m_is_var); + quick_for_each_expr(v, e); + } catch (const is_ground_ns::found &) { return false; } + return true; +} + +class term { + // -- an app represented by this term + expr_ref m_expr; // NSB: to make usable with exprs + // -- root of the equivalence class + term *m_root; + // -- representative of the equivalence class + term *m_repr; + // -- next element in the equivalence class (cyclic linked list) + term *m_next; + // -- general purpose mark + unsigned m_mark : 1; + // -- general purpose second mark + unsigned m_mark2 : 1; + // -- is an interpreted constant + unsigned m_interpreted : 1; + // caches whether m_expr is an equality + unsigned m_is_eq : 1; + // caches whether m_expr is an inequality + unsigned m_is_neq : 1; + // caches whether m_expr is a distinct + unsigned m_is_distinct : 1; + // caches whether m_expr is a partial equality + unsigned m_is_peq : 1; + // caches whether m_expr is the child of not + unsigned m_is_neq_child : 1; + + // -- the term is a compound term can be rewritten to be ground or it is a + // ground constant + unsigned m_cgr : 1; + // -- the term is ground + unsigned m_gr : 1; + + // -- terms that contain this term as a child (only maintained for root + // nodes) + ptr_vector m_parents; + + // arguments of term. + ptr_vector m_children; + + struct class_props { + // TODO: parents should be here + // -- the class has a ground representative + unsigned m_gr_class : 1; // -- eq class size unsigned m_class_size; - // -- general purpose mark - unsigned m_mark:1; - // -- general purpose second mark - unsigned m_mark2:1; - // -- is an interpreted constant - unsigned m_interpreted:1; + // -- disequality sets that the class belongs to + term_graph::deqs m_deqs; - // -- terms that contain this term as a child - ptr_vector m_parents; - - // arguments of term. - ptr_vector m_children; - - public: - term(expr_ref const& v, u_map& app2term) : - m_expr(v), - m_root(this), - m_next(this), - m_class_size(1), - m_mark(false), - m_mark2(false), - m_interpreted(false) { - if (!is_app(m_expr)) return; - for (expr* e : *to_app(m_expr)) { - term* t = app2term[e->get_id()]; - t->get_root().m_parents.push_back(this); - m_children.push_back(t); - } - } - - ~term() {} - - class parents { - term const& t; - public: - parents(term const& _t):t(_t) {} - parents(term const* _t):t(*_t) {} - ptr_vector::const_iterator begin() const { return t.m_parents.begin(); } - ptr_vector::const_iterator end() const { return t.m_parents.end(); } - }; - - class children { - term const& t; - public: - children(term const& _t):t(_t) {} - children(term const* _t):t(*_t) {} - ptr_vector::const_iterator begin() const { return t.m_children.begin(); } - ptr_vector::const_iterator end() const { return t.m_children.end(); } - }; - - // Congruence table hash function is based on - // roots of children and function declaration. - - unsigned get_hash() const { - unsigned a, b, c; - a = b = c = get_decl_id(); - for (term * ch : children(this)) { - a = ch->get_root().get_id(); - mix(a, b, c); - } - return c; - } - - static bool cg_eq(term const * t1, term const * t2) { - if (t1->get_decl_id() != t2->get_decl_id()) return false; - if (t1->m_children.size() != t2->m_children.size()) return false; - for (unsigned i = 0, sz = t1->m_children.size(); i < sz; ++ i) { - if (t1->m_children[i]->get_root().get_id() != t2->m_children[i]->get_root().get_id()) return false; - } - return true; - } - - unsigned get_id() const { return m_expr->get_id();} - - unsigned get_decl_id() const { return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() : m_expr->get_id(); } - - bool is_marked() const {return m_mark;} - void set_mark(bool v){m_mark = v;} - bool is_marked2() const {return m_mark2;} // NSB: where is this used? - void set_mark2(bool v){m_mark2 = v;} // NSB: where is this used? - - bool is_interpreted() const {return m_interpreted;} - bool is_theory() const { return !is_app(m_expr) || to_app(m_expr)->get_family_id() != null_family_id; } - void mark_as_interpreted() {m_interpreted=true;} - expr* get_expr() const {return m_expr;} - unsigned get_num_args() const { return is_app(m_expr) ? to_app(m_expr)->get_num_args() : 0; } - - term &get_root() const {return *m_root;} - bool is_root() const {return m_root == this;} - void set_root(term &r) {m_root = &r;} - term &get_next() const {return *m_next;} - void add_parent(term* p) { m_parents.push_back(p); } - - unsigned get_class_size() const {return m_class_size;} - - void merge_eq_class(term &b) { - std::swap(this->m_next, b.m_next); - m_class_size += b.get_class_size(); + class_props() : m_gr_class(0), m_class_size(1) {} + void merge(class_props &b) { + m_class_size += b.m_class_size; + m_gr_class |= b.m_gr_class; + m_deqs |= b.m_deqs; // merge disequalities // -- reset (useful for debugging) b.m_class_size = 0; + b.m_gr_class = false; + b.m_deqs.reset(); } - - // -- make this term the root of its equivalence class - void mk_root() { - if (is_root()) return; - - term *curr = this; - do { - if (curr->is_root()) { - // found previous root - SASSERT(curr != this); - m_class_size = curr->get_class_size(); - curr->m_class_size = 0; - } - curr->set_root(*this); - curr = &curr->get_next(); - } - while (curr != this); + void transfer(class_props &b) { + // TODO replace by std::swap of the whole struct? + m_class_size = b.m_class_size; + b.m_class_size = 0; + std::swap(m_deqs, b.m_deqs); + m_gr_class = b.m_gr_class; + b.m_gr_class = false; } + }; + class_props m_class_props; - std::ostream& display(std::ostream& out) const { - out << get_id() << ": " << m_expr - << (is_root() ? " R" : "") << " - "; - term const* r = &this->get_next(); - while (r != this) { - out << r->get_id() << " "; - r = &r->get_next(); - } - out << "\n"; - return out; + public: + term(expr_ref const &v, u_map &app2term) + : m_expr(v), m_root(this), m_repr(nullptr), m_next(this), m_mark(false), + m_mark2(false), m_interpreted(false), + m_is_eq(m_expr.get_manager().is_eq(m_expr)), m_is_peq(false), + m_is_neq_child(false), m_cgr(0), m_gr(0) { + m_is_neq = m_expr.get_manager().is_not(m_expr) && + m_expr.get_manager().is_eq(to_app(m_expr)->get_arg(0)); + m_is_distinct = m_expr.get_manager().is_distinct(m_expr); + m_children.reset(); + if (!is_app(m_expr)) return; + for (expr *e : *to_app(m_expr)) { + term *t = app2term[e->get_id()]; + t->get_root().m_parents.push_back(this); + m_children.push_back(t); + } + m_is_peq = is_partial_eq(to_app(m_expr)); + } + + ~term() {} + + class parents { + term const &t; + + public: + parents(term const &_t) : t(_t) {} + parents(term const *_t) : t(*_t) {} + ptr_vector::const_iterator begin() const { + return t.m_parents.begin(); + } + ptr_vector::const_iterator end() const { + return t.m_parents.end(); } }; - static std::ostream& operator<<(std::ostream& out, term const& t) { - return t.display(out); - } + class children { + term const &t; - bool term_graph::is_variable_proc::operator()(const expr * e) const { - if (!is_app(e)) return false; - const app *a = ::to_app(e); - TRACE("qe_verbose", tout << a->get_family_id() << " " << m_solved.contains(a->get_decl()) << " " << m_decls.contains(a->get_decl()) << "\n";); - return - a->get_family_id() == null_family_id && - !m_solved.contains(a->get_decl()) && - m_exclude == m_decls.contains(a->get_decl()); - } - - bool term_graph::is_variable_proc::operator()(const term &t) const { - return (*this)(t.get_expr()); - } - - void term_graph::is_variable_proc::set_decls(const func_decl_ref_vector &decls, bool exclude) { - reset(); - m_exclude = exclude; - for (auto *d : decls) m_decls.insert(d); - } - void term_graph::is_variable_proc::mark_solved(const expr *e) { - if ((*this)(e) && is_app(e)) - m_solved.insert(::to_app(e)->get_decl()); - } - - - unsigned term_graph::term_hash::operator()(term const* t) const { return t->get_hash(); } - - bool term_graph::term_eq::operator()(term const* a, term const* b) const { return term::cg_eq(a, b); } - - term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m), m_projector(nullptr) { - m_plugins.register_plugin(mbp::mk_basic_solve_plugin(m, m_is_var)); - m_plugins.register_plugin(mbp::mk_arith_solve_plugin(m, m_is_var)); - } - - term_graph::~term_graph() { - dealloc(m_projector); - reset(); - } - - bool term_graph::is_pure_def(expr *atom, expr*& v) { - expr *e = nullptr; - return m.is_eq(atom, v, e) && m_is_var(v) && is_pure(m_is_var, e); - } - - static family_id get_family_id(ast_manager &m, expr *lit) { - if (m.is_not(lit, lit)) - return get_family_id(m, lit); - - expr *a = nullptr, *b = nullptr; - // deal with equality using sort of range - if (m.is_eq (lit, a, b)) { - return a->get_sort()->get_family_id(); + public: + children(term const &_t) : t(_t) {} + children(term const *_t) : t(*_t) {} + ptr_vector::const_iterator begin() const { + return t.m_children.begin(); } - // extract family_id of top level app - else if (is_app(lit)) { - return to_app(lit)->get_decl()->get_family_id(); + ptr_vector::const_iterator end() const { + return t.m_children.end(); } - else { - return null_family_id; - } - } - void term_graph::add_lit(expr *l) { - expr_ref lit(m); - expr_ref_vector lits(m); - lits.push_back(l); - for (unsigned i = 0; i < lits.size(); ++i) { - l = lits.get(i); - family_id fid = get_family_id(m, l); - mbp::solve_plugin *pin = m_plugins.get_plugin(fid); - lit = pin ? (*pin)(l) : l; - if (m.is_and(lit)) { - lits.append(::to_app(lit)->get_num_args(), ::to_app(lit)->get_args()); - } - else { - m_lits.push_back(lit); - internalize_lit(lit); - } + }; + + // Congruence table hash function is based on + // roots of children and function declaration. + + unsigned get_hash() const { + unsigned a, b, c; + a = b = c = get_decl_id(); + for (term *ch : children(this)) { + a = ch->get_root().get_id(); + mix(a, b, c); } + return c; } - bool term_graph::is_internalized(expr *a) { - return m_app2term.contains(a->get_id()); - } - - term* term_graph::get_term(expr *a) { - term *res; - return m_app2term.find (a->get_id(), res) ? res : nullptr; - } - - term *term_graph::mk_term(expr *a) { - expr_ref e(a, m); - term * t = alloc(term, e, m_app2term); - if (t->get_num_args() == 0 && m.is_unique_value(a)) - t->mark_as_interpreted(); - - m_terms.push_back(t); - m_app2term.insert(a->get_id(), t); - return t; - } - - term* term_graph::internalize_term(expr *t) { - term* res = get_term(t); - if (res) return res; - ptr_buffer todo; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - res = get_term(t); - if (res) { - todo.pop_back(); - continue; - } - unsigned sz = todo.size(); - if (is_app(t)) { - for (expr * arg : *::to_app(t)) { - if (!get_term(arg)) - todo.push_back(arg); - } - } - if (sz < todo.size()) continue; - todo.pop_back(); - res = mk_term(t); - } - SASSERT(res); - return res; - } - - void term_graph::internalize_eq(expr *a1, expr* a2) { - SASSERT(m_merge.empty()); - merge(*internalize_term(a1), *internalize_term(a2)); - merge_flush(); - SASSERT(m_merge.empty()); - } - - void term_graph::internalize_lit(expr* lit) { - expr *e1 = nullptr, *e2 = nullptr, *v = nullptr; - if (m.is_eq (lit, e1, e2)) { - internalize_eq (e1, e2); - } - else { - internalize_term(lit); - } - if (is_pure_def(lit, v)) { - m_is_var.mark_solved(v); - } - } - - void term_graph::merge_flush() { - while (!m_merge.empty()) { - term* t1 = m_merge.back().first; - term* t2 = m_merge.back().second; - m_merge.pop_back(); - merge(*t1, *t2); - } - } - - void term_graph::merge(term &t1, term &t2) { - term *a = &t1.get_root(); - term *b = &t2.get_root(); - - if (a == b) return; - - // -- merge might invalidate term2app cache - m_term2app.reset(); - m_pinned.reset(); - - if (a->get_class_size() > b->get_class_size()) { - std::swap(a, b); - } - - // Remove parents of b from the cg table. - for (term* p : term::parents(b)) { - if (!p->is_marked()) { - p->set_mark(true); - m_cg_table.erase(p); - } - } - // make 'a' be the root of the equivalence class of 'b' - b->set_root(*a); - for (term *it = &b->get_next(); it != b; it = &it->get_next()) { - it->set_root(*a); - } - - // merge equivalence classes - a->merge_eq_class(*b); - - // Insert parents of b's old equilvalence class into the cg table - for (term* p : term::parents(b)) { - if (p->is_marked()) { - term* p_old = m_cg_table.insert_if_not_there(p); - p->set_mark(false); - a->add_parent(p); - // propagate new equalities. - if (p->get_root().get_id() != p_old->get_root().get_id()) { - m_merge.push_back(std::make_pair(p, p_old)); - } - } - } - SASSERT(marks_are_clear()); - } - - expr* term_graph::mk_app_core (expr *e) { - if (is_app(e)) { - expr_ref_buffer kids(m); - app* a = ::to_app(e); - for (expr * arg : *a) { - kids.push_back (mk_app(arg)); - } - app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.data()); - m_pinned.push_back(res); - return res; - } - else { - return e; - } - } - - expr_ref term_graph::mk_app(term const &r) { - SASSERT(r.is_root()); - - if (r.get_num_args() == 0) { - return expr_ref(r.get_expr(), m); - } - - expr* res = nullptr; - if (m_term2app.find(r.get_id(), res)) { - return expr_ref(res, m); - } - - res = mk_app_core (r.get_expr()); - m_term2app.insert(r.get_id(), res); - return expr_ref(res, m); - - } - - expr_ref term_graph::mk_app(expr *a) { - term *t = get_term(a); - if (!t) - return expr_ref(a, m); - else - return mk_app(t->get_root()); - - } - - void term_graph::mk_equalities(term const &t, expr_ref_vector &out) { - SASSERT(t.is_root()); - expr_ref rep(mk_app(t), m); - for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { - expr* mem = mk_app_core(it->get_expr()); - out.push_back (m.mk_eq (rep, mem)); - } - } - - void term_graph::mk_all_equalities(term const &t, expr_ref_vector &out) { - mk_equalities(t, out); - - for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) { - expr* a1 = mk_app_core (it->get_expr()); - for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) { - expr* a2 = mk_app_core(it2->get_expr()); - out.push_back (m.mk_eq (a1, a2)); - } - } - } - - void term_graph::reset_marks() { - for (term * t : m_terms) { - t->set_mark(false); - } - } - - bool term_graph::marks_are_clear() { - for (term * t : m_terms) { - if (t->is_marked()) return false; + static bool cg_eq(term const *t1, term const *t2) { + if (t1->get_decl_id() != t2->get_decl_id()) return false; + if (t1->m_children.size() != t2->m_children.size()) return false; + for (unsigned i = 0, sz = t1->m_children.size(); i < sz; ++i) { + if (t1->m_children[i]->get_root().get_id() != + t2->m_children[i]->get_root().get_id()) + return false; } return true; } - /// Order of preference for roots of equivalence classes - /// XXX This should be factored out to let clients control the preference - bool term_graph::term_lt(term const &t1, term const &t2) { - // prefer constants over applications - // prefer uninterpreted constants over values - // prefer smaller expressions over larger ones - if (t1.get_num_args() == 0 || t2.get_num_args() == 0) { - if (t1.get_num_args() == t2.get_num_args()) { - // t1.get_num_args() == t2.get_num_args() == 0 - if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr())) - return t1.get_id() < t2.get_id(); - return m.is_value(t2.get_expr()); - } - return t1.get_num_args() < t2.get_num_args(); - } - - unsigned sz1 = get_num_exprs(t1.get_expr()); - unsigned sz2 = get_num_exprs(t2.get_expr()); - return sz1 < sz2; + unsigned deg() const { return m_children.size(); } + unsigned get_id() const { return m_expr->get_id(); } + bool is_eq_or_neq() const { return m_is_eq || m_is_neq || m_is_distinct; } + bool is_eq_or_peq() const { return m_is_eq || m_is_peq; } + bool is_neq() const { return m_is_neq; } + void set_neq_child() { m_is_neq_child = true; } + bool is_neq_child() const { return m_is_neq_child; } + unsigned get_decl_id() const { + return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() + : m_expr->get_id(); } - void term_graph::pick_root (term &t) { - term *r = &t; - for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { - it->set_mark(true); - if (term_lt(*it, *r)) { r = it; } - } + bool is_marked() const { return m_mark; } + void set_mark(bool v) { m_mark = v; } + bool is_marked2() const { return m_mark2; } // NSB: where is this used? + void set_mark2(bool v) { m_mark2 = v; } // NSB: where is this used? - // -- if found something better, make it the new root - if (r != &t) { - r->mk_root(); + bool is_cgr() const { return m_cgr; } + void set_cgr(bool v) { m_cgr = v; } + + bool is_gr() const { return m_gr; } + void set_gr(bool v) { m_gr = v; } + + bool is_class_gr_root() const { + SASSERT(is_root()); + return m_class_props.m_gr_class; + } + void set_class_gr_root(bool v) { + SASSERT(is_root()); + m_class_props.m_gr_class = v; + } + bool is_class_gr() const { return m_root->is_class_gr_root(); } + void set_class_gr(bool v) { m_root->set_class_gr_root(v); } + + static bool are_deq(const term &t1, const term &t2) { + term_graph::deqs const &ds1 = t1.get_root().get_deqs(); + term_graph::deqs const &ds2 = t2.get_root().get_deqs(); + + term_graph::deqs tmp(ds1); // copy + + tmp &= ds2; + return tmp != 0; + } + + static void set_deq(term_graph::deqs &ds, unsigned idx) { + ds.resize(idx + 1); + ds.set(idx); + } + + bool all_children_ground() { + SASSERT(deg() != 0); + return all_of(m_children, + [&](const term *t) { return t->is_class_gr(); }); + } + + void set_mark2_terms_class(bool v) { // TODO: remove + if (is_marked2()) return; + term *curr = this; + do { + curr->set_mark2(v); + curr = &curr->get_next(); + } + while (curr != this); + } + + bool is_interpreted() const { return m_interpreted; } + bool is_theory() const { + return !is_app(m_expr) || + to_app(m_expr)->get_family_id() != null_family_id; + } + void mark_as_interpreted() { m_interpreted = true; } + expr *get_expr() const { return m_expr; } + unsigned get_num_args() const { + return is_app(m_expr) ? to_app(m_expr)->get_num_args() : 0; + } + + term &get_root() const { return *m_root; } + bool is_root() const { return m_root == this; } + void set_root(term &r) { m_root = &r; } + term *get_repr() { return m_repr; } + bool is_repr() const { return m_repr == this; } + void set_repr(term *t) { + SASSERT(get_root().get_id() == t->get_root().get_id()); + m_repr = t; + } + void reset_repr() { m_repr = nullptr; } + term &get_next() const { return *m_next; } + void add_parent(term *p) { m_parents.push_back(p); } + + unsigned get_class_size() const { return m_class_props.m_class_size; } + + void merge_eq_class(term &b) { + std::swap(this->m_next, b.m_next); + m_class_props.merge(b.m_class_props); + } + + // -- make this term the repr of its equivalence class + void mk_repr() { + term *curr = this; + do { + curr->set_repr(this); + curr = &curr->get_next(); + } + while (curr != this); + } + + std::ostream &display(std::ostream &out) const { + out << get_id() << ": " << m_expr << (is_repr() ? " R" : "") + << (is_gr() ? " G" : "") << (is_class_gr() ? " clsG" : "") + << (is_cgr() ? " CG" : "") << " deg:" << deg() << " - "; + term const *r = &this->get_next(); + while (r != this) { + out << r->get_id() << " " << (r->is_cgr() ? " CG" : "") << " "; + r = &r->get_next(); + } + out << "\n"; + return out; + } + + term_graph::deqs &get_deqs() { return m_class_props.m_deqs; } +}; + +static std::ostream &operator<<(std::ostream &out, term const &t) { + return t.display(out); +} + +// t1 != t2 +void term_graph::add_deq_proc::operator()(term *t1, term *t2) { + ptr_vector ts(2); + ts[0] = t1; + ts[1] = t2; + (*this)(ts); +} + +// distinct(ts) +void term_graph::add_deq_proc::operator()(ptr_vector &ts) { + for (auto t : ts) { term::set_deq(t->get_root().get_deqs(), m_deq_cnt); } + SASSERT(m_deq_cnt < UINT64_MAX); + m_deq_cnt++; +} + +bool term_graph::is_variable_proc::operator()(const expr *e) const { + if (!is_app(e)) return false; + const app *a = ::to_app(e); + TRACE("qe_verbose", tout << a->get_family_id() << " " + << m_solved.contains(a->get_decl()) << " " + << m_decls.contains(a->get_decl()) << "\n";); + return a->get_family_id() == null_family_id && + !m_solved.contains(a->get_decl()) && + m_exclude == m_decls.contains(a->get_decl()); +} + +bool term_graph::is_variable_proc::operator()(const term &t) const { + return (*this)(t.get_expr()); +} + +void term_graph::is_variable_proc::set_decls(const func_decl_ref_vector &decls, + bool exclude) { + reset(); + m_exclude = exclude; + for (auto *d : decls) m_decls.insert(d); +} + +void term_graph::is_variable_proc::add_decls(const app_ref_vector &decls) { + for (auto *d : decls) m_decls.insert(d->get_decl()); +} + +void term_graph::is_variable_proc::add_decl(app *d) { + m_decls.insert(d->get_decl()); +} + +void term_graph::is_variable_proc::set_decls(const app_ref_vector &vars, + bool exclude) { + reset(); + m_exclude = exclude; + for (auto *v : vars) m_decls.insert(v->get_decl()); +} + +void term_graph::is_variable_proc::mark_solved(const expr *e) { + if ((*this)(e) && is_app(e)) m_solved.insert(::to_app(e)->get_decl()); +} + +unsigned term_graph::term_hash::operator()(term const *t) const { + return t->get_hash(); +} + +bool term_graph::term_eq::operator()(term const *a, term const *b) const { + return term::cg_eq(a, b); +} + +term_graph::term_graph(ast_manager &man) + : m(man), m_lits(m), m_pinned(m), m_projector(nullptr), + m_explicit_eq(false), m_repick_repr(false) { + m_is_var.reset(); + m_plugins.register_plugin(mbp::mk_basic_solve_plugin(m, m_is_var)); + m_plugins.register_plugin(mbp::mk_arith_solve_plugin(m, m_is_var)); +} + +term_graph::~term_graph() { + dealloc(m_projector); + reset(); +} + +bool term_graph::is_pure_def(expr *atom, expr *&v) { + expr *e = nullptr; + return m.is_eq(atom, v, e) && m_is_var(v) && is_pure(m_is_var, e); +} + +static family_id get_family_id(ast_manager &m, expr *lit) { + if (m.is_not(lit, lit)) return get_family_id(m, lit); + + expr *a = nullptr, *b = nullptr; + // deal with equality using sort of range + if (m.is_eq(lit, a, b)) { return a->get_sort()->get_family_id(); } + // extract family_id of top level app + else if (is_app(lit)) { return to_app(lit)->get_decl()->get_family_id(); } + else { return null_family_id; } +} +void term_graph::add_lit(expr *l) { + expr_ref lit(m); + expr_ref_vector lits(m); + lits.push_back(l); + for (unsigned i = 0; i < lits.size(); ++i) { + l = lits.get(i); + family_id fid = get_family_id(m, l); + mbp::solve_plugin *pin = m_plugins.get_plugin(fid); + lit = pin ? (*pin)(l) : l; + if (m.is_and(lit)) { + lits.append(::to_app(lit)->get_num_args(), + ::to_app(lit)->get_args()); + } + else { + m_lits.push_back(lit); + internalize_lit(lit); + } + } +} + +// collect expressions of all terms in the term graph +// optionally, exclude constructively ground nodes that are not equalities +// overwrites res +void term_graph::get_terms(expr_ref_vector &res, bool exclude_cground) { + std::function fil = nullptr; + if (exclude_cground) { + fil = [](term *t) { + return !t->is_neq_child() && (t->is_eq_or_peq() || !t->is_cgr()); + }; + } + else { + fil = [](term *t) { return !t->is_neq_child(); }; + } + auto terms = m_terms.filter_pure(fil); + res.resize(terms.size()); + unsigned i = 0; + for (term *t : terms) res[i++] = t->get_expr(); +} + +bool term_graph::is_cgr(expr *e) { + if (!is_internalized(e)) return false; + term *t = get_term(e); + return (!t->is_eq_or_peq() && t->is_cgr()); +} + +bool term_graph::is_internalized(expr *a) { + return m_app2term.contains(a->get_id()); +} + +term *term_graph::get_term(expr *a) { + term *res; + return m_app2term.find(a->get_id(), res) ? res : nullptr; +} + +term *term_graph::mk_term(expr *a) { + expr_ref e(a, m); + term *t = alloc(term, e, m_app2term); + if (is_ground(a)) { + t->set_gr(true); + t->set_cgr(true); + t->set_class_gr(true); + } + else if (t->deg() > 0 && t->all_children_ground()) { + t->set_cgr(true); + t->set_class_gr(true); + } + if (t->get_num_args() == 0 && m.is_unique_value(a)) + t->mark_as_interpreted(); + + m_terms.push_back(t); + m_app2term.insert(a->get_id(), t); + return t; +} + +term *term_graph::internalize_term(expr *t) { + term *res = get_term(t); + if (res) return res; + ptr_buffer todo; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + res = get_term(t); + if (res) { + todo.pop_back(); + continue; + } + unsigned sz = todo.size(); + if (is_app(t)) { + for (expr *arg : *::to_app(t)) { + if (!get_term(arg)) todo.push_back(arg); + } + } + if (sz < todo.size()) continue; + todo.pop_back(); + res = mk_term(t); + + // the term was not internalized in this syntactic form, but it + // could be congruent with some other term, if that is the case, we + // need to merge them. + term *res_old = m_cg_table.insert_if_not_there(res); + if (res->is_cgr()) res_old->set_cgr(true); + SASSERT(res_old->is_cgr() == res->is_cgr()); + if (res_old->get_root().get_id() != res->get_root().get_id()) { + m_merge.push_back(std::make_pair(res, res_old)); + } + } + merge_flush(); + SASSERT(res); + return res; +} + +void term_graph::internalize_eq(expr *a1, expr *a2) { + SASSERT(m_merge.empty()); + merge(*internalize_term(a1), *internalize_term(a2)); + merge_flush(); + SASSERT(m_merge.empty()); + if (!m_explicit_eq) return; + expr_ref eq(m.mk_eq(a1, a2), m); + term *res = get_term(eq); + if (!res) mk_term(eq); +} + +void term_graph::internalize_distinct(expr *d) { + app *a = to_app(d); + ptr_vector ts(a->get_decl()->get_arity()); + auto tsit = ts.begin(); + for (auto arg : *a) { + *tsit = internalize_term(arg); + tsit++; + } + m_add_deq(ts); + m_deq_distinct.push_back(ts); + if (!m_explicit_eq) return; + term *t = get_term(d); + if (!t) mk_term(d); +} + +// Assumes that a1 != a2 is satisfiable +void term_graph::internalize_deq(expr *a1, expr *a2) { + term *t1 = internalize_term(a1); + term *t2 = internalize_term(a2); + m_add_deq(t1, t2); + m_deq_pairs.push_back({t1, t2}); + if (!m_explicit_eq) return; + expr_ref eq(m.mk_eq(a1, a2), m); + term *eq_term = mk_term(eq); + eq_term->set_neq_child(); + expr_ref deq(m.mk_not(eq), m); + term *res = get_term(deq); + if (!res) mk_term(deq); +} + +void term_graph::internalize_lit(expr *lit) { + expr *e1 = nullptr, *e2 = nullptr, *ne = nullptr, *v = nullptr; + if (m.is_eq(lit, e1, e2)) { // internalize equality + internalize_eq(e1, e2); + } + else if (m.is_distinct(lit)) { internalize_distinct(lit); } + else if (m.is_not(lit, ne) && m.is_eq(ne, e1, e2)) { + internalize_deq(e1, e2); + } + else { internalize_term(lit); } + if (is_pure_def(lit, v)) { m_is_var.mark_solved(v); } +} + +void term_graph::merge_flush() { + while (!m_merge.empty()) { + term *t1 = m_merge.back().first; + term *t2 = m_merge.back().second; + m_merge.pop_back(); + merge(*t1, *t2); + } +} + +void term_graph::merge(term &t1, term &t2) { + term *a = &t1.get_root(); + term *b = &t2.get_root(); + + if (a == b) return; + + // -- merge might invalidate term2app cache + m_term2app.reset(); + m_pinned.reset(); + m_repick_repr = true; + + if (a->get_class_size() > b->get_class_size()) { std::swap(a, b); } + + // Remove parents of b from the cg table + for (term *p : term::parents(b)) { + if (!p->is_marked()) { + p->set_mark(true); + m_cg_table.erase(p); } } - /// Choose better roots for equivalence classes - void term_graph::pick_roots() { - SASSERT(marks_are_clear()); - for (term* t : m_terms) { - if (!t->is_marked() && t->is_root()) - pick_root(*t); - } - reset_marks(); + bool prop_cgroundness = (b->is_class_gr() != a->is_class_gr()); + // make 'a' be the root of the equivalence class of 'b' + b->set_root(*a); + for (term *it = &b->get_next(); it != b; it = &it->get_next()) { + it->set_root(*a); } - void term_graph::display(std::ostream &out) { - for (term * t : m_terms) { - out << *t; + // merge equivalence classes + a->merge_eq_class(*b); + + // Insert parents of b's old equivalence class into the cg table + // bottom-up merge of parents + for (term *p : term::parents(b)) { + if (p->is_marked()) { + term *p_old = m_cg_table.insert_if_not_there(p); + p->set_mark(false); + a->add_parent(p); + // propagate new equalities. + if (p->get_root().get_id() != p_old->get_root().get_id()) { + m_merge.push_back(std::make_pair(p, p_old)); + } + } + } + if (prop_cgroundness) cground_percolate_up(a); + + SASSERT(marks_are_clear()); +} + +expr *term_graph::mk_app_core(expr *e) { + if (is_app(e)) { + expr_ref_buffer kids(m); + app *a = ::to_app(e); + for (expr *arg : *a) { kids.push_back(mk_app(arg)); } + app *res = m.mk_app(a->get_decl(), a->get_num_args(), kids.data()); + m_pinned.push_back(res); + return res; + } + else { return e; } +} + +expr_ref term_graph::mk_app(term &r) { + SASSERT(r.is_repr()); + + if (r.get_num_args() == 0) { return expr_ref(r.get_expr(), m); } + + expr *res = nullptr; + if (m_term2app.find(r.get_id(), res)) { return expr_ref(res, m); } + + res = mk_app_core(r.get_expr()); + m_term2app.insert(r.get_id(), res); + return expr_ref(res, m); +} + +expr_ref term_graph::mk_app(expr *a) { + term *t = get_term(a); + if (!t) + return expr_ref(a, m); + else { + SASSERT(t->get_repr()); + return mk_app(*t->get_repr()); + } +} + +void term_graph::mk_equalities(term &t, expr_ref_vector &out) { + SASSERT(t.is_repr()); + if (t.get_class_size() == 1) return; + expr_ref rep(mk_app(t), m); + for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { + expr *mem = mk_app_core(it->get_expr()); + out.push_back(m.mk_eq(rep, mem)); + } +} + +void term_graph::mk_all_equalities(term &t, expr_ref_vector &out) { + if (t.get_class_size() == 1) return; + + mk_equalities(t, out); + + for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { + expr *a1 = mk_app_core(it->get_expr()); + for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) { + expr *a2 = mk_app_core(it2->get_expr()); + out.push_back(m.mk_eq(a1, a2)); + } + } +} + +void term_graph::mk_qe_lite_equalities(term &t, expr_ref_vector &out, + check_pred &contains_nc) { + SASSERT(t.is_repr()); + if (t.get_class_size() == 1) return; + expr_ref rep(m); + rep = mk_app(t); + if (contains_nc(rep)) { + TRACE( + "qe_debug", tout << "repr not in core " << t; + for (term *it = &t.get_next(); it != &t; + it = &it->get_next()) { tout << *it << "\n"; };); + DEBUG_CODE( + for (term *it = &t.get_next(); it != &t; it = &it->get_next()) + SASSERT(!it->is_cgr() || + contains_nc(mk_app_core(it->get_expr())));); + return; + } + for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { + expr *e = it->get_expr(); + SASSERT(is_app(e)); + app *a = to_app(e); + // don't add equalities for vars to eliminate + if (m_is_var.contains(a->get_decl())) continue; + expr *mem = mk_app_core(e); + if (rep != mem && !contains_nc(mem)) out.push_back(m.mk_eq(rep, mem)); + } +} + +void term_graph::reset_marks() { + for (term *t : m_terms) { t->set_mark(false); } +} + +void term_graph::reset_marks2() { + for (term *t : m_terms) { t->set_mark2(false); } +} + +bool term_graph::marks_are_clear() { + for (term *t : m_terms) { + if (t->is_marked()) return false; + } + return true; +} + +/// Order of preference for roots of equivalence classes +/// XXX This should be factored out to let clients control the preference +bool term_graph::term_lt(term const &t1, term const &t2) { + // prefer constants over applications (ground) + // prefer applications over variables (for non-ground) + // prefer uninterpreted constants over values + // prefer smaller expressions over larger ones + + if (t1.get_num_args() == 0 || t2.get_num_args() == 0) { + if (t1.get_num_args() == t2.get_num_args()) { + if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr())) + return t1.get_id() < t2.get_id(); + return m.is_value(t2.get_expr()); + } + return t1.get_num_args() < t2.get_num_args(); + } + + // XXX this is the internalized size, not the size with the new + // representatives + unsigned sz1 = get_num_exprs(t1.get_expr()); + unsigned sz2 = get_num_exprs(t2.get_expr()); + return sz1 < sz2; +} + +bool all_children_picked(term *t) { + if (t->deg() == 0) return true; + for (term *c : term::children(t)) { + if (!c->get_repr()) return false; + } + return true; +} + +// pick representatives for all terms in todo. Then, pick representatives for +// all terms whose children have representatives +void term_graph::pick_repr_percolate_up(ptr_vector &todo) { + term *t; + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (t->get_repr()) continue; + pick_repr_class(t); + for (auto it : term::parents(t->get_root())) + if (all_children_picked(it)) todo.push_back(it); + } +} + +// iterate through all terms in a class and pick a representative that: +// 1. is cgr and 2. least according to term_lt +void term_graph::pick_repr_class(term *t) { + SASSERT(all_children_picked(t)); + term *r = t; + for (term *it = &t->get_next(); it != t; it = &it->get_next()) { + if (!all_children_picked(it)) continue; + if ((it->is_cgr() && !r->is_cgr()) || + (it->is_cgr() == r->is_cgr() && term_lt(*it, *r))) + r = it; + } + r->mk_repr(); +} + +// Choose repr for equivalence classes +// repr has the following properties: +// 1. acyclicity (mk_app terminates) +// 2. maximal wrt cgr +// 3. each class has exactly one repr +// assumes that cgroundness has been computed +void term_graph::pick_repr() { + // invalidates cache + m_term2app.reset(); + DEBUG_CODE(for (term *t + : m_terms) + SASSERT(t->deg() == 0 || !t->all_children_ground() || + t->is_cgr());); + for (term *t : m_terms) t->reset_repr(); + ptr_vector todo; + for (term *t : m_terms) { + if (t->deg() == 0 && t->is_cgr()) todo.push_back(t); + } + pick_repr_percolate_up(todo); + DEBUG_CODE(for (term *t : m_terms) SASSERT(!t->is_cgr() || t->get_repr());); + + for (term *t : m_terms) { + if (t->get_repr()) continue; + if (t->deg() == 0) todo.push_back(t); + } + pick_repr_percolate_up(todo); + DEBUG_CODE(for (term *t : m_terms) SASSERT(t->get_repr());); + DEBUG_CODE(for (auto t + : m_terms) + SASSERT(!t->is_cgr() || t->get_repr()->is_cgr());); +} + +// if t is a variable, attempt to pick non-var +void term_graph::refine_repr_class(term *t) { + SASSERT(t->is_repr()); + auto is_var = [&](term *p) { + SASSERT(is_app(p->get_expr())); + return m_is_var.contains(to_app(p->get_expr())->get_decl()); + }; + if (!is_var(t)) return; + term *r = t; + for (term *it = &t->get_next(); it != t; it = &it->get_next()) { + if (makes_cycle(it)) continue; + if (is_var(r) && !is_var(it)) r = it; + } + r->mk_repr(); +} + +// check if t makes a cycle if chosen as repr. This function assumes that the +// current repr doesn't have cycles. If there is a cycle in a child class the +// function doesn't terminate. +bool term_graph::makes_cycle(term *t) { + term &r = t->get_root(); + ptr_vector todo; + for (auto *it : term::children(t)) { todo.push_back(it->get_repr()); } + term *it; + while (!todo.empty()) { + it = todo.back(); + todo.pop_back(); + if (it->get_root().get_id() == r.get_id()) return true; + for (auto *ch : term::children(it)) { todo.push_back(ch->get_repr()); } + } + return false; +} + +void term_graph::refine_repr() { + // invalidates cache + m_term2app.reset(); + for (term *t : m_terms) { + if (!t->get_repr()->is_cgr()) refine_repr_class(t->get_repr()); + } +} + +// returns true if tg ==> e = v where v is a value +bool term_graph::has_val_in_class(expr *e) { + term *r = get_term(e); + if (!r) return false; + auto is_val = [&](term *t) { return m.is_value(t->get_expr()); }; + if (is_val(r)) return true; + for (term *it = &r->get_next(); it != r; it = &it->get_next()) + if (is_val(it)) return true; + return false; +} + +// if there exists an uninterpreted const c s.t. tg ==> e = c, return c +// else return nullptr +app *term_graph::get_const_in_class(expr *e) { + term *r = get_term(e); + if (!r) return nullptr; + auto is_const = [](term *t) { return is_uninterp_const(t->get_expr()); }; + if (is_const(r)) return ::to_app(r->get_expr()); + for (term *it = &r->get_next(); it != r; it = &it->get_next()) + if (is_const(it)) return ::to_app(it->get_expr()); + return nullptr; +} + +void term_graph::display(std::ostream &out) { + for (term *t : m_terms) { out << *t; } +} + +void term_graph::to_lits(expr_ref_vector &lits, bool all_equalities, + bool repick_repr) { + if (m_repick_repr || repick_repr) pick_repr(); + + for (expr *a : m_lits) { + if (is_internalized(a)) { + if (m_explicit_eq && get_term(a)->is_eq_or_neq()) continue; + lits.push_back(::to_app(mk_app(a))); } } - void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) { - pick_roots(); - - for (expr * a : m_lits) { - if (is_internalized(a)) { - lits.push_back (::to_app(mk_app(a))); - } - } - - for (term * t : m_terms) { - if (!t->is_root()) - continue; - else if (all_equalities) - mk_all_equalities (*t, lits); - else - mk_equalities(*t, lits); - } + for (term *t : m_terms) { + if (t->is_eq_or_neq()) continue; + if (!t->is_repr()) + continue; + else if (all_equalities) + mk_all_equalities(*t, lits); + else + mk_equalities(*t, lits); } - expr_ref term_graph::to_expr() { - expr_ref_vector lits(m); - to_lits(lits); - return mk_and(lits); + // TODO: use seen to prevent duplicate disequalities + for (auto p : m_deq_pairs) { + lits.push_back(mk_neq(m, mk_app(p.first->get_expr()), + mk_app(p.second->get_expr()))); } - void term_graph::reset() { - m_term2app.reset(); - m_pinned.reset(); - m_app2term.reset(); - std::for_each(m_terms.begin(), m_terms.end(), delete_proc()); - m_terms.reset(); - m_lits.reset(); - m_cg_table.reset(); + for (auto t : m_deq_distinct) { + ptr_vector args(t.size()); + for (auto c : t) args.push_back(mk_app(c->get_expr())); + lits.push_back(m.mk_distinct(args.size(), args.data())); + } +} + +// assumes that representatives have already been picked +void term_graph::to_lits_qe_lite(expr_ref_vector &lits, + std::function *non_core) { + DEBUG_CODE(for (auto t : m_terms) SASSERT(t->get_repr());); + DEBUG_CODE(for (auto t + : m_terms) + SASSERT(!t->is_cgr() || t->get_repr()->is_cgr());); + is_non_core not_in_core(non_core); + check_pred contains_nc(not_in_core, m, false); + // literals other than eq, neq, distinct + for (expr *a : m_lits) { + if (!is_internalized(a)) continue; + if (m_explicit_eq && get_term(a)->is_eq_or_neq()) continue; + expr_ref r(m); + r = mk_app(a); + if (non_core == nullptr || !contains_nc(r)) lits.push_back(r); } - class term_graph::projector { - term_graph &m_tg; - ast_manager &m; - u_map m_term2app; - u_map m_root2rep; - th_rewriter m_rewriter; + // equalities + for (term *t : m_terms) { + if (t->is_eq_or_neq()) continue; + if (!t->is_repr()) continue; + mk_qe_lite_equalities(*t, lits, contains_nc); + } + // disequalities and distinct + // TODO: use seen to prevent duplicate disequalities + expr_ref e1(m), e2(m), d(m), distinct(m); + expr_ref_vector args(m); + for (auto p : m_deq_pairs) { + e1 = mk_app(*(p.first->get_repr())); + e2 = mk_app(*(p.second->get_repr())); + if (non_core == nullptr || (!contains_nc(e1) && !contains_nc(e2))) + lits.push_back(mk_neq(m, e1, e2)); + } - model_ref m_model; - expr_ref_vector m_pinned; // tracks expr in the maps + for (auto t : m_deq_distinct) { + args.reset(); + for (auto c : t) { + d = mk_app(*(c->get_repr())); + if (non_core == nullptr || !contains_nc(d)) args.push_back(d); + } + if (args.size() < 2) continue; + if (args.size() == 2) + distinct = mk_neq(m, args.get(0), args.get(1)); + else + distinct = m.mk_distinct(args.size(), args.data()); + lits.push_back(distinct); + } +} - expr* mk_pure(term const& t) { - TRACE("qe", t.display(tout);); - expr* e = nullptr; - if (find_term2app(t, e)) return e; - e = t.get_expr(); - if (!is_app(e)) return nullptr; - app* a = ::to_app(e); - expr_ref_buffer kids(m); - for (term* ch : term::children(t)) { - // prefer a node that resembles current child, - // otherwise, pick a root representative, if present. - if (find_term2app(*ch, e)) { - kids.push_back(e); - } - else if (m_root2rep.find(ch->get_root().get_id(), e)) { - kids.push_back(e); - } - else { - return nullptr; - } - TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";); +expr_ref term_graph::to_expr(bool repick_repr) { + expr_ref_vector lits(m); + to_lits(lits, false, repick_repr); + return mk_and(lits); +} + +void term_graph::reset() { + m_term2app.reset(); + m_pinned.reset(); + m_app2term.reset(); + std::for_each(m_terms.begin(), m_terms.end(), delete_proc()); + m_terms.reset(); + m_lits.reset(); + m_cg_table.reset(); +} + +class term_graph::projector { + term_graph &m_tg; + ast_manager &m; + u_map m_term2app; + u_map m_root2rep; + th_rewriter m_rewriter; + + model_ref m_model; + expr_ref_vector m_pinned; // tracks expr in the maps + + expr *mk_pure(term const &t) { + TRACE("qe", t.display(tout);); + expr *e = nullptr; + if (find_term2app(t, e)) return e; + e = t.get_expr(); + if (!is_app(e)) return nullptr; + app *a = ::to_app(e); + expr_ref_buffer kids(m); + for (term *ch : term::children(t)) { + // prefer a node that resembles current child, + // otherwise, pick a root representative, if present. + if (find_term2app(*ch, e)) { kids.push_back(e); } + else if (m_root2rep.find(ch->get_root().get_id(), e)) { + kids.push_back(e); } - expr_ref pure = m_rewriter.mk_app(a->get_decl(), kids.size(), kids.data()); - m_pinned.push_back(pure); - add_term2app(t, pure); - return pure; + else { return nullptr; } + TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";); } + expr_ref pure = + m_rewriter.mk_app(a->get_decl(), kids.size(), kids.data()); + m_pinned.push_back(pure); + add_term2app(t, pure); + return pure; + } + bool is_better_rep(expr *t1, expr *t2) { + if (!t2) return t1 != nullptr; + return m.is_unique_value(t1) && !m.is_unique_value(t2); + } - bool is_better_rep(expr *t1, expr *t2) { - if (!t2) return t1 != nullptr; - return m.is_unique_value(t1) && !m.is_unique_value(t2); + struct term_depth { + bool operator()(term const *t1, term const *t2) const { + return get_depth(t1->get_expr()) < get_depth(t2->get_expr()); } + }; - struct term_depth { - bool operator()(term const* t1, term const* t2) const { - return get_depth(t1->get_expr()) < get_depth(t2->get_expr()); - } - }; - - - void solve_core() { - ptr_vector worklist; - for (term * t : m_tg.m_terms) { - // skip pure terms - if (!in_term2app(*t)) { - worklist.push_back(t); - t->set_mark(true); - } - } - term_depth td; - std::sort(worklist.begin(), worklist.end(), td); - - for (unsigned i = 0; i < worklist.size(); ++i) { - term* t = worklist[i]; - t->set_mark(false); - if (in_term2app(*t)) - continue; - - expr* pure = mk_pure(*t); - if (!pure) - continue; - - add_term2app(*t, pure); - expr* rep = nullptr; - // ensure that the root has a representative - m_root2rep.find(t->get_root().get_id(), rep); - - if (!rep) { - m_root2rep.insert(t->get_root().get_id(), pure); - for (term * p : term::parents(t->get_root())) { - SASSERT(!in_term2app(*p)); - if (!p->is_marked()) { - p->set_mark(true); - worklist.push_back(p); - } - } - } - } - m_tg.reset_marks(); - } - - bool find_app(term &t, expr *&res) { - return - find_term2app(t, res) || - m_root2rep.find(t.get_root().get_id(), res); - } - - bool find_app(expr *lit, expr *&res) { - term const* t = m_tg.get_term(lit); - return - find_term2app(*t, res) || - m_root2rep.find(t->get_root().get_id(), res); - } - - void mk_lits(expr_ref_vector &res) { - expr *e = nullptr; - for (auto *lit : m_tg.m_lits) { - if (!m.is_eq(lit) && find_app(lit, e)) - res.push_back(e); - } - TRACE("qe", tout << "literals: " << res << "\n";); - } - - void lits2pure(expr_ref_vector& res) { - expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr; - for (auto *lit : m_tg.m_lits) { - if (m.is_eq(lit, e1, e2)) { - if (find_app(e1, p1) && find_app(e2, p2)) { - if (p1 != p2) - res.push_back(m.mk_eq(p1, p2)); - } - else - TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); - } - else if (m.is_distinct(lit)) { - ptr_buffer diff; - for (expr* arg : *to_app(lit)) - if (find_app(arg, p1)) - diff.push_back(p1); - if (diff.size() > 1) - res.push_back(m.mk_distinct(diff.size(), diff.data())); - else - TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); - } - else if (find_app(lit, p1)) - res.push_back(p1); - else - TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); - } - remove_duplicates(res); - TRACE("qe", tout << "literals: " << res << "\n";); - } - - void remove_duplicates(expr_ref_vector& v) { - obj_hashtable seen; - unsigned j = 0; - for (expr* e : v) { - if (!seen.contains(e)) { - v[j++] = e; - seen.insert(e); - } - } - v.shrink(j); - } - - vector> m_decl2terms; // terms that use function f - ptr_vector m_decls; - - void collect_decl2terms() { - // Collect the projected function symbols. - m_decl2terms.reset(); - m_decls.reset(); - for (term *t : m_tg.m_terms) { - expr* e = t->get_expr(); - if (!is_app(e)) continue; - if (!is_projected(*t)) continue; - app* a = to_app(e); - func_decl* d = a->get_decl(); - if (d->get_arity() == 0) continue; - unsigned id = d->get_small_id(); - m_decl2terms.reserve(id+1); - if (m_decl2terms[id].empty()) m_decls.push_back(d); - m_decl2terms[id].push_back(t); - } - } - - void args_are_distinct(expr_ref_vector& res) { - // - // for each projected function that occurs - // (may occur) in multiple congruence classes, - // produce assertions that non-congruent arguments - // are distinct. - // - for (func_decl* d : m_decls) { - unsigned id = d->get_small_id(); - ptr_vector const& terms = m_decl2terms[id]; - if (terms.size() <= 1) continue; - unsigned arity = d->get_arity(); - for (unsigned i = 0; i < arity; ++i) { - obj_hashtable roots, root_vals; - expr_ref_vector pinned(m); - for (term* t : terms) { - expr* arg = to_app(t->get_expr())->get_arg(i); - term const& root = m_tg.get_term(arg)->get_root(); - expr* r = root.get_expr(); - // if a model is given, then use the equivalence class induced - // by the model. Otherwise, use the congruence class. - if (m_model) { - expr_ref tmp(m); - tmp = (*m_model)(r); - if (!root_vals.contains(tmp)) { - root_vals.insert(tmp); - roots.insert(r); - pinned.push_back(tmp); - } - } - else { - roots.insert(r); - } - } - if (roots.size() > 1) { - ptr_buffer args; - for (expr* r : roots) { - args.push_back(r); - } - TRACE("qe", tout << "function: " << d->get_name() << "\n";); - res.push_back(m.mk_distinct(args.size(), args.data())); - } - } - } - } - - void mk_distinct(expr_ref_vector& res) { - collect_decl2terms(); - args_are_distinct(res); - TRACE("qe", tout << res << "\n";); - } - - void mk_pure_equalities(const term &t, expr_ref_vector &res) { - SASSERT(t.is_root()); - expr *rep = nullptr; - if (!m_root2rep.find(t.get_id(), rep)) return; - obj_hashtable members; - members.insert(rep); - term const * r = &t; - do { - expr* member = nullptr; - if (find_term2app(*r, member) && !members.contains(member)) { - res.push_back (m.mk_eq (rep, member)); - members.insert(member); - } - r = &r->get_next(); - } - while (r != &t); - } - - bool is_projected(const term &t) { - return m_tg.m_is_var(t); - } - - void mk_unpure_equalities(const term &t, expr_ref_vector &res) { - expr *rep = nullptr; - if (!m_root2rep.find(t.get_id(), rep)) return; - obj_hashtable members; - members.insert(rep); - term const * r = &t; - do { - expr* member = mk_pure(*r); - SASSERT(member); - if (!members.contains(member) && - (!is_projected(*r) || !is_solved_eq(rep, member))) { - res.push_back(m.mk_eq(rep, member)); - members.insert(member); - } - r = &r->get_next(); - } - while (r != &t); - } - - template - void mk_equalities(expr_ref_vector &res) { - for (term *t : m_tg.m_terms) { - if (!t->is_root()) continue; - if (!m_root2rep.contains(t->get_id())) continue; - if (pure) - mk_pure_equalities(*t, res); - else - mk_unpure_equalities(*t, res); - } - TRACE("qe", tout << "literals: " << res << "\n";); - } - - void mk_pure_equalities(expr_ref_vector &res) { - mk_equalities(res); - } - - void mk_unpure_equalities(expr_ref_vector &res) { - mk_equalities(res); - } - - // TBD: generalize for also the case of a (:var n) - bool is_solved_eq(expr *lhs, expr* rhs) { - return is_uninterp_const(rhs) && !occurs(rhs, lhs); - } - - /// Add equalities and disequalities for all pure representatives - /// based on their equivalence in the model - void model_complete(expr_ref_vector &res) { - if (!m_model) return; - obj_map val2rep; - model_evaluator mev(*m_model); - for (auto &kv : m_root2rep) { - expr *rep = kv.m_value; - expr_ref val(m); - expr *u = nullptr; - if (!mev.eval(rep, val)) continue; - if (val2rep.find(val, u)) { - res.push_back(m.mk_eq(u, rep)); - } - else { - val2rep.insert(val, rep); - } - } - - // TBD: optimize further based on implied values (e.g., - // some literals are forced to be true/false) and based on - // unique_values (e.g., (x=1 & y=1) does not require - // (x!=y) to be added - ptr_buffer reps; - for (auto &kv : val2rep) { - expr *rep = kv.m_value; - if (!m.is_unique_value(rep)) - reps.push_back(kv.m_value); - } - - if (reps.size() <= 1) return; - - // -- sort representatives, call mk_distinct on any range - // -- of the same sort longer than 1 - std::sort(reps.data(), reps.data() + reps.size(), sort_lt_proc()); - unsigned i = 0; - unsigned sz = reps.size(); - while (i < sz) { - sort* last_sort = res.get(i)->get_sort(); - unsigned j = i + 1; - while (j < sz && last_sort == reps.get(j)->get_sort()) {++j;} - if (j - i == 2) { - expr_ref d(m); - d = mk_neq(m, reps.get(i), reps.get(i+1)); - if (!m.is_true(d)) res.push_back(d); - } - else if (j - i > 2) - res.push_back(m.mk_distinct(j - i, reps.data() + i)); - i = j; - } - TRACE("qe", tout << "after distinct: " << res << "\n";); - } - - std::ostream& display(std::ostream& out) const { - m_tg.display(out); - out << "term2app:\n"; - for (auto const& kv : m_term2app) { - out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; - } - out << "root2rep:\n"; - for (auto const& kv : m_root2rep) { - out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; - } - return out; - } - - public: - projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_rewriter(m), m_pinned(m) {} - - void add_term2app(term const& t, expr* a) { - m_term2app.insert(t.get_id(), a); - } - - void del_term2app(term const& t) { - m_term2app.remove(t.get_id()); - } - - bool find_term2app(term const& t, expr*& r) { - return m_term2app.find(t.get_id(), r); - } - - expr* find_term2app(term const& t) { - expr* r = nullptr; - find_term2app(t, r); - return r; - } - - bool in_term2app(term const& t) { - return m_term2app.contains(t.get_id()); - } - - void set_model(model &mdl) { m_model = &mdl; } - - void reset() { - m_tg.reset_marks(); - m_term2app.reset(); - m_root2rep.reset(); - m_pinned.reset(); - m_model.reset(); - } - - expr_ref_vector project() { - expr_ref_vector res(m); - purify(); - lits2pure(res); - mk_distinct(res); - reset(); - return res; - } - - expr_ref_vector get_ackerman_disequalities() { - expr_ref_vector res(m); - purify(); - lits2pure(res); - unsigned sz = res.size(); - mk_distinct(res); - reset(); - unsigned j = 0; - for (unsigned i = sz; i < res.size(); ++i) { - res[j++] = res.get(i); - } - res.shrink(j); - return res; - } - - expr_ref_vector solve() { - expr_ref_vector res(m); - purify(); - solve_core(); - mk_lits(res); - mk_unpure_equalities(res); - reset(); - return res; - } - - vector get_partition(model& mdl, bool include_bool) { - vector result; - expr_ref_vector pinned(m); - obj_map pid; - auto insert_val = [&](expr* a, expr* val) { - unsigned p = 0; - // NB. works for simple domains Integers, Rationals, - // but not for algebraic numerals. - if (!pid.find(val, p)) { - p = pid.size(); - pid.insert(val, p); - pinned.push_back(val); - result.push_back(expr_ref_vector(m)); - } - result[p].push_back(a); - }; - model::scoped_model_completion _smc(mdl, true); - for (term *t : m_tg.m_terms) { - expr* a = t->get_expr(); - if (!is_app(a)) - continue; - if (m.is_bool(a) && !include_bool) - continue; - expr_ref val = mdl(a); - insert_val(a, val); - } - - return result; - } - - expr_ref_vector shared_occurrences(family_id fid) { - expr_ref_vector result(m); - for (term *t : m_tg.m_terms) { - expr* e = t->get_expr(); - if (e->get_sort()->get_family_id() != fid) continue; - for (term * p : term::parents(t->get_root())) { - expr* pe = p->get_expr(); - if (!is_app(pe)) continue; - if (to_app(pe)->get_family_id() == fid) continue; - if (to_app(pe)->get_family_id() == m.get_basic_family_id()) continue; - result.push_back(e); - break; - } - } - return result; - } - - void purify() { - // - propagate representatives up over parents. - // use work-list + marking to propagate. - // - produce equalities over represented classes. - // - produce other literals over represented classes - // (walk disequalities in m_lits and represent - // lhs/rhs over decls or excluding decls) - - ptr_vector worklist; - for (term * t : m_tg.m_terms) { + void solve_core() { + ptr_vector worklist; + for (term *t : m_tg.m_terms) { + // skip pure terms + if (!in_term2app(*t) && !t->is_eq_or_neq()) { worklist.push_back(t); t->set_mark(true); } - // traverse worklist in order of depth. - term_depth td; - std::sort(worklist.begin(), worklist.end(), td); - - for (unsigned i = 0; i < worklist.size(); ++i) { - term* t = worklist[i]; - t->set_mark(false); - if (in_term2app(*t)) - continue; - if (!t->is_theory() && is_projected(*t)) - continue; - - expr* pure = mk_pure(*t); - if (!pure) continue; - - add_term2app(*t, pure); - TRACE("qe_verbose", tout << "purified " << *t << " " << mk_pp(pure, m) << "\n";); - expr* rep = nullptr; // ensure that the root has a representative - m_root2rep.find(t->get_root().get_id(), rep); - - // update rep with pure if it is better - if (pure != rep && is_better_rep(pure, rep)) { - m_root2rep.insert(t->get_root().get_id(), pure); - for (term * p : term::parents(t->get_root())) { - del_term2app(*p); - if (!p->is_marked()) { - p->set_mark(true); - worklist.push_back(p); - } - } - } - } - - // Here we could also walk equivalence classes that - // contain interpreted values by sort and extract - // disequalities between non-unique value - // representatives. these disequalities are implied - // and can be mined using other means, such as theory - // aware core minimization - m_tg.reset_marks(); - TRACE("qe", display(tout << "after purify\n");); } + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); - }; + for (unsigned i = 0; i < worklist.size(); ++i) { + term *t = worklist[i]; + t->set_mark(false); + if (in_term2app(*t)) continue; - void term_graph::set_vars(func_decl_ref_vector const& decls, bool exclude) { - m_is_var.set_decls(decls, exclude); - } + expr *pure = mk_pure(*t); + if (!pure) continue; - expr_ref_vector term_graph::project() { - // reset solved vars so that they are not considered pure by projector - m_is_var.reset_solved(); - term_graph::projector p(*this); - return p.project(); - } + add_term2app(*t, pure); + expr *rep = nullptr; + // ensure that the root has a representative + m_root2rep.find(t->get_root().get_id(), rep); - expr_ref_vector term_graph::project(model &mdl) { - m_is_var.reset_solved(); - term_graph::projector p(*this); - p.set_model(mdl); - return p.project(); - } - - expr_ref_vector term_graph::solve() { - // reset solved vars so that they are not considered pure by projector - m_is_var.reset_solved(); - term_graph::projector p(*this); - return p.solve(); - } - - expr_ref_vector term_graph::get_ackerman_disequalities() { - m_is_var.reset_solved(); - dealloc(m_projector); - m_projector = alloc(term_graph::projector, *this); - return m_projector->get_ackerman_disequalities(); - } - - vector term_graph::get_partition(model& mdl) { - dealloc(m_projector); - m_projector = alloc(term_graph::projector, *this); - return m_projector->get_partition(mdl, false); - } - - expr_ref_vector term_graph::shared_occurrences(family_id fid) { - term_graph::projector p(*this); - return p.shared_occurrences(fid); - } - - void term_graph::add_model_based_terms(model& mdl, expr_ref_vector const& terms) { - for (expr* t : terms) { - internalize_term(t); - } - m_is_var.reset_solved(); - - SASSERT(!m_projector); - m_projector = alloc(term_graph::projector, *this); - - // retrieve partition of terms - vector equivs = m_projector->get_partition(mdl, true); - - // merge term graph on equal terms. - for (auto const& cs : equivs) { - term* t0 = get_term(cs[0]); - for (unsigned i = 1; i < cs.size(); ++i) { - merge(*t0, *get_term(cs[i])); - } - } - TRACE("qe", - for (auto & es : equivs) { - tout << "equiv: "; - for (expr* t : es) tout << expr_ref(t, m) << " "; - tout << "\n"; - } - display(tout);); - // create representatives for shared/projected variables. - m_projector->set_model(mdl); - m_projector->purify(); - - } - - expr* term_graph::rep_of(expr* e) { - SASSERT(m_projector); - term* t = get_term(e); - SASSERT(t && "only get representatives"); - return m_projector->find_term2app(*t); - } - - expr_ref_vector term_graph::dcert(model& mdl, expr_ref_vector const& lits) { - TRACE("qe", tout << "dcert " << lits << "\n";); - struct pair_t { - expr* a, *b; - pair_t(): a(nullptr), b(nullptr) {} - pair_t(expr* _a, expr* _b):a(_a), b(_b) { - if (a->get_id() > b->get_id()) std::swap(a, b); - } - struct hash { - unsigned operator()(pair_t const& p) const { return mk_mix(p.a ? p.a->hash() : 0, p.b ? p.b->hash() : 0, 1); } - }; - struct eq { - bool operator()(pair_t const& a, pair_t const& b) const { return a.a == b.a && a.b == b.b; } - }; - }; - hashtable diseqs; - expr_ref_vector result(m); - add_lits(lits); - svector todo; - - for (expr* e : lits) { - expr* ne, *a, *b; - if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) { - diseqs.insert(pair_t(a, b)); - } - else if (is_uninterp(e)) { - diseqs.insert(pair_t(e, m.mk_false())); - } - else if (m.is_not(e, ne) && is_uninterp(ne)) { - diseqs.insert(pair_t(ne, m.mk_true())); - } - } - for (auto& p : diseqs) todo.push_back(p); - - auto const partitions = get_partition(mdl); - obj_map term2pid; - unsigned id = 0; - for (auto const& vec : partitions) { - for (expr* e : vec) term2pid.insert(e, id); - ++id; - } - expr_ref_vector empty(m); - auto partition_of = [&](expr* e) { - unsigned pid; - if (!term2pid.find(e, pid)) - return empty; - return partitions[pid]; - }; - auto in_table = [&](expr* a, expr* b) { - return diseqs.contains(pair_t(a, b)); - }; - auto same_function = [](expr* a, expr* b) { - return is_app(a) && is_app(b) && - to_app(a)->get_decl() == to_app(b)->get_decl() && to_app(a)->get_family_id() == null_family_id; - }; - - // make sure that diseqs is closed under function applications - // of uninterpreted functions. - for (unsigned idx = 0; idx < todo.size(); ++idx) { - auto p = todo[idx]; - for (expr* t1 : partition_of(p.a)) { - for (expr* t2 : partition_of(p.b)) { - if (same_function(t1, t2)) { - unsigned sz = to_app(t1)->get_num_args(); - bool found = false; - pair_t q(t1, t2); - for (unsigned i = 0; i < sz; ++i) { - expr* arg1 = to_app(t1)->get_arg(i); - expr* arg2 = to_app(t2)->get_arg(i); - if (mdl(arg1) == mdl(t2)) { - continue; - } - if (in_table(arg1, arg2)) { - found = true; - break; - } - q = pair_t(arg1, arg2); - } - if (!found) { - diseqs.insert(q); - todo.push_back(q); - result.push_back(m.mk_not(m.mk_eq(q.a, q.b))); - } + if (!rep) { + m_root2rep.insert(t->get_root().get_id(), pure); + for (term *p : term::parents(t->get_root())) { + SASSERT(!in_term2app(*p)); + if (!p->is_marked()) { + p->set_mark(true); + worklist.push_back(p); } } } } - for (auto const& terms : partitions) { - expr* a = nullptr; - for (expr* b : terms) { - if (is_uninterp(b)) { - if (a) - result.push_back(m.mk_eq(a, b)); - else - a = b; + m_tg.reset_marks(); + } + + bool find_app(term &t, expr *&res) { + return find_term2app(t, res) || + m_root2rep.find(t.get_root().get_id(), res); + } + + bool find_app(expr *lit, expr *&res) { + term const *t = m_tg.get_term(lit); + return find_term2app(*t, res) || + m_root2rep.find(t->get_root().get_id(), res); + } + + void mk_lits(expr_ref_vector &res) { + expr *e = nullptr; + for (auto *lit : m_tg.m_lits) { + if (!m.is_eq(lit) && find_app(lit, e)) res.push_back(e); + } + TRACE("qe", tout << "literals: " << res << "\n";); + } + + void lits2pure(expr_ref_vector &res) { + expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr; + for (auto *lit : m_tg.m_lits) { + if (m.is_eq(lit, e1, e2)) { + if (find_app(e1, p1) && find_app(e2, p2)) { + if (p1 != p2) res.push_back(m.mk_eq(p1, p2)); + } + else + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + else if (m.is_distinct(lit)) { + ptr_buffer diff; + for (expr *arg : *to_app(lit)) + if (find_app(arg, p1)) diff.push_back(p1); + if (diff.size() > 1) + res.push_back(m.mk_distinct(diff.size(), diff.data())); + else + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + else if (find_app(lit, p1)) + res.push_back(p1); + else + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + remove_duplicates(res); + TRACE("qe", tout << "literals: " << res << "\n";); + } + + void remove_duplicates(expr_ref_vector &v) { + obj_hashtable seen; + unsigned j = 0; + for (expr *e : v) { + if (!seen.contains(e)) { + v[j++] = e; + seen.insert(e); + } + } + v.shrink(j); + } + + vector> m_decl2terms; // terms that use function f + ptr_vector m_decls; + + void collect_decl2terms() { + // Collect the projected function symbols. + m_decl2terms.reset(); + m_decls.reset(); + for (term *t : m_tg.m_terms) { + if (t->is_eq_or_neq()) continue; + expr *e = t->get_expr(); + if (!is_app(e)) continue; + if (!is_projected(*t)) continue; + app *a = to_app(e); + func_decl *d = a->get_decl(); + if (d->get_arity() == 0) continue; + unsigned id = d->get_small_id(); + m_decl2terms.reserve(id + 1); + if (m_decl2terms[id].empty()) m_decls.push_back(d); + m_decl2terms[id].push_back(t); + } + } + + void args_are_distinct(expr_ref_vector &res) { + // + // for each projected function that occurs + // (may occur) in multiple congruence classes, + // produce assertions that non-congruent arguments + // are distinct. + // + for (func_decl *d : m_decls) { + unsigned id = d->get_small_id(); + ptr_vector const &terms = m_decl2terms[id]; + if (terms.size() <= 1) continue; + unsigned arity = d->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + obj_hashtable roots, root_vals; + expr_ref_vector pinned(m); + for (term *t : terms) { + expr *arg = to_app(t->get_expr())->get_arg(i); + term const &root = m_tg.get_term(arg)->get_root(); + expr *r = root.get_expr(); + // if a model is given, then use the equivalence class + // induced by the model. Otherwise, use the congruence + // class. + if (m_model) { + expr_ref tmp(m); + tmp = (*m_model)(r); + if (!root_vals.contains(tmp)) { + root_vals.insert(tmp); + roots.insert(r); + pinned.push_back(tmp); + } + } + else { roots.insert(r); } + } + if (roots.size() > 1) { + ptr_buffer args; + for (expr *r : roots) { args.push_back(r); } + TRACE("qe", tout << "function: " << d->get_name() << "\n";); + res.push_back(m.mk_distinct(args.size(), args.data())); } } } - TRACE("qe", tout << result << "\n";); + } + + void mk_distinct(expr_ref_vector &res) { + collect_decl2terms(); + args_are_distinct(res); + TRACE("qe", tout << res << "\n";); + } + + void mk_pure_equalities(const term &t, expr_ref_vector &res) { + SASSERT(t.is_root()); + expr *rep = nullptr; + if (!m_root2rep.find(t.get_id(), rep)) return; + obj_hashtable members; + members.insert(rep); + term const *r = &t; + do { + expr *member = nullptr; + if (find_term2app(*r, member) && !members.contains(member)) { + res.push_back(m.mk_eq(rep, member)); + members.insert(member); + } + r = &r->get_next(); + } + while (r != &t); + } + + bool is_projected(const term &t) { return m_tg.m_is_var(t); } + + void mk_unpure_equalities(const term &t, expr_ref_vector &res) { + expr *rep = nullptr; + if (!m_root2rep.find(t.get_id(), rep)) return; + obj_hashtable members; + members.insert(rep); + term const *r = &t; + do { + expr *member = mk_pure(*r); + SASSERT(member); + if (!members.contains(member) && + (!is_projected(*r) || !is_solved_eq(rep, member))) { + res.push_back(m.mk_eq(rep, member)); + members.insert(member); + } + r = &r->get_next(); + } + while (r != &t); + } + + template void mk_equalities(expr_ref_vector &res) { + for (term *t : m_tg.m_terms) { + if (t->is_eq_or_neq()) continue; + if (!t->is_root()) continue; + if (!m_root2rep.contains(t->get_id())) continue; + if (pure) + mk_pure_equalities(*t, res); + else + mk_unpure_equalities(*t, res); + } + TRACE("qe", tout << "literals: " << res << "\n";); + } + + void mk_pure_equalities(expr_ref_vector &res) { mk_equalities(res); } + + void mk_unpure_equalities(expr_ref_vector &res) { + mk_equalities(res); + } + + // TBD: generalize for also the case of a (:var n) + bool is_solved_eq(expr *lhs, expr *rhs) { + return is_uninterp_const(rhs) && !occurs(rhs, lhs); + } + + /// Add equalities and disequalities for all pure representatives + /// based on their equivalence in the model + void model_complete(expr_ref_vector &res) { + if (!m_model) return; + obj_map val2rep; + model_evaluator mev(*m_model); + for (auto &kv : m_root2rep) { + expr *rep = kv.m_value; + expr_ref val(m); + expr *u = nullptr; + if (!mev.eval(rep, val)) continue; + if (val2rep.find(val, u)) { res.push_back(m.mk_eq(u, rep)); } + else { val2rep.insert(val, rep); } + } + + // TBD: optimize further based on implied values (e.g., + // some literals are forced to be true/false) and based on + // unique_values (e.g., (x=1 & y=1) does not require + // (x!=y) to be added + ptr_buffer reps; + for (auto &kv : val2rep) { + expr *rep = kv.m_value; + if (!m.is_unique_value(rep)) reps.push_back(kv.m_value); + } + + if (reps.size() <= 1) return; + + // -- sort representatives, call mk_distinct on any range + // -- of the same sort longer than 1 + std::sort(reps.data(), reps.data() + reps.size(), sort_lt_proc()); + unsigned i = 0; + unsigned sz = reps.size(); + while (i < sz) { + sort *last_sort = res.get(i)->get_sort(); + unsigned j = i + 1; + while (j < sz && last_sort == reps.get(j)->get_sort()) { ++j; } + if (j - i == 2) { + expr_ref d(m); + d = mk_neq(m, reps.get(i), reps.get(i + 1)); + if (!m.is_true(d)) res.push_back(d); + } + else if (j - i > 2) + res.push_back(m.mk_distinct(j - i, reps.data() + i)); + i = j; + } + TRACE("qe", tout << "after distinct: " << res << "\n";); + } + + std::ostream &display(std::ostream &out) const { + m_tg.display(out); + out << "term2app:\n"; + for (auto const &kv : m_term2app) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } + out << "root2rep:\n"; + for (auto const &kv : m_root2rep) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } + return out; + } + + public: + projector(term_graph &tg) + : m_tg(tg), m(m_tg.m), m_rewriter(m), m_pinned(m) {} + + void add_term2app(term const &t, expr *a) { + m_term2app.insert(t.get_id(), a); + } + + void del_term2app(term const &t) { m_term2app.remove(t.get_id()); } + + bool find_term2app(term const &t, expr *&r) { + return m_term2app.find(t.get_id(), r); + } + + expr *find_term2app(term const &t) { + expr *r = nullptr; + find_term2app(t, r); + return r; + } + + bool in_term2app(term const &t) { return m_term2app.contains(t.get_id()); } + + void set_model(model &mdl) { m_model = &mdl; } + + void reset() { + m_tg.reset_marks(); + m_term2app.reset(); + m_root2rep.reset(); + m_pinned.reset(); + m_model.reset(); + } + + expr_ref_vector project() { + expr_ref_vector res(m); + purify(); + lits2pure(res); + mk_distinct(res); + reset(); + return res; + } + + expr_ref_vector get_ackerman_disequalities() { + expr_ref_vector res(m); + purify(); + lits2pure(res); + unsigned sz = res.size(); + mk_distinct(res); + reset(); + unsigned j = 0; + for (unsigned i = sz; i < res.size(); ++i) { res[j++] = res.get(i); } + res.shrink(j); + return res; + } + + expr_ref_vector solve() { + expr_ref_vector res(m); + purify(); + solve_core(); + mk_lits(res); + mk_unpure_equalities(res); + reset(); + return res; + } + + vector get_partition(model &mdl, bool include_bool) { + vector result; + expr_ref_vector pinned(m); + obj_map pid; + auto insert_val = [&](expr *a, expr *val) { + unsigned p = 0; + // NB. works for simple domains Integers, Rationals, + // but not for algebraic numerals. + if (!pid.find(val, p)) { + p = pid.size(); + pid.insert(val, p); + pinned.push_back(val); + result.push_back(expr_ref_vector(m)); + } + result[p].push_back(a); + }; + model::scoped_model_completion _smc(mdl, true); + for (term *t : m_tg.m_terms) { + if (t->is_eq_or_neq()) continue; + expr *a = t->get_expr(); + if (!is_app(a)) continue; + if (m.is_bool(a) && !include_bool) continue; + expr_ref val = mdl(a); + insert_val(a, val); + } return result; } + expr_ref_vector shared_occurrences(family_id fid) { + expr_ref_vector result(m); + for (term *t : m_tg.m_terms) { + if (t->is_eq_or_neq()) continue; + expr *e = t->get_expr(); + if (e->get_sort()->get_family_id() != fid) continue; + for (term *p : term::parents(t->get_root())) { + expr *pe = p->get_expr(); + if (!is_app(pe)) continue; + if (to_app(pe)->get_family_id() == fid) continue; + if (to_app(pe)->get_family_id() == m.get_basic_family_id()) + continue; + result.push_back(e); + break; + } + } + return result; + } + + void purify() { + // - propagate representatives up over parents. + // use work-list + marking to propagate. + // - produce equalities over represented classes. + // - produce other literals over represented classes + // (walk disequalities in m_lits and represent + // lhs/rhs over decls or excluding decls) + + ptr_vector worklist; + for (term *t : m_tg.m_terms) { + if (t->is_eq_or_neq()) continue; + worklist.push_back(t); + t->set_mark(true); + } + // traverse worklist in order of depth. + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); + + for (unsigned i = 0; i < worklist.size(); ++i) { + term *t = worklist[i]; + t->set_mark(false); + if (in_term2app(*t)) continue; + if (!t->is_theory() && is_projected(*t)) continue; + + expr *pure = mk_pure(*t); + if (!pure) continue; + + add_term2app(*t, pure); + TRACE("qe_verbose", + tout << "purified " << *t << " " << mk_pp(pure, m) << "\n";); + expr *rep = nullptr; // ensure that the root has a representative + m_root2rep.find(t->get_root().get_id(), rep); + + // update rep with pure if it is better + if (pure != rep && is_better_rep(pure, rep)) { + m_root2rep.insert(t->get_root().get_id(), pure); + for (term *p : term::parents(t->get_root())) { + del_term2app(*p); + if (!p->is_marked()) { + p->set_mark(true); + worklist.push_back(p); + } + } + } + } + + // Here we could also walk equivalence classes that + // contain interpreted values by sort and extract + // disequalities between non-unique value + // representatives. these disequalities are implied + // and can be mined using other means, such as theory + // aware core minimization + m_tg.reset_marks(); + TRACE("qe", display(tout << "after purify\n");); + } +}; + +// produce a quantifier reduction of the formula stored in the term graph +// removes from `vars` the variables that have a ground representative +// modifies `vars` to keep the variables that could not be eliminated +void term_graph::qel(app_ref_vector &vars, expr_ref &fml, + std::function *non_core) { + unsigned i = 0; + for (auto v : vars) { + if (is_internalized(v)) { vars[i++] = v; } + } + vars.shrink(i); + pick_repr(); + refine_repr(); + + expr_ref_vector lits(m); + to_lits_qe_lite(lits, non_core); + if (lits.size() == 0) + fml = m.mk_true(); + else if (lits.size() == 1) + fml = lits[0].get(); + else + fml = m.mk_and(lits); + + // Remove all variables that are do not appear in the formula + expr_sparse_mark mark; + mark_all_sub_expr marker(mark); + quick_for_each_expr(marker, fml); + i = 0; + for (auto v : vars) { + if (mark.is_marked(v)) vars[i++] = v; + } + vars.shrink(i); } + +void term_graph::set_vars(func_decl_ref_vector const &decls, bool exclude) { + m_is_var.set_decls(decls, exclude); +} + +void term_graph::set_vars(app_ref_vector const &vars, bool exclude) { + m_is_var.set_decls(vars, exclude); +} + +void term_graph::add_vars(app_ref_vector const &vars) { + m_is_var.add_decls(vars); +} + +void term_graph::add_var(app *var) { m_is_var.add_decl(var); } + +expr_ref_vector term_graph::project() { + // reset solved vars so that they are not considered pure by projector + m_is_var.reset_solved(); + term_graph::projector p(*this); + return p.project(); +} + +expr_ref_vector term_graph::project(model &mdl) { + m_is_var.reset_solved(); + term_graph::projector p(*this); + p.set_model(mdl); + return p.project(); +} + +expr_ref_vector term_graph::solve() { + // reset solved vars so that they are not considered pure by projector + m_is_var.reset_solved(); + term_graph::projector p(*this); + return p.solve(); +} + +expr_ref_vector term_graph::get_ackerman_disequalities() { + m_is_var.reset_solved(); + dealloc(m_projector); + m_projector = alloc(term_graph::projector, *this); + return m_projector->get_ackerman_disequalities(); +} + +vector term_graph::get_partition(model &mdl) { + dealloc(m_projector); + m_projector = alloc(term_graph::projector, *this); + return m_projector->get_partition(mdl, false); +} + +expr_ref_vector term_graph::shared_occurrences(family_id fid) { + term_graph::projector p(*this); + return p.shared_occurrences(fid); +} + +void term_graph::add_model_based_terms(model &mdl, + expr_ref_vector const &terms) { + for (expr *t : terms) { internalize_term(t); } + m_is_var.reset_solved(); + + SASSERT(!m_projector); + m_projector = alloc(term_graph::projector, *this); + + // retrieve partition of terms + vector equivs = m_projector->get_partition(mdl, true); + + // merge term graph on equal terms. + for (auto const &cs : equivs) { + term *t0 = get_term(cs[0]); + for (unsigned i = 1; i < cs.size(); ++i) { + merge(*t0, *get_term(cs[i])); + } + } + TRACE( + "qe", for (auto &es + : equivs) { + tout << "equiv: "; + for (expr *t : es) tout << expr_ref(t, m) << " "; + tout << "\n"; + } display(tout);); + // create representatives for shared/projected variables. + m_projector->set_model(mdl); + m_projector->purify(); +} + +expr *term_graph::rep_of(expr *e) { + SASSERT(m_projector); + term *t = get_term(e); + SASSERT(t && "only get representatives"); + return m_projector->find_term2app(*t); +} + +expr_ref_vector term_graph::dcert(model &mdl, expr_ref_vector const &lits) { + TRACE("qe", tout << "dcert " << lits << "\n";); + struct pair_t { + expr *a, *b; + pair_t() : a(nullptr), b(nullptr) {} + pair_t(expr *_a, expr *_b) : a(_a), b(_b) { + if (a->get_id() > b->get_id()) std::swap(a, b); + } + struct hash { + unsigned operator()(pair_t const &p) const { + return mk_mix(p.a ? p.a->hash() : 0, p.b ? p.b->hash() : 0, 1); + } + }; + struct eq { + bool operator()(pair_t const &a, pair_t const &b) const { + return a.a == b.a && a.b == b.b; + } + }; + }; + hashtable diseqs; + expr_ref_vector result(m); + add_lits(lits); + svector todo; + + for (expr *e : lits) { + expr *ne, *a, *b; + if (m.is_not(e, ne) && m.is_eq(ne, a, b) && + (is_uninterp(a) || is_uninterp(b))) { + diseqs.insert(pair_t(a, b)); + } + else if (is_uninterp(e)) { diseqs.insert(pair_t(e, m.mk_false())); } + else if (m.is_not(e, ne) && is_uninterp(ne)) { + diseqs.insert(pair_t(ne, m.mk_true())); + } + } + for (auto &p : diseqs) todo.push_back(p); + + auto const partitions = get_partition(mdl); + obj_map term2pid; + unsigned id = 0; + for (auto const &vec : partitions) { + for (expr *e : vec) term2pid.insert(e, id); + ++id; + } + expr_ref_vector empty(m); + auto partition_of = [&](expr *e) { + unsigned pid; + if (!term2pid.find(e, pid)) return empty; + return partitions[pid]; + }; + auto in_table = [&](expr *a, expr *b) { + return diseqs.contains(pair_t(a, b)); + }; + auto same_function = [](expr *a, expr *b) { + return is_app(a) && is_app(b) && + to_app(a)->get_decl() == to_app(b)->get_decl() && + to_app(a)->get_family_id() == null_family_id; + }; + + // make sure that diseqs is closed under function applications + // of uninterpreted functions. + for (unsigned idx = 0; idx < todo.size(); ++idx) { + auto p = todo[idx]; + for (expr *t1 : partition_of(p.a)) { + for (expr *t2 : partition_of(p.b)) { + if (same_function(t1, t2)) { + unsigned sz = to_app(t1)->get_num_args(); + bool found = false; + pair_t q(t1, t2); + for (unsigned i = 0; i < sz; ++i) { + expr *arg1 = to_app(t1)->get_arg(i); + expr *arg2 = to_app(t2)->get_arg(i); + if (mdl(arg1) == mdl(t2)) { continue; } + if (in_table(arg1, arg2)) { + found = true; + break; + } + q = pair_t(arg1, arg2); + } + if (!found) { + diseqs.insert(q); + todo.push_back(q); + result.push_back(m.mk_not(m.mk_eq(q.a, q.b))); + } + } + } + } + } + for (auto const &terms : partitions) { + expr *a = nullptr; + for (expr *b : terms) { + if (is_uninterp(b)) { + if (a) + result.push_back(m.mk_eq(a, b)); + else + a = b; + } + } + } + TRACE("qe", tout << result << "\n";); + return result; +} + +void term_graph::cground_percolate_up(term *t) { + SASSERT(t->is_class_gr()); + term *it = t; + // there is a cgr term in all ground classes + while (!it->is_cgr()) { + it = &it->get_next(); + SASSERT(it != t); + } + + ptr_vector todo; + todo.push_back(it); + cground_percolate_up(todo); +} + +void term_graph::cground_percolate_up(ptr_vector &todo) { + term *t; + + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + t->set_cgr(true); + t->set_class_gr(true); + for (auto p : term::parents(t->get_root())) + if (!p->is_cgr() && p->all_children_ground()) todo.push_back(p); + } +} + +void term_graph::compute_cground() { + for (auto t : m_terms) { + t->set_cgr(false); + t->set_class_gr(false); + } + ptr_vector todo; + for (auto t : m_terms) { + if (t->is_gr()) { todo.push_back(t); } + } + cground_percolate_up(todo); + DEBUG_CODE(for (auto t + : m_terms) { + bool isclsg = true; + for (auto c : term::children(t)) isclsg &= c->is_class_gr(); + SASSERT(t->deg() == 0 || !isclsg || t->is_cgr()); + SASSERT(t->deg() == 0 || isclsg || !t->is_cgr()); + }); +} +} // namespace mbp diff --git a/src/qe/mbp/mbp_term_graph.h b/src/qe/mbp/mbp_term_graph.h index 37d1e7b8d..1300034a6 100644 --- a/src/qe/mbp/mbp_term_graph.h +++ b/src/qe/mbp/mbp_term_graph.h @@ -12,6 +12,12 @@ Abstract: Author: Arie Gurfinkel + Hari Govind V K (hgvk94) + Isabel Garcia (igcontreras) + +Revision History: + + Added implementation of qe_lite using term graph Notes: @@ -19,138 +25,237 @@ Notes: #pragma once #include "ast/ast.h" +#include "ast/expr_functors.h" #include "ast/is_variable_test.h" -#include "util/plugin_manager.h" -#include "qe/mbp/mbp_solve_plugin.h" #include "model/model.h" +#include "qe/mbp/mbp_solve_plugin.h" +#include "util/plugin_manager.h" namespace mbp { +namespace is_ground_ns { +struct proc; +struct found; +} // namespace is_ground_ns +class term; - class term; +class term_graph { + class projector; + friend struct is_ground_ns::proc; + friend struct is_ground_ns::found; - class term_graph { - class projector; + class is_variable_proc : public ::is_variable_proc { + bool m_exclude; + obj_hashtable m_decls, m_solved; - class is_variable_proc : public ::is_variable_proc { - bool m_exclude; - obj_hashtable m_decls, m_solved; - public: - bool operator()(const expr *e) const override; - bool operator()(const term &t) const; - - void set_decls(const func_decl_ref_vector &decls, bool exclude); - void mark_solved(const expr *e); - void reset_solved() {m_solved.reset();} - void reset() {m_decls.reset(); m_solved.reset(); m_exclude = true;} - }; - - struct term_hash { unsigned operator()(term const* t) const; }; - struct term_eq { bool operator()(term const* a, term const* b) const; }; - ast_manager & m; - ptr_vector m_terms; - expr_ref_vector m_lits; // NSB: expr_ref_vector? - u_map m_app2term; - ast_ref_vector m_pinned; - projector* m_projector; - u_map m_term2app; - plugin_manager m_plugins; - ptr_hashtable m_cg_table; - vector> m_merge; - - term_graph::is_variable_proc m_is_var; - void merge(term &t1, term &t2); - void merge_flush(); - - term *mk_term(expr *t); - term *get_term(expr *t); - - term *internalize_term(expr *t); - void internalize_eq(expr *a1, expr *a2); - void internalize_lit(expr *lit); - - bool is_internalized(expr *a); - - bool term_lt(term const &t1, term const &t2); - void pick_root (term &t); - void pick_roots(); - - void reset_marks(); - bool marks_are_clear(); - - expr* mk_app_core(expr* a); - expr_ref mk_app(term const &t); - expr* mk_pure(term& t); - expr_ref mk_app(expr *a); - void mk_equalities(term const &t, expr_ref_vector &out); - void mk_all_equalities(term const &t, expr_ref_vector &out); - void display(std::ostream &out); - - bool is_pure_def(expr* atom, expr *& v); - - public: - term_graph(ast_manager &m); - ~term_graph(); - - void set_vars(func_decl_ref_vector const& decls, bool exclude); - - ast_manager& get_ast_manager() const { return m;} - - void add_lit(expr *lit); - void add_lits(expr_ref_vector const &lits) { for (expr* e : lits) add_lit(e); } - void add_eq(expr* a, expr* b) { internalize_eq(a, b); } - - void reset(); - - // deprecate? - void to_lits(expr_ref_vector &lits, bool all_equalities = false); - expr_ref to_expr(); - - /** - * Return literals obtained by projecting added literals - * onto the vocabulary of decls (if exclude is false) or outside the - * vocabulary of decls (if exclude is true). - */ - expr_ref_vector project(); - expr_ref_vector solve(); - expr_ref_vector project(model &mdl); - - /** - * Return disequalities to ensure that disequalities between - * excluded functions are preserved. - * For example if f(a) = b, f(c) = d, and b and d are not - * congruent, then produce the disequality a != c. - */ - expr_ref_vector get_ackerman_disequalities(); - - /** - * Produce model-based disequality - * certificate corresponding to - * definition in BGVS 2020. - * A disequality certificate is a reduced set of - * disequalities, true under mdl, such that the literals - * can be satisfied when non-shared symbols are projected. - */ - expr_ref_vector dcert(model& mdl, expr_ref_vector const& lits); - - /** - * Produce a model-based partition. - */ - vector get_partition(model& mdl); - - /** - * Extract shared occurrences of terms whose sort are - * fid, but appear in a context that is not fid. - * for example f(x + y) produces the shared occurrence - * x + y when f is uninterpreted and x + y has sort Int or Real. - */ - expr_ref_vector shared_occurrences(family_id fid); - - /** - * Map expression that occurs in added literals into representative if it exists. - */ - void add_model_based_terms(model& mdl, expr_ref_vector const& terms); - expr* rep_of(expr* e); + public: + bool operator()(const expr *e) const override; + bool operator()(const term &t) const; + void set_decls(const func_decl_ref_vector &decls, bool exclude); + void set_decls(const app_ref_vector &vars, bool exclude); + void add_decls(const app_ref_vector &vars); + void add_decl(app *var); + void mark_solved(const expr *e); + void reset_solved() { m_solved.reset(); } + void reset() { + m_decls.reset(); + m_solved.reset(); + m_exclude = true; + } + bool contains(func_decl *f) { return m_decls.contains(f) == m_exclude; } }; -} + class is_non_core : public i_expr_pred { + std::function *m_non_core; + + public: + is_non_core(std::function *nc) : m_non_core(nc) {} + bool operator()(expr *n) override { + if (m_non_core == nullptr) return false; + return (*m_non_core)(n); + } + }; + + struct term_hash { + unsigned operator()(term const *t) const; + }; + struct term_eq { + bool operator()(term const *a, term const *b) const; + }; + ast_manager &m; + ptr_vector m_terms; + expr_ref_vector m_lits; // NSB: expr_ref_vector? + u_map m_app2term; + ast_ref_vector m_pinned; + projector *m_projector; + bool m_explicit_eq; + bool m_repick_repr; + u_map + m_term2app; // any representative change invalidates this cache + plugin_manager m_plugins; + ptr_hashtable m_cg_table; + vector> m_merge; + + term_graph::is_variable_proc m_is_var; + + void merge(term &t1, term &t2); + void merge_flush(); + + term *mk_term(expr *t); + term *get_term(expr *t); + term *get_term(func_decl *f); + + term *internalize_term(expr *t); + void internalize_eq(expr *a1, expr *a2); + void internalize_lit(expr *lit); + void internalize_distinct(expr *d); + void internalize_deq(expr *a1, expr *a2); + + bool is_internalized(expr *a); + bool is_ground(expr *e); + + bool term_lt(term const &t1, term const &t2); + void pick_repr_percolate_up(ptr_vector &todo); + void pick_repr_class(term *t); + void pick_repr(); + + void reset_marks(); + void reset_marks2(); + bool marks_are_clear(); + + expr *mk_app_core(expr *a); + expr_ref mk_app(term &t); + expr *mk_pure(term &t); + expr_ref mk_app(expr *a); + void mk_equalities(term &t, expr_ref_vector &out); + void mk_all_equalities(term &t, expr_ref_vector &out); + void mk_qe_lite_equalities(term &t, expr_ref_vector &out, + check_pred ¬_in_core); + void display(std::ostream &out); + + bool is_pure_def(expr *atom, expr *&v); + void cground_percolate_up(ptr_vector &); + void cground_percolate_up(term *t); + void compute_cground(); + + public: + term_graph(ast_manager &m); + ~term_graph(); + + const expr_ref_vector &get_lits() const { return m_lits; } + void get_terms(expr_ref_vector &res, bool exclude_cground = true); + bool is_cgr(expr *e); + unsigned size() { return m_terms.size(); } + + void set_vars(func_decl_ref_vector const &decls, bool exclude = true); + void set_vars(app_ref_vector const &vars, bool exclude = true); + void add_vars(app_ref_vector const &vars); + void add_var(app *var); + + ast_manager &get_ast_manager() const { return m; } + + void add_lit(expr *lit); + void add_lits(expr_ref_vector const &lits) { + for (expr *e : lits) add_lit(e); + } + void add_eq(expr *a, expr *b) { internalize_eq(a, b); } + void add_deq(expr *a, expr *b) { internalize_deq(a, b); } + + void reset(); + + // deprecate? + void to_lits(expr_ref_vector &lits, bool all_equalities = false, + bool repick_repr = true); + void to_lits_qe_lite(expr_ref_vector &lits, + std::function *non_core = nullptr); + expr_ref to_expr(bool repick_repr = true); + + /** + * Return literals obtained by projecting added literals + * onto the vocabulary of decls (if exclude is false) or outside the + * vocabulary of decls (if exclude is true). + */ + expr_ref_vector project(); + expr_ref_vector solve(); + expr_ref_vector project(model &mdl); + + /** + * Return disequalities to ensure that disequalities between + * excluded functions are preserved. + * For example if f(a) = b, f(c) = d, and b and d are not + * congruent, then produce the disequality a != c. + */ + expr_ref_vector get_ackerman_disequalities(); + + /** + * Produce model-based disequality + * certificate corresponding to + * definition in BGVS 2020. + * A disequality certificate is a reduced set of + * disequalities, true under mdl, such that the literals + * can be satisfied when non-shared symbols are projected. + */ + expr_ref_vector dcert(model &mdl, expr_ref_vector const &lits); + + /** + * Produce a model-based partition. + */ + vector get_partition(model &mdl); + + /** + * Extract shared occurrences of terms whose sort are + * fid, but appear in a context that is not fid. + * for example f(x + y) produces the shared occurrence + * x + y when f is uninterpreted and x + y has sort Int or Real. + */ + expr_ref_vector shared_occurrences(family_id fid); + + /** + * Map expression that occurs in added literals into representative if it + * exists. + */ + void add_model_based_terms(model &mdl, expr_ref_vector const &terms); + expr *rep_of(expr *e); + + using deqs = bit_vector; + struct add_deq_proc { + uint64_t m_deq_cnt = 0; + void operator()(term *t1, term *t2); + void operator()(ptr_vector &ts); + }; + + // -- disequalities added for output + vector> m_deq_pairs; + // -- maybe they are not necessary since they are in the original formula + vector> m_deq_distinct; + + expr_ref_vector non_ground_terms(); + void gr_terms_to_lits(expr_ref_vector &lits, bool all_equalities); + // produce a quantifier reduction of the formula stored in the term graph + // output of qel will not contain expression e s.t. non_core(e) == true + void qel(app_ref_vector &vars, expr_ref &fml, + std::function *non_core = nullptr); + bool has_val_in_class(expr *e); + app *get_const_in_class(expr *e); + void set_explicit_eq() { m_explicit_eq = true; } + + private: + add_deq_proc m_add_deq; + void refine_repr_class(term *t); + void refine_repr(); + bool makes_cycle(term *t); +}; + +namespace is_ground_ns { +struct found {}; +struct proc { + term_graph::is_variable_proc &m_is_var; + proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {} + void operator()(var *n) const {} + void operator()(app const *n) const { + if (m_is_var.contains(n->get_decl())) throw found(); + } + void operator()(quantifier *n) const {} +}; +} // namespace is_ground_ns +} // namespace mbp diff --git a/src/qe/mbp/mbp_tg_plugins.h b/src/qe/mbp/mbp_tg_plugins.h new file mode 100644 index 000000000..ab4a54333 --- /dev/null +++ b/src/qe/mbp/mbp_tg_plugins.h @@ -0,0 +1,34 @@ +/*++ + + Module Name: + + mbp_tg_plugins.h + +Abstract: + + Model Based Projection for a theory + +Author: + + Hari Govind V K (hgvk94) 2022-07-12 + +Revision History: + + +--*/ +#pragma once +#include "ast/ast.h" +#include "qe/mbp/mbp_qel_util.h" +#include "qe/mbp/mbp_term_graph.h" +#include "util/obj_hashtable.h" + +class mbp_tg_plugin { + public: + // iterate through all terms in m_tg and apply all theory MBP rules once + // returns true if any rules were applied + virtual bool apply() { return false; }; + virtual ~mbp_tg_plugin() = default; + virtual void use_model() { }; + virtual void get_new_vars(app_ref_vector*&) { }; + virtual family_id get_family_id() const { return null_family_id; }; +}; diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 9f5d9063c..d53684100 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -18,25 +18,127 @@ Revision History: --*/ -#include "ast/rewriter/expr_safe_replace.h" +#include "qe/qe_mbp.h" #include "ast/ast_pp.h" #include "ast/ast_util.h" -#include "ast/occurs.h" -#include "ast/rewriter/th_rewriter.h" #include "ast/expr_functors.h" #include "ast/for_each_expr.h" +#include "ast/occurs.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/rewriter.h" +#include "ast/rewriter/rewriter_def.h" #include "ast/scoped_proof.h" -#include "qe/qe_mbp.h" +#include "util/gparams.h" +#include "model/model_evaluator.h" +#include "model/model_pp.h" +#include "qe/lite/qe_lite_tactic.h" +#include "qe/lite/qel.h" #include "qe/mbp/mbp_arith.h" #include "qe/mbp/mbp_arrays.h" +#include "qe/mbp/mbp_qel.h" #include "qe/mbp/mbp_datatypes.h" -#include "qe/lite/qe_lite_tactic.h" -#include "model/model_pp.h" -#include "model/model_evaluator.h" - using namespace qe; +namespace { +// rewrite select(store(a, i, k), j) into k if m \models i = j and select(a, j) if m \models i != j + struct rd_over_wr_rewriter : public default_rewriter_cfg { + ast_manager &m; + array_util m_arr; + model_evaluator m_eval; + expr_ref_vector m_sc; + + rd_over_wr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_eval(mdl), m_sc(m) { + m_eval.set_model_completion(false); + } + + br_status reduce_app(func_decl *f, unsigned num, expr *const *args, + expr_ref &result, proof_ref &result_pr) { + if (m_arr.is_select(f) && m_arr.is_store(args[0])) { + expr_ref ind1(m), ind2(m); + ind1 = m_eval(args[1]); + ind2 = m_eval(to_app(args[0])->get_arg(1)); + if (ind1 == ind2) { + result = to_app(args[0])->get_arg(2); + m_sc.push_back(m.mk_eq(args[1], to_app(args[0])->get_arg(1))); + return BR_DONE; + } + m_sc.push_back(m.mk_not(m.mk_eq(args[1], to_app(args[0])->get_arg(1)))); + expr_ref_vector new_args(m); + new_args.push_back(to_app(args[0])->get_arg(0)); + new_args.push_back(args[1]); + result = m_arr.mk_select(new_args); + return BR_REWRITE1; + } + return BR_FAILED; + } + }; +// rewrite all occurrences of (as const arr c) to (as const arr v) where v = m_eval(c) + struct app_const_arr_rewriter : public default_rewriter_cfg { + ast_manager &m; + array_util m_arr; + datatype_util m_dt_util; + model_evaluator m_eval; + expr_ref val; + + app_const_arr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_dt_util(m), m_eval(mdl), val(m) { + m_eval.set_model_completion(false); + } + br_status reduce_app(func_decl *f, unsigned num, expr *const *args, + expr_ref &result, proof_ref &result_pr) { + if (m_arr.is_const(f) && !m.is_value(args[0])) { + val = m_eval(args[0]); + SASSERT(m.is_value(val)); + result = m_arr.mk_const_array(f->get_range(), val); + return BR_DONE; + } + if (m_dt_util.is_constructor(f)) { + // cons(head(x), tail(x)) --> x + ptr_vector const *accessors = + m_dt_util.get_constructor_accessors(f); + + SASSERT(num == accessors->size()); + // -- all accessors must have exactly one argument + if (any_of(*accessors, [&](const func_decl* acc) { return acc->get_arity() != 1; })) { + return BR_FAILED; + } + + if (num >= 1 && is_app(args[0]) && to_app(args[0])->get_decl() == accessors->get(0)) { + bool is_all = true; + expr* t = to_app(args[0])->get_arg(0); + for(unsigned i = 1; i < num && is_all; ++i) { + is_all &= (is_app(args[i]) && + to_app(args[i])->get_decl() == accessors->get(i) && + to_app(args[i])->get_arg(0) == t); + } + if (is_all) { + result = t; + return BR_DONE; + } + } + } + return BR_FAILED; + } + }; +} +void rewrite_as_const_arr(expr* in, model& mdl, expr_ref& out) { + app_const_arr_rewriter cfg(out.m(), mdl); + rewriter_tpl rw(out.m(), false, cfg); + rw(in, out); +} + +void rewrite_read_over_write(expr *in, model &mdl, expr_ref &out) { + rd_over_wr_rewriter cfg(out.m(), mdl); + rewriter_tpl rw(out.m(), false, cfg); + rw(in, out); + if (cfg.m_sc.empty()) return; + expr_ref_vector sc(out.m()); + SASSERT(out.m().is_and(out)); + flatten_and(out, sc); + sc.append(cfg.m_sc); + out = mk_and(sc); +} class mbproj::impl { ast_manager& m; @@ -47,6 +149,7 @@ class mbproj::impl { // parameters bool m_reduce_all_selects; bool m_dont_sub; + bool m_use_qel; void add_plugin(mbp::project_plugin* p) { family_id fid = p->get_family_id(); @@ -253,9 +356,35 @@ public: m_params.append(p); m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false); m_dont_sub = m_params.get_bool("dont_sub", false); + auto q = gparams::get_module("smt"); + m_params.append(q); + m_use_qel = m_params.get_bool("qsat_use_qel", true); } void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + if (m_use_qel) { + extract_literals(model, vars, fmls); + expr_ref e(m); + bool change = true; + while (change && !vars.empty()) { + change = false; + e = mk_and(fmls); + do_qel(vars, e); + fmls.reset(); + flatten_and(e, fmls); + for (auto* p : m_plugins) { + if (p && p->solve(model, vars, fmls)) { + change = true; + } + } + } + //rewrite as_const_arr terms + expr_ref fml(m); + fml = mk_and(fmls); + rewrite_as_const_arr(fml, model, fml); + flatten_and(fml, fmls); + } + else { extract_literals(model, vars, fmls); bool change = true; while (change && !vars.empty()) { @@ -267,6 +396,7 @@ public: } } } + } bool validate_model(model& model, expr_ref_vector const& fmls) { for (expr* f : fmls) { @@ -276,6 +406,22 @@ public: } void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { + if (m_use_qel) { + bool dsub = m_dont_sub; + m_dont_sub = !force_elim; + expr_ref fml(m); + fml = mk_and(fmls); + spacer_qel(vars, model, fml); + fmls.reset(); + flatten_and(fml, fmls); + m_dont_sub = dsub; + } + else { + mbp(force_elim, vars, model, fmls); + } + } + + void mbp(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { SASSERT(validate_model(model, fmls)); expr_ref val(m), tmp(m); app_ref var(m); @@ -341,6 +487,17 @@ public: SASSERT(!m.is_false(fml)); } + + void do_qel(app_ref_vector &vars, expr_ref &fml) { + qel qe(m, m_params); + qe(vars, fml); + m_rw(fml); + TRACE("qe", tout << "After qel:\n" + << fml << "\n" + << "Vars: " << vars << "\n";); + SASSERT(!m.is_false(fml)); + } + void do_qe_bool(model& mdl, app_ref_vector& vars, expr_ref& fml) { expr_ref_vector fmls(m); fmls.push_back(fml); @@ -348,7 +505,86 @@ public: fml = mk_and(fmls); } + void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) { + flatten_and(fml); + mbp::mbp_qel mbptg(m, m_params); + mbptg(vars, fml, mdl); + if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml); + m_rw(fml); + TRACE("qe", tout << "After mbp_tg:\n" + << fml << " models " << mdl.is_true(fml) << "\n" + << "Vars: " << vars << "\n";); + } + + void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) { + TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";); + + model_evaluator eval(mdl, m_params); + eval.set_model_completion(true); + app_ref_vector other_vars(m); + app_ref_vector sub_vars(m); + array_util arr_u(m); + arith_util ari_u(m); + datatype_util dt_u(m); + + do_qel(vars, fml); + qel_project(vars, mdl, fml, m_reduce_all_selects); + flatten_and(fml); + m_rw(fml); + rewrite_as_const_arr(fml, mdl, fml); + + for (app* v : vars) { + SASSERT(!arr_u.is_array(v) && !dt_u.is_datatype(v->get_sort())); + other_vars.push_back(v); + } + + // project reals, ints and other variables. + if (!other_vars.empty()) { + TRACE("qe", tout << "Other vars: " << other_vars << "\n" << mdl;); + + expr_ref_vector fmls(m); + flatten_and(fml, fmls); + + mbp(false, other_vars, mdl, fmls); + fml = mk_and(fmls); + m_rw(fml); + + TRACE("qe", + tout << "Projected other vars:\n" << fml << "\n"; + tout << "Remaining other vars:\n" << other_vars << "\n";); + SASSERT(!m.is_false(fml)); + } + + if (!other_vars.empty()) { + project_vars(mdl, other_vars, fml); + m_rw(fml); + } + + // substitute any remaining other vars + if (!m_dont_sub && !other_vars.empty()) { + subst_vars(eval, other_vars, fml); + TRACE("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";); + // an extra round of simplification because subst_vars is not simplifying + m_rw(fml); + other_vars.reset(); + } + + SASSERT(!eval.is_false(fml)); + + vars.reset(); + vars.append(other_vars); + } + void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) { + if (m_use_qel) { + spacer_qel(vars, mdl, fml); + } + else { + spacer_qe_lite(vars, mdl, fml); + } + } + + void spacer_qe_lite(app_ref_vector& vars, model& mdl, expr_ref& fml) { TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";); model_evaluator eval(mdl, m_params); @@ -428,7 +664,6 @@ public: vars.reset(); vars.append(other_vars); } - }; mbproj::mbproj(ast_manager& m, params_ref const& p) { @@ -447,6 +682,7 @@ void mbproj::updt_params(params_ref const& p) { void mbproj::get_param_descrs(param_descrs& r) { r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects"); r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables"); + r.insert("use_qel", CPK_BOOL, "(default: true) use egraph based QEL"); } void mbproj::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) { @@ -468,3 +704,5 @@ opt::inf_eps mbproj::maximize(expr_ref_vector const& fmls, model& mdl, app* t, e scoped_no_proof _sp(fmls.get_manager()); return m_impl->maximize(fmls, mdl, t, ge, gt); } +template class rewriter_tpl; +template class rewriter_tpl; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 7e28437f6..fe4c4945c 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -39,6 +39,7 @@ Notes: #include "qe/qe_mbp.h" #include "qe/qe.h" #include "ast/rewriter/label_rewriter.h" +#include "util/params.h" namespace qe { @@ -164,8 +165,9 @@ namespace qe { TRACE("qe_assumptions", model_v2_pp(tout, *mdl);); expr_ref val(m); - for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { - app* p = m_preds[level - 1][j].get(); + for (unsigned i = 0; i <= level-1; ++i) { + for (unsigned j = 0; j < m_preds[i].size(); ++j) { + app* p = m_preds[i][j].get(); eval(p, val); if (!m.inc()) return; @@ -176,6 +178,7 @@ namespace qe { SASSERT(m.is_true(val)); m_asms.push_back(p); } + } } asms.append(m_asms); @@ -529,11 +532,14 @@ namespace qe { ast_manager& m; params_ref m_params; ref m_solver; + + expr_ref m_last_assert; public: kernel(ast_manager& m): m(m), - m_solver(nullptr) + m_solver(nullptr), + m_last_assert(m) { m_params.set_bool("model", true); m_params.set_uint("relevancy", 0); @@ -544,7 +550,7 @@ namespace qe { solver const& s() const { return *m_solver; } void init() { - m_solver = mk_smt_solver(m, m_params, symbol::null); + m_solver = mk_smt2_solver(m, m_params, symbol::null); } void collect_statistics(statistics & st) const { if (m_solver) @@ -561,7 +567,23 @@ namespace qe { void clear() { m_solver = nullptr; } - void assert_expr(expr* e) { + + void assert_expr(expr *e) { + if (!m.is_true(e)) + m_solver->assert_expr(e); + } + void assert_blocking_fml(expr* e) { + if (m.is_true(e)) return; + if (m_last_assert) { + if (e == m_last_assert) { + verbose_stream() << "Asserting this expression twice in a row:\n " << m_last_assert << "\n"; + SASSERT(false); + std::exit(3); + } + + } + m_last_assert = e; + m_solver->assert_expr(e); } @@ -618,7 +640,9 @@ namespace qe { lbool check_sat() { while (true) { ++m_stats.m_num_rounds; - IF_VERBOSE(3, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";); + TRACE("qe", + tout << "level: " << m_level << " round: " << m_stats.m_num_rounds << "\n"); check_cancel(); expr_ref_vector asms(m_asms); m_pred_abs.get_assumptions(m_model.get(), asms); @@ -951,7 +975,8 @@ namespace qe { } else { fml = m_pred_abs.mk_abstract(fml); - get_kernel(m_level).assert_expr(fml); + TRACE("qe_block", tout << "Blocking fml at level: " << m_level << "\n" << fml << "\n";); + get_kernel(m_level).assert_blocking_fml(fml); } SASSERT(!m_model.get()); return true; @@ -1235,8 +1260,11 @@ namespace qe { m_value(nullptr), m_was_sat(false), m_gt(m) - { - } + { + params_ref q = params_ref(); + q.set_bool("use_qel", false); + m_mbp.updt_params(q); + } ~qsat() override { clear(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 7bc9bc3fa..2bb3d4197 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -132,6 +132,7 @@ def_module_params(module_name='smt', ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'), - ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy') + ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), + ('qsat_use_qel', BOOL, True, 'Use QEL for lite quantifier elimination and model-based projection in QSAT') ))