From 51d3c279d0656a729c1fe27249f7fd5f3f59e71c Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 2 Aug 2023 12:34:06 -0400 Subject: [PATCH] QEL: Fast Approximated Quantifier Elimination (#6820) * qe_lite: cleanup and comment no change to code * mbp_arrays: refactor out partial equality (peq) Partial array equality, PEQ, is used as an intermediate expression during MBP for arrays. We need to factor it out so that it can be shared between MBP-QEL and existing MBP. Partial array equality (peq) is used in MBP for arrays. Factoring this out to be used by multiple MBP implementations. * rewriter: new rewrite rules These rules are specializes for terms that are created in QEL. QEL commit is comming later * datatype_rw: new rewrite rule for ADTs The rule handles this special case: (cons (head x) (tail x)) --> x * array_rewriter rules for rewriting PEQs Special rules to simplify PEQs * th_rewriter: wire PEQ simplifications * spacer_iuc: avoid terms with default in IUC Spacer prfers to not have a term representing default value of an array. This guides IUC from picking such terms in interpolation * mbp_term_graph: replace root with repr * mbp_term_graph: formatting * mbp_term_graph: class_props, getters, setters Class properties allow to keep information for an equivalence class. Getters and setters for terms allow accessing information * mbp_term_graph: auxiliary methods for qel QEL commit is comming later in the history * mbp_term_graph: bug fix * mbp_term_graph: pick, refine repr, compute cgrnd * mbp_term_graph: internalize deq * mbp_term_graph: constructor * mbp_term_graph: optionally internalize equalities Reperesent equalities explicitly by nodes in the term_graph * qel * formatting * comments on term_lt * get terms and other api for mbp_qel * plugins for mbp_qel * mbp_qel_util: utilities for mbp_qel * qe_mbp: QEL-based mbp * qel: expose QEL API * spacer: replace qe_lite in qe_project_spacer by qel This changes the default projection engine that spacer uses. * cmd_context: debug commands for qel and mbp_qel New commands are mbp-qel -- MBP with term graphs qel -- QEL with term graphs qe-lite -- older qelite * qe_mbp: model-based rewriters for arrays * qe_mbp: QEL-based projection functions * qsat: wire in QEL-based mbp * qsat: debug code * qsat: maybe a bug fix Changed the code to follow the paper by adding all predicates above a given level, not just predicates of immediately preceding level. * chore: use new api to create solver in qsat * mbp_term_graph use all_of idiom * feat: solver for integer multiplication * array_peq: formatting, no change to code * mbp_qel_util: block comment + format * mbt_term_graph: clang-format * bug fix. Move dt rewrite to qe_mbp * array_peq: add header * run clang format on mbp plugins * clang format on mul solver * format do-while * format * format do-while * update release notes --------- Co-authored-by: hgvk94 Co-authored-by: Isabel Garcia --- RELEASE_NOTES.md | 1 + src/ast/CMakeLists.txt | 1 + src/ast/array_peq.cpp | 107 + src/ast/array_peq.h | 91 + src/ast/rewriter/array_rewriter.cpp | 43 +- src/ast/rewriter/datatype_rewriter.cpp | 3 +- src/ast/rewriter/th_rewriter.cpp | 5 + src/cmd_context/extra_cmds/dbg_cmds.cpp | 196 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 20 +- src/muz/spacer/spacer_util.h | 1 + src/qe/lite/CMakeLists.txt | 2 + src/qe/lite/qe_lite_tactic.cpp | 6 +- src/qe/lite/qe_lite_tactic.h | 1 + src/qe/lite/qel.cpp | 54 + src/qe/lite/qel.h | 49 + src/qe/mbp/CMakeLists.txt | 5 + src/qe/mbp/mbp_arrays.cpp | 142 +- src/qe/mbp/mbp_arrays_tg.cpp | 394 +++ src/qe/mbp/mbp_arrays_tg.h | 47 + src/qe/mbp/mbp_basic_tg.cpp | 101 + src/qe/mbp/mbp_basic_tg.h | 40 + src/qe/mbp/mbp_dt_tg.cpp | 202 ++ src/qe/mbp/mbp_dt_tg.h | 44 + src/qe/mbp/mbp_qel.cpp | 226 ++ src/qe/mbp/mbp_qel.h | 41 + src/qe/mbp/mbp_qel_util.cpp | 110 + src/qe/mbp/mbp_qel_util.h | 41 + src/qe/mbp/mbp_solve_plugin.cpp | 92 +- src/qe/mbp/mbp_term_graph.cpp | 2926 +++++++++++-------- src/qe/mbp/mbp_term_graph.h | 355 ++- src/qe/mbp/mbp_tg_plugins.h | 34 + src/qe/qe_mbp.cpp | 256 +- src/qe/qsat.cpp | 46 +- src/smt/params/smt_params_helper.pyg | 3 +- 35 files changed, 4170 insertions(+), 1517 deletions(-) create mode 100644 src/ast/array_peq.cpp create mode 100644 src/ast/array_peq.h create mode 100644 src/qe/lite/qel.cpp create mode 100644 src/qe/lite/qel.h create mode 100644 src/qe/mbp/mbp_arrays_tg.cpp create mode 100644 src/qe/mbp/mbp_arrays_tg.h create mode 100644 src/qe/mbp/mbp_basic_tg.cpp create mode 100644 src/qe/mbp/mbp_basic_tg.h create mode 100644 src/qe/mbp/mbp_dt_tg.cpp create mode 100644 src/qe/mbp/mbp_dt_tg.h create mode 100644 src/qe/mbp/mbp_qel.cpp create mode 100644 src/qe/mbp/mbp_qel.h create mode 100644 src/qe/mbp/mbp_qel_util.cpp create mode 100644 src/qe/mbp/mbp_qel_util.h create mode 100644 src/qe/mbp/mbp_tg_plugins.h 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') ))