From efbe0a655414ba8e64c5a0b3c62e02730f622691 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Nov 2022 17:56:45 -0800 Subject: [PATCH] wip - updated version of elim_uncstr_tactic - remove reduce_invertible. It is subsumed by reduce_uncstr(2) - introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter. reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence. The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner. --- src/ast/arith_decl_plugin.h | 2 + src/ast/array_decl_plugin.h | 4 + src/ast/bv_decl_plugin.h | 8 + src/ast/converters/CMakeLists.txt | 1 + src/ast/converters/expr_inverter.cpp | 791 ++++++++++++++++++ src/ast/converters/expr_inverter.h | 57 ++ src/ast/converters/generic_model_converter.h | 4 + src/ast/for_each_expr.cpp | 13 +- src/ast/for_each_expr.h | 12 +- src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/elim_unconstrained.cpp | 297 +++++++ src/ast/simplifiers/elim_unconstrained.h | 84 ++ .../model_reconstruction_trail.cpp | 8 + .../simplifiers/model_reconstruction_trail.h | 13 +- src/tactic/core/CMakeLists.txt | 3 +- src/tactic/core/elim_uncnstr2_tactic.h | 41 + src/tactic/core/elim_uncnstr_tactic.cpp | 7 +- src/tactic/core/reduce_invertible_tactic.cpp | 576 ------------- src/tactic/core/reduce_invertible_tactic.h | 32 - src/tactic/dependent_expr_state_tactic.h | 1 + 20 files changed, 1334 insertions(+), 621 deletions(-) create mode 100644 src/ast/converters/expr_inverter.cpp create mode 100644 src/ast/converters/expr_inverter.h create mode 100644 src/ast/simplifiers/elim_unconstrained.cpp create mode 100644 src/ast/simplifiers/elim_unconstrained.h create mode 100644 src/tactic/core/elim_uncnstr2_tactic.h delete mode 100644 src/tactic/core/reduce_invertible_tactic.cpp delete mode 100644 src/tactic/core/reduce_invertible_tactic.h diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 0c77867d4f0..93d0edf2ff6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -447,6 +447,8 @@ class arith_util : public arith_recognizers { app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); } app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.data()); } app * mk_add(expr_ref_buffer const& args) const { return mk_add(args.size(), args.data()); } + app * mk_add(ptr_buffer const& args) const { return mk_add(args.size(), args.data()); } + app * mk_add(ptr_vector const& args) const { return mk_add(args.size(), args.data()); } app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); } app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 83d54109726..79c6e682e65 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -207,6 +207,10 @@ class array_util : public array_recognizers { return mk_store(args.size(), args.data()); } + app* mk_store(ptr_buffer const& args) const { + return mk_store(args.size(), args.data()); + } + app * mk_select(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args); } diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 37531d9363f..ee618b42cbb 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -448,9 +448,17 @@ class bv_util : public bv_recognizers { app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); } app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); } app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } + app * mk_bv_add(ptr_buffer const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); } + app * mk_bv_add(ptr_vector const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); } + app * mk_bv_add(expr_ref_vector const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); } + app * mk_bv_add(expr_ref_buffer const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); } app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); } + app* mk_bv_mul(ptr_buffer const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); } + app* mk_bv_mul(ptr_vector const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); } + app* mk_bv_mul(expr_ref_vector const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); } + app* mk_bv_mul(expr_ref_buffer const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); } app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); } app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); } app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); } diff --git a/src/ast/converters/CMakeLists.txt b/src/ast/converters/CMakeLists.txt index 52895f06486..64f5060e791 100644 --- a/src/ast/converters/CMakeLists.txt +++ b/src/ast/converters/CMakeLists.txt @@ -1,5 +1,6 @@ z3_add_component(converters SOURCES + expr_inverter.cpp equiv_proof_converter.cpp generic_model_converter.cpp horn_subsume_model_converter.cpp diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp new file mode 100644 index 00000000000..504c04ab0c4 --- /dev/null +++ b/src/ast/converters/expr_inverter.cpp @@ -0,0 +1,791 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + expr_inverter.cpp + +Abstract: + + inverter interface and instance + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-11 + +--*/ + +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/ast_util.h" +#include "ast/arith_decl_plugin.h" +#include "ast/converters/expr_inverter.h" + +class basic_expr_inverter : public iexpr_inverter { +public: + + basic_expr_inverter(ast_manager& m) : iexpr_inverter(m) {} + + /** + * if (c, x, x') -> fresh + * x := fresh + * x' := fresh + * + * if (x, x', e) -> fresh + * x := true + * x' := fresh + * + * if (x, t, x') -> fresh + * x := false + * x' := fresh + * + * not x -> fresh + * x := not fresh + * + * x & x' -> fresh + * x := fresh + * x' := true + * + * x or x' -> fresh + * x := fresh + * x' := false + * + * x = t -> fresh + * x := if(fresh, t, diff(t)) + * where diff is a diagnonalization function available in domains of size > 1. + * + */ + + bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) { + SASSERT(f->get_family_id() == m.get_basic_family_id()); + switch (f->get_decl_kind()) { + case OP_ITE: + SASSERT(num == 3); + if (uncnstr(args[1]) && uncnstr(args[2])) { + mk_fresh_uncnstr_var_for(f, r); + add_def(args[1], r); + add_def(args[2], r); + return true; + } + if (uncnstr(args[0]) && uncnstr(args[1])) { + mk_fresh_uncnstr_var_for(f, r); + add_def(args[0], m.mk_true()); + add_def(args[1], r); + return true; + } + if (uncnstr(args[0]) && uncnstr(args[2])) { + mk_fresh_uncnstr_var_for(f, r); + add_def(args[0], m.mk_false()); + add_def(args[2], r); + return true; + } + return false; + case OP_NOT: + SASSERT(num == 1); + if (uncnstr(args[0])) { + mk_fresh_uncnstr_var_for(f, r); + add_def(args[0], m.mk_not(r)); + return true; + } + return false; + case OP_AND: + if (num > 0 && uncnstr(num, args)) { + mk_fresh_uncnstr_var_for(f, r); + add_defs(num, args, r, m.mk_true()); + return true; + } + return false; + case OP_OR: + if (num > 0 && uncnstr(num, args)) { + mk_fresh_uncnstr_var_for(f, r); + add_defs(num, args, r, m.mk_false()); + return true; + } + return false; + case OP_EQ: + SASSERT(num == 2); + // return process_eq(f, args[0], args[1]); + default: + return false; + } + return false; + } + + bool mk_diff(expr* t, expr_ref& r) override { + SASSERT(m.is_bool(t)); + r = mk_not(m, t); + return true; + } +}; + +class arith_expr_inverter : public iexpr_inverter { + arith_util a; +public: + + arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {} + + family_id get_fid() const { return a.get_family_id(); } + + bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) { + expr* v; + expr* t; + if (uncnstr(arg1)) { + v = arg1; + t = arg2; + } + else if (uncnstr(arg2)) { + v = arg2; + t = arg1; + le = !le; + } + else + return false; + + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + // v = ite(u, t, t + 1) if le + // v = ite(u, t, t - 1) if !le + add_def(v, m.mk_ite(r, t, a.mk_add(t, a.mk_numeral(rational(le ? 1 : -1), arg1->get_sort())))); + } + return true; + } + + bool process_add(unsigned num, expr* const* args, expr_ref& u) { + if (num == 0) + return false; + unsigned i; + expr* v = nullptr; + for (i = 0; i < num; i++) { + expr* arg = args[i]; + if (uncnstr(arg)) { + v = arg; + break; + } + } + if (v == nullptr) + return false; + mk_fresh_uncnstr_var_for(v->get_sort(), u); + if (!m_mc) + return true; + ptr_buffer new_args; + for (unsigned j = 0; j < num; j++) + if (j != i) + new_args.push_back(args[j]); + + if (new_args.empty()) + add_def(v, u); + else { + expr* rest = a.mk_add(new_args); + add_def(v, a.mk_sub(u, rest)); + } + return true; + } + + bool process_arith_mul(unsigned num, expr* const* args, expr_ref & u) { + if (num == 0) + return false; + sort* s = args[0]->get_sort(); + if (uncnstr(num, args)) { + mk_fresh_uncnstr_var_for(s, u); + if (m_mc) + add_defs(num, args, u, a.mk_numeral(rational(1), s)); + return true; + } + // c * v case for reals + bool is_int; + rational val; + if (num == 2 && uncnstr(args[1]) && a.is_numeral(args[0], val, is_int) && !is_int) { + if (val.is_zero()) + return false; + mk_fresh_uncnstr_var_for(s, u); + if (m_mc) { + val = rational(1) / val; + add_def(args[1], a.mk_mul(a.mk_numeral(val, false), u)); + } + return true; + } + return false; + } + + + bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override { + SASSERT(f->get_family_id() == a.get_family_id()); + switch (f->get_decl_kind()) { + case OP_ADD: + return process_add(num, args, r); + case OP_MUL: + return process_arith_mul(num, args, r); + case OP_LE: + SASSERT(num == 2); + return process_le_ge(f, args[0], args[1], true, r); + case OP_GE: + SASSERT(num == 2); + return process_le_ge(f, args[0], args[1], false, r); + default: + return false; + } + } + + + bool mk_diff(expr* t, expr_ref& r) override { + SASSERT(a.is_int_real(t)); + r = a.mk_add(t, a.mk_numeral(rational(1), a.is_int(t))); + return true; + } +}; + +class bv_expr_inverter : public iexpr_inverter { + bv_util bv; + + bool process_add(unsigned num, expr* const* args, expr_ref& u) { + if (num == 0) + return false; + unsigned i; + expr* v = nullptr; + for (i = 0; i < num; i++) { + expr* arg = args[i]; + if (uncnstr(arg)) { + v = arg; + break; + } + } + if (!v) + return false; + mk_fresh_uncnstr_var_for(v->get_sort(), u); + if (!m_mc) + return true; + ptr_buffer new_args; + for (unsigned j = 0; j < num; j++) + if (j != i) + new_args.push_back(args[j]); + + if (new_args.empty()) + add_def(v, u); + else { + expr* rest = bv.mk_bv_add(new_args); + add_def(v, bv.mk_bv_sub(u, rest)); + } + return true; + } + + bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) { + if (num == 0) + return nullptr; + if (uncnstr(num, args)) { + sort* s = args[0]->get_sort(); + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) + add_defs(num, args, r, bv.mk_numeral(rational(1), s)); + return true; + } + // c * v (c is odd) case + unsigned sz; + rational val; + rational inv; + if (num == 2 && + uncnstr(args[1]) && + bv.is_numeral(args[0], val, sz) && + val.mult_inverse(sz, inv)) { + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) + add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv, sz), r)); + return true; + } + + // + // x * K -> fresh[hi-sh-1:0] ++ 0...0 + // where sh = parity of K + // then x -> J^-1*fresh + // where J = K >> sh + // Because x * K = fresh * K * J^-1 = fresh * 2^sh = fresh[hi-sh-1:0] ++ 0...0 + // + if (num == 2 && + uncnstr(args[1]) && + bv.is_numeral(args[0], val, sz) && + val.is_pos()) { + unsigned sh = 0; + while (val.is_even()) { + val /= rational(2); + ++sh; + } + mk_fresh_uncnstr_var_for(f, r); + if (sh > 0) + r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_numeral(0, sh)); + + if (m_mc) { + rational inv_r; + VERIFY(val.mult_inverse(sz, inv_r)); + add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), r)); + } + return true; + } + + // + // assume x is unconstrained, we can handle general multiplication as follows: + // x * y -> if y = 0 then y else fresh << parity(y) + // and x -> if y = 0 then y else (y >> parity(y))^-1 + // parity can be defined using a "giant" ite expression. + // + + return false; + } + + + bool process_extract(func_decl* f, expr* arg, expr_ref& r) { + if (!uncnstr(arg)) + return false; + mk_fresh_uncnstr_var_for(f, r); + if (!m_mc) + return true; + unsigned high = bv.get_extract_high(f); + unsigned low = bv.get_extract_low(f); + unsigned bv_size = bv.get_bv_size(arg->get_sort()); + if (bv_size == high - low + 1) + add_def(arg, r); + else { + ptr_buffer args; + if (high < bv_size - 1) + args.push_back(bv.mk_numeral(rational(0), bv_size - high - 1)); + args.push_back(r); + if (low > 0) + args.push_back(bv.mk_numeral(rational(0), low)); + add_def(arg, bv.mk_concat(args.size(), args.data())); + } + return true; + } + + bool process_bv_div(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) { + if (uncnstr(arg1) && uncnstr(arg2)) { + sort* s = arg1->get_sort(); + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + add_def(arg1, r); + add_def(arg2, bv.mk_numeral(rational(1), s)); + } + return true; + } + return false; + } + + bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) { + if (num == 0) + return false; + if (!uncnstr(num, args)) + return false; + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + unsigned i = num; + unsigned low = 0; + while (i > 0) { + --i; + expr* arg = args[i]; + unsigned sz = bv.get_bv_size(arg); + add_def(arg, bv.mk_extract(low + sz - 1, low, r)); + low += sz; + } + } + return true; + } + + bool process_bv_le(func_decl* f, expr* arg1, expr* arg2, bool is_signed, expr_ref& r) { + if (uncnstr(arg1)) { + // v <= t + expr* v = arg1; + expr* t = arg2; + // v <= t ---> (u or t == MAX) u is fresh + // add definition v = ite(u or t == MAX, t, t+1) + unsigned bv_sz = bv.get_bv_size(arg1); + rational MAX; + if (is_signed) + MAX = rational::power_of_two(bv_sz - 1) - rational(1); + else + MAX = rational::power_of_two(bv_sz) - rational(1); + mk_fresh_uncnstr_var_for(f, r); + r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MAX, bv_sz))); + if (m_mc) + add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_numeral(rational(1), bv_sz)))); + return true; + } + if (uncnstr(arg2)) { + // v >= t + expr* v = arg2; + expr* t = arg1; + // v >= t ---> (u ot t == MIN) u is fresh + // add definition v = ite(u or t == MIN, t, t-1) + unsigned bv_sz = bv.get_bv_size(arg1); + rational MIN; + if (is_signed) + MIN = -rational::power_of_two(bv_sz - 1); + else + MIN = rational(0); + mk_fresh_uncnstr_var_for(f, r); + r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MIN, bv_sz))); + if (m_mc) + add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_numeral(rational(1), bv_sz)))); + return true; + } + return false; + } + + bool process_bvnot(expr* e, expr_ref& r) { + if (!uncnstr(e)) + return false; + mk_fresh_uncnstr_var_for(e->get_sort(), r); + if (m_mc) + add_def(e, bv.mk_bv_not(r)); + return true; + } + + public: + bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {} + + family_id get_fid() const { return bv.get_family_id(); } + + /** + * x + t -> fresh + * x := fresh - t + * + * x * x' * x'' -> fresh + * x := fresh + * x', x'' := 1 + * + * c * x -> fresh, c is odd + * x := fresh*c^-1 + * + * x[sz-1:0] -> fresh + * x := fresh + * + * x[hi:lo] -> fresh + * x := fresh1 ++ fresh ++ fresh2 + * + * x udiv x', x sdiv x' -> fresh + * x' := 1 + * x := fresh + * + * x ++ x' ++ x'' -> fresh + * x := fresh[hi1:lo1] + * x' := fresh[hi2:lo2] + * x'' := fresh[hi3:lo3] + * + * x <= t -> fresh or t == MAX + * x := if(fresh, t, t + 1) + * t <= x -> fresh or t == MIN + * x := if(fresh, t, t - 1) + * + * ~x -> fresh + * x := ~fresh + * + * x | y -> fresh + * x := fresh + * y := 0 + * + */ + bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override { + SASSERT(f->get_family_id() == bv.get_family_id()); + switch (f->get_decl_kind()) { + case OP_BADD: + return process_add(num, args, r); + case OP_BMUL: + return process_bv_mul(f, num, args, r); + case OP_BSDIV: + case OP_BUDIV: + case OP_BSDIV_I: + case OP_BUDIV_I: + SASSERT(num == 2); + return process_bv_div(f, args[0], args[1], r); + case OP_SLEQ: + SASSERT(num == 2); + return process_bv_le(f, args[0], args[1], true, r); + case OP_ULEQ: + SASSERT(num == 2); + return process_bv_le(f, args[0], args[1], false, r); + case OP_CONCAT: + return process_concat(f, num, args, r); + case OP_EXTRACT: + SASSERT(num == 1); + return process_extract(f, args[0], r); + case OP_BNOT: + SASSERT(num == 1); + return process_bvnot(args[0], r); + case OP_BOR: + if (num > 0 && uncnstr(num, args)) { + sort* s = args[0]->get_sort(); + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) + add_defs(num, args, r, bv.mk_numeral(rational(0), s)); + return true; + } + return false; + default: + return false; + } + } + + bool mk_diff(expr* t, expr_ref& r) override { + r = bv.mk_bv_not(t); + return true; + } +}; + + + +/** + * F[select(x, i)] -> F[fresh] + * x := const(fresh) + + * F[store(x, ..., x')] -> F[fresh] + * x' := select(x, ...) + * x := fresh + */ + +class array_expr_inverter : public iexpr_inverter { + array_util a; + iexpr_inverter& inv; +public: + array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {} + + family_id get_fid() const { return a.get_family_id(); } + + bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override { + SASSERT(f->get_family_id() == a.get_family_id()); + switch (f->get_decl_kind()) { + case OP_SELECT: + if (uncnstr(args[0])) { + mk_fresh_uncnstr_var_for(f, r); + sort* s = args[0]->get_sort(); + if (m_mc) + add_def(args[0], a.mk_const_array(s, r)); + return true; + } + return false; + case OP_STORE: + if (uncnstr(args[0]) && uncnstr(args[num - 1])) { + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + add_def(args[num - 1], m.mk_app(a.get_family_id(), OP_SELECT, num - 1, args)); + add_def(args[0], r); + } + return true; + } + default: + return false; + } + } + + bool mk_diff(expr* t, expr_ref& r) override { + sort* s = t->get_sort(); + SASSERT(a.is_array(s)); + if (m.is_uninterp(get_array_range(s))) + return false; + unsigned arity = get_array_arity(s); + for (unsigned i = 0; i < arity; i++) + if (m.is_uninterp(get_array_domain(s, i))) + return false; + // building + // r = (store t i1 ... in d) + // where i1 ... in are arbitrary values + // and d is a term different from (select t i1 ... in) + expr_ref_vector new_args(m); + new_args.push_back(t); + for (unsigned i = 0; i < arity; i++) + new_args.push_back(m.get_some_value(get_array_domain(s, i))); + expr_ref sel(m); + sel = a.mk_select(new_args); + expr_ref diff_sel(m); + if (!inv.mk_diff(sel, diff_sel)) + return false; + new_args.push_back(diff_sel); + r = a.mk_store(new_args); + return true; + } +}; + + + +class dt_expr_inverter : public iexpr_inverter { + datatype_util dt; +public: + + dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {} + + family_id get_fid() const { return dt.get_family_id(); } + /** + * head(x) -> fresh + * x := cons(fresh, arb) + */ + bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override { + if (dt.is_accessor(f)) { + SASSERT(num == 1); + if (uncnstr(args[0])) { + if (!m_mc) { + mk_fresh_uncnstr_var_for(f, r); + return true; + } + func_decl* c = dt.get_accessor_constructor(f); + for (unsigned i = 0; i < c->get_arity(); i++) + if (!m.is_fully_interp(c->get_domain(i))) + return false; + mk_fresh_uncnstr_var_for(f, r); + ptr_vector const& accs = *dt.get_constructor_accessors(c); + ptr_buffer new_args; + for (unsigned i = 0; i < accs.size(); i++) { + if (accs[i] == f) + new_args.push_back(r); + else + new_args.push_back(m.get_some_value(c->get_domain(i))); + } + add_def(args[0], m.mk_app(c, new_args)); + return true; + } + } + return false; + } + + bool mk_diff(expr* t, expr_ref& r) override { + // In the current implementation, I only handle the case where + // the datatype has a recursive constructor. + sort* s = t->get_sort(); + ptr_vector const& constructors = *dt.get_datatype_constructors(s); + for (func_decl* constructor : constructors) { + unsigned num = constructor->get_arity(); + unsigned target = UINT_MAX; + for (unsigned i = 0; i < num; i++) { + sort* s_arg = constructor->get_domain(i); + if (s == s_arg) { + target = i; + continue; + } + if (m.is_uninterp(s_arg)) + break; + } + if (target == UINT_MAX) + continue; + // use the constructor the distinct term constructor(...,t,...) + ptr_buffer new_args; + for (unsigned i = 0; i < num; i++) { + if (i == target) + new_args.push_back(t); + else + new_args.push_back(m.get_some_value(constructor->get_domain(i))); + } + r = m.mk_app(constructor, new_args); + return true; + } + return false; + } +}; + + + +expr_inverter::~expr_inverter() { + for (auto* v : m_inverters) + dealloc(v); +} + + +bool iexpr_inverter::uncnstr(unsigned num, expr * const * args) const { + for (unsigned i = 0; i < num; i++) + if (!m_is_var(args[i])) + return false; + return true; +} + +/** + \brief Create a fresh variable for abstracting (f args[0] ... args[num-1]) + Return true if it a new variable was created, and false if the variable already existed for this + application. Store the variable in v +*/ +void iexpr_inverter::mk_fresh_uncnstr_var_for(sort * s, expr_ref & v) { + v = m.mk_fresh_const(nullptr, s); + if (m_mc) + m_mc->hide(v); +} + +void iexpr_inverter::add_def(expr * v, expr * def) { + expr_ref _v(v, m); + expr_ref _d(def, m); + if (!m_mc) + return; + SASSERT(uncnstr(v)); + SASSERT(to_app(v)->get_num_args() == 0); + m_mc->add(to_app(v)->get_decl(), def); +} + +void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* identity) { + expr_ref _id(identity, m); + if (!m_mc) + return; + add_def(args[0], u); + for (unsigned i = 1; i < num; i++) + add_def(args[i], identity); +} + + +expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) { + auto* a = alloc(arith_expr_inverter, m); + auto* b = alloc(bv_expr_inverter, m); + auto* ar = alloc(array_expr_inverter, m, *this); + auto* dt = alloc(dt_expr_inverter, m); + m_inverters.setx(m.get_basic_family_id(), alloc(basic_expr_inverter, m), nullptr); + m_inverters.setx(a->get_fid(), a, nullptr); + m_inverters.setx(b->get_fid(), b, nullptr); + m_inverters.setx(ar->get_fid(), ar, nullptr); + m_inverters.setx(dt->get_fid(), dt, nullptr); +} + +bool expr_inverter::is_converted(func_decl* f, unsigned num, expr* const* args) { + return false; +} + +bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) { + if (num == 0) + return false; + + for (unsigned i = 0; i < num; i++) + if (!is_ground(args[i])) + return false; + + family_id fid = f->get_family_id(); + if (fid == null_family_id) + return false; + + if (is_converted(f, num, args)) + return false; + + auto* p = m_inverters.get(fid, nullptr); + return p && (*p)(f, num, args, new_expr, side_cond); +} + +bool expr_inverter::mk_diff(expr* t, expr_ref& r) { + sort * s = t->get_sort(); + if (!m.is_fully_interp(s)) + return false; + + // If the interpreted sort has only one element, + // then it is unsound to eliminate the unconstrained variable in the equality + sort_size sz = s->get_num_elements(); + if (sz.is_finite() && sz.size() <= 1) + return false; + + if (!m_mc) { + // easy case, model generation is disabled. + mk_fresh_uncnstr_var_for(s, r); + return true; + } + + family_id fid = s->get_family_id(); + auto* p = m_inverters.get(fid, nullptr); + return p && p->mk_diff(t, r); +} + +void expr_inverter::set_is_var(std::function& is_var) { + for (auto* p : m_inverters) + if (p) + p->set_is_var(is_var); +} + +void expr_inverter::set_model_converter(generic_model_converter* mc) { + for (auto* p : m_inverters) + if (p) + p->set_model_converter(mc); +} \ No newline at end of file diff --git a/src/ast/converters/expr_inverter.h b/src/ast/converters/expr_inverter.h new file mode 100644 index 00000000000..1ca77dbabe4 --- /dev/null +++ b/src/ast/converters/expr_inverter.h @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + expr_inverter.h + +Abstract: + + inverter interface and instance + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-11 + + +--*/ +#pragma once + +#include "ast/converters/generic_model_converter.h" + +class iexpr_inverter { +protected: + ast_manager& m; + std::function m_is_var; + generic_model_converter_ref m_mc; + + bool uncnstr(expr* e) const { return m_is_var(e); } + bool uncnstr(unsigned num, expr * const * args) const; + void mk_fresh_uncnstr_var_for(sort* s, expr_ref& v); + void mk_fresh_uncnstr_var_for(func_decl* f, expr_ref& v) { mk_fresh_uncnstr_var_for(f->get_range(), v); } + void add_def(expr * v, expr * def); + void add_defs(unsigned num, expr * const * args, expr * u, expr * identity); + +public: + iexpr_inverter(ast_manager& m): m(m) {} + virtual ~iexpr_inverter() {} + virtual void set_is_var(std::function& is_var) { m_is_var = is_var; } + virtual void set_model_converter(generic_model_converter* mc) { m_mc = mc; } + + virtual bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) = 0; + virtual bool mk_diff(expr* t, expr_ref& r) = 0; +}; + +class expr_inverter : public iexpr_inverter { + ptr_vector m_inverters; + + bool is_converted(func_decl* f, unsigned num, expr* const* args); + +public: + expr_inverter(ast_manager& m); + ~expr_inverter() override; + bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) override; + bool mk_diff(expr* t, expr_ref& r) override; + void set_is_var(std::function& is_var) override; + void set_model_converter(generic_model_converter* mc) override; +}; diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h index c20bfebb34d..85e8d03904d 100644 --- a/src/ast/converters/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -22,6 +22,7 @@ Module Name: #include "ast/converters/model_converter.h" class generic_model_converter : public model_converter { +public: enum instruction { HIDE, ADD }; struct entry { func_decl_ref m_f; @@ -30,6 +31,7 @@ class generic_model_converter : public model_converter { entry(func_decl* f, expr* d, ast_manager& m, instruction i): m_f(f, m), m_def(d, m), m_instruction(i) {} }; +private: ast_manager& m; std::string m_orig; vector m_entries; @@ -67,6 +69,8 @@ class generic_model_converter : public model_converter { void set_env(ast_pp_util* visitor) override; void get_units(obj_map& units) override; + + vector const& entries() const { return m_entries; } }; typedef ref generic_model_converter_ref; diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 0790b418df8..1e7b6da3b89 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -120,11 +120,11 @@ bool subterms::iterator::operator!=(iterator const& other) const { } -subterms_postorder::subterms_postorder(expr_ref_vector const& es): m_es(es) {} -subterms_postorder::subterms_postorder(expr_ref const& e) : m_es(e.m()) { if (e) m_es.push_back(e); } +subterms_postorder::subterms_postorder(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {} +subterms_postorder::subterms_postorder(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) { if (e) m_es.push_back(e); } subterms_postorder::iterator subterms_postorder::begin() { return iterator(*this, true); } subterms_postorder::iterator subterms_postorder::end() { return iterator(*this, false); } -subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_es(f.m_es) { +subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) { if (!start) m_es.reset(); next(); } @@ -153,6 +153,13 @@ void subterms_postorder::iterator::next() { } } } + else if (is_quantifier(e) && m_include_bound) { + expr* body = to_quantifier(e)->get_expr(); + if (!m_visited.is_marked(body)) { + m_es.push_back(body); + all_visited = false; + } + } if (all_visited) { m_visited.mark(e, true); break; diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 99a0f6b9d27..2d5ed05ae4f 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -200,9 +200,15 @@ class subterms { }; class subterms_postorder { + bool m_include_bound; expr_ref_vector m_es; + subterms_postorder(expr_ref_vector const& es, bool include_bound); + subterms_postorder(expr_ref const& e, bool include_bound); + + public: class iterator { + bool m_include_bound = false; expr_ref_vector m_es; expr_mark m_visited, m_seen; void next(); @@ -214,8 +220,10 @@ class subterms_postorder { bool operator==(iterator const& other) const; bool operator!=(iterator const& other) const; }; - subterms_postorder(expr_ref_vector const& es); - subterms_postorder(expr_ref const& e); + static subterms_postorder all(expr_ref_vector const& es) { return subterms_postorder(es, true); } + static subterms_postorder ground(expr_ref_vector const& es) { return subterms_postorder(es, false); } + static subterms_postorder all(expr_ref const& e) { return subterms_postorder(e, true); } + static subterms_postorder ground(expr_ref const& e) { return subterms_postorder(e, false); } iterator begin(); iterator end(); }; diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index ef04cc43371..75aa1ec7a87 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(simplifiers SOURCES bv_slice.cpp + elim_unconstrained.cpp euf_completion.cpp extract_eqs.cpp model_reconstruction_trail.cpp diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp new file mode 100644 index 00000000000..cbd575b6af7 --- /dev/null +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -0,0 +1,297 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + elim_unconstrained.cpp + +Abstract: + + Incremental, modular and more efficient version of elim_unconstr_tactic and + reduce_invertible_tactic. + + reduce_invertible_tactic should be subsumed by elim_unconstr_tactic + elim_unconstr_tactic has some built-in limitations that are not easy to fix with small changes: + - it is inefficient for examples like x <= y, y <= z, z <= u, ... + All variables x, y, z, .. can eventually be eliminated, but the tactic requires a global + analysis between each elimination. We address this by using reference counts and maintaining + a heap of reference counts. + - it does not accomodate side constraints. The more general invertibility reduction methods, such + as those introduced for bit-vectors use side constraints. + - it is not modular: we detach the expression invertion routines to self-contained code. + + Maintain a representation of terms as a set of nodes. + Each node has: + + - reference count = number of parents that are live + - orig - original term, the orig->get_id() is the index to the node + - term - current term representing the node after rewriting + - parents - list of parents where orig occurs. + + Subterms have reference counts + Elegible variables are inserted into a heap ordered by reference counts. + Variables that have reference count 1 are examined for invertibility. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-11. + +--*/ + + + +#include "ast/ast_ll_pp.h" +#include "ast/ast_pp.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/simplifiers/elim_unconstrained.h" + +elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) : + dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) { + + std::function is_var = [&](expr* e) { + return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount == 1; + }; + + m_inverter.set_is_var(is_var); +} + + +void elim_unconstrained::eliminate() { + + while (!m_heap.empty()) { + expr_ref r(m), side_cond(m); + int v = m_heap.erase_min(); + node& n = get_node(v); + IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n"); + if (n.m_refcount == 0) + continue; + if (n.m_refcount > 1) + return; + + if (n.m_parents.empty()) + continue; + expr* e = get_parent(v); + for (expr* p : n.m_parents) + IF_VERBOSE(11, verbose_stream() << "parent " << mk_pp(p, m) << "\n"); + if (!is_app(e)) + continue; + if (!is_ground(e)) + continue; + app* t = to_app(e); + m_args.reset(); + for (expr* arg : *to_app(t)) + m_args.push_back(get_node(arg).m_term); + if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) + continue; + + m_stats.m_num_eliminated++; + n.m_refcount = 0; + SASSERT(r); + m_trail.push_back(r); + gc(e); + + get_node(e).m_term = r; + get_node(e).m_refcount++; + IF_VERBOSE(11, verbose_stream() << mk_pp(e, m) << "\n"); + SASSERT(!m_heap.contains(e->get_id())); + if (is_uninterp_const(r)) + m_heap.insert(e->get_id()); + + IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " " << mk_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n"); + + SASSERT(!side_cond && "not implemented to add side conditions\n"); + } +} + +void elim_unconstrained::add_term(expr* t) { + expr_ref_vector terms(m); + terms.push_back(t); + init_terms(terms); +} + +expr* elim_unconstrained::get_parent(unsigned n) const { + for (expr* p : get_node(n).m_parents) + if (get_node(p).m_refcount > 0 && get_node(p).m_term == get_node(p).m_orig) + return p; + IF_VERBOSE(0, verbose_stream() << "term " << mk_pp(get_node(n).m_term, m) << "\n"); + for (expr* p : get_node(n).m_parents) + IF_VERBOSE(0, verbose_stream() << "parent " << mk_pp(p, m) << "\n"); + UNREACHABLE(); + return nullptr; +} +/** + * initialize node structure + */ +void elim_unconstrained::init_nodes() { + expr_ref_vector terms(m); + for (unsigned i = 0; i < m_fmls.size(); ++i) + terms.push_back(m_fmls[i].fml()); + m_trail.append(terms); + m_heap.reset(); + + init_terms(terms); + + for (expr* e : terms) + inc_ref(e); + + // freeze subterms before the head. + terms.reset(); + for (unsigned i = 0; i < m_qhead; ++i) + terms.push_back(m_fmls[i].fml()); + for (expr* e : subterms::all(terms)) + m_frozen.mark(e, true); + + + recfun::util rec(m); + if (rec.has_rec_defs()) { + for (func_decl* f : rec.get_rec_funs()) { + expr* rhs = rec.get_def(f).get_rhs(); + for (expr* t : subterms::all(expr_ref(rhs, m))) + m_frozen.mark(t); + } + } +} + +void elim_unconstrained::init_terms(expr_ref_vector const& terms) { + unsigned max_id = 0; + for (expr* e : subterms::all(terms)) + max_id = std::max(max_id, e->get_id()); + + m_nodes.reserve(max_id + 1); + m_heap.reserve(max_id + 1); + + for (expr* e : subterms_postorder::all(terms)) { + node& n = get_node(e); + if (n.m_term) + continue; + n.m_orig = e; + n.m_term = e; + n.m_refcount = 0; + if (is_uninterp_const(e)) + m_heap.insert(e->get_id()); + if (is_quantifier(e)) { + expr* body = to_quantifier(e)->get_expr(); + get_node(body).m_parents.push_back(e); + inc_ref(body); + } + else if (is_app(e)) { + for (expr* arg : *to_app(e)) { + get_node(arg).m_parents.push_back(e); + inc_ref(arg); + } + } + } +} + +void elim_unconstrained::gc(expr* t) { + ptr_vector todo; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + node& n = get_node(t); + if (n.m_refcount == 0) + continue; + dec_ref(t); + if (n.m_refcount != 0) + continue; + if (is_app(t)) { + for (expr* arg : *to_app(t)) + todo.push_back(arg); + } + else if (is_quantifier(t)) + todo.push_back(to_quantifier(t)->get_expr()); + } +} + +/** + * walk nodes starting from lowest depth and reconstruct their normalized forms. + */ +void elim_unconstrained::reconstruct_terms() { + expr_ref_vector terms(m); + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + terms.push_back(m_fmls[i].fml()); + + for (expr* e : subterms_postorder::all(terms)) { + node& n = get_node(e); + expr* t = n.m_term; + if (t != n.m_orig) + continue; + if (is_app(t)) { + bool change = false; + m_args.reset(); + for (expr* arg : *to_app(t)) { + node& n2 = get_node(arg); + m_args.push_back(n2.m_term); + change |= n2.m_term != n2.m_orig; + } + if (change) { + n.m_term = m.mk_app(to_app(t)->get_decl(), m_args); + m_trail.push_back(n.m_term); + } + } + else if (is_quantifier(t)) { + node& n2 = get_node(to_quantifier(t)->get_expr()); + if (n2.m_term != n2.m_orig) { + n.m_term = m.update_quantifier(to_quantifier(t), n2.m_term); + m_trail.push_back(n.m_term); + } + } + } +} + +void elim_unconstrained::assert_normalized(vector& old_fmls) { + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + auto [f, d] = m_fmls[i](); + node& n = get_node(f); + expr* g = n.m_term; + if (f == g) + continue; + old_fmls.push_back(m_fmls[i]); + m_fmls.update(i, dependent_expr(m, g, d)); + IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n"); + TRACE("elim_unconstrained", tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n"); + } +} + +void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector const& old_fmls) { + auto& trail = m_fmls.model_trail(); + scoped_ptr rp = mk_default_expr_replacer(m, false); + scoped_ptr sub = alloc(expr_substitution, m, true, false); + rp->set_substitution(sub.get()); + expr_ref new_def(m); + for (auto const& entry : mc.entries()) { + switch (entry.m_instruction) { + case generic_model_converter::instruction::HIDE: + break; + case generic_model_converter::instruction::ADD: + new_def = entry.m_def; + (*rp)(new_def); + sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr); + break; + } + } + trail.push(sub.detach(), old_fmls); + + for (auto const& entry : mc.entries()) { + switch (entry.m_instruction) { + case generic_model_converter::instruction::HIDE: + trail.push(entry.m_f); + break; + case generic_model_converter::instruction::ADD: + break; + } + } +} + +void elim_unconstrained::reduce() { + generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); + m_inverter.set_model_converter(mc.get()); + init_nodes(); + eliminate(); + reconstruct_terms(); + vector old_fmls; + assert_normalized(old_fmls); + update_model_trail(*mc, old_fmls); + advance_qhead(m_fmls.size()); +} diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h new file mode 100644 index 00000000000..327ceeff0b4 --- /dev/null +++ b/src/ast/simplifiers/elim_unconstrained.h @@ -0,0 +1,84 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + elim_unconstrained.h + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "util/heap.h" +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/converters/expr_inverter.h" + + +class elim_unconstrained : public dependent_expr_simplifier { + + struct node { + unsigned m_refcount; + expr* m_term; + expr* m_orig; + ptr_vector m_parents; + }; + struct var_lt { + elim_unconstrained& s; + var_lt(elim_unconstrained& s) : s(s) {} + bool operator()(int v1, int v2) const { + return s.get_node(v1).m_refcount < s.get_node(v2).m_refcount; + } + }; + struct stats { + unsigned m_num_eliminated = 0; + void reset() { m_num_eliminated = 0; } + }; + expr_inverter m_inverter; + vector m_nodes; + var_lt m_lt; + heap m_heap; + expr_ref_vector m_trail; + ptr_vector m_args; + expr_mark m_frozen; + stats m_stats; + + bool operator()(int v1, int v2) const { return get_node(v1).m_refcount < get_node(v2).m_refcount; } + + node& get_node(unsigned n) { return m_nodes[n]; } + node const& get_node(unsigned n) const { return m_nodes[n]; } + node& get_node(expr* t) { return m_nodes[t->get_id()]; } + node const& get_node(expr* t) const { return m_nodes[t->get_id()]; } + unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; } + void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); } + void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); } + void gc(expr* t); + + expr* get_parent(unsigned n) const; + void init_refcounts(); + void dec_refcounts(expr* t); + + void add_term(expr* t); + void init_terms(expr_ref_vector const& terms); + + void init_nodes(); + void eliminate(); + void reconstruct_terms(); + void assert_normalized(vector& old_fmls); + void update_model_trail(generic_model_converter& mc, vector const& old_fmls); + +public: + + elim_unconstrained(ast_manager& m, dependent_expr_state& fmls); + + void reduce() override; + + void collect_statistics(statistics& st) const override { st.update("elim-unconstr", m_stats.m_num_eliminated); } + + void reset_statistics() override { m_stats.reset(); } +}; diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 373a500bf21..a5f1cf8b030 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -30,6 +30,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vectorm_active) continue; + if (t->m_hide) + continue; + // updates that have no intersections with current variables are skipped if (!t->intersects(free_vars)) continue; @@ -79,6 +82,11 @@ model_converter_ref model_reconstruction_trail::get_model_converter() { if (!t->m_active) continue; + if (t->m_hide) { + mc->hide(t->m_hide); + continue; + } + if (first) { first = false; for (auto const& [v, def] : t->m_subst->sub()) { diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index c9b42bc9211..eeef136ee95 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -35,11 +35,14 @@ class model_reconstruction_trail { struct entry { scoped_ptr m_subst; vector m_removed; + func_decl* m_hide = nullptr; bool m_active = true; entry(expr_substitution* s, vector const& rem) : m_subst(s), m_removed(rem) {} + entry(func_decl* h) : m_hide(h) {} + bool is_loose() const { return !m_removed.empty(); } bool intersects(ast_mark const& free_vars) const { @@ -48,8 +51,6 @@ class model_reconstruction_trail { return true; return false; } - - }; ast_manager& m; @@ -81,6 +82,14 @@ class model_reconstruction_trail { */ void push(expr_substitution* s, vector const& removed) { m_trail.push_back(alloc(entry, s, removed)); + m_trail_stack.push(push_back_vector(m_trail)); + } + + /** + * add declaration to hide + */ + void push(func_decl* f) { + m_trail.push_back(alloc(entry, f)); m_trail_stack.push(push_back_vector(m_trail)); } diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 38d2699f0a2..bab61afce87 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -17,7 +17,6 @@ z3_add_component(core_tactics pb_preprocess_tactic.cpp propagate_values_tactic.cpp reduce_args_tactic.cpp - reduce_invertible_tactic.cpp simplify_tactic.cpp solve_eqs_tactic.cpp special_relations_tactic.cpp @@ -39,6 +38,7 @@ z3_add_component(core_tactics dom_simplify_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h + elim_uncnstr2_tactic.h euf_completion_tactic.h injectivity_tactic.h nnf_tactic.h @@ -46,7 +46,6 @@ z3_add_component(core_tactics pb_preprocess_tactic.h propagate_values_tactic.h reduce_args_tactic.h - reduce_invertible_tactic.h simplify_tactic.h solve_eqs_tactic.h solve_eqs2_tactic.h diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h new file mode 100644 index 00000000000..2c5f81d5e9d --- /dev/null +++ b/src/tactic/core/elim_uncnstr2_tactic.h @@ -0,0 +1,41 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + elim_unconstr2_tactic.h + +Abstract: + + Tactic for eliminating unconstrained terms. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ +#pragma once + +#include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/elim_unconstrained.h" +#include "ast/simplifiers/elim_unconstrained.h" + +class elim_uncnstr2_tactic_factory : public dependent_expr_simplifier_factory { +public: + dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { + return alloc(elim_unconstrained, m, s); + } +}; + +inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory), "elim-unconstr2"); +} + + +/* + ADD_TACTIC("elim-uncnstr2", "eliminate unconstrained variables.", "mk_elim_uncnstr2_tactic(m, p)") +*/ + + diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 34aa748d97c..5f0963bfda8 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -856,9 +856,8 @@ class elim_uncnstr_tactic : public tactic { void init_mc(bool produce_models) { m_mc = nullptr; - if (produce_models) { - m_mc = alloc(mc, m(), "elim_uncstr"); - } + if (produce_models) + m_mc = alloc(mc, m(), "elim_uncstr"); } void init_rw(bool produce_proofs) { @@ -872,7 +871,7 @@ class elim_uncnstr_tactic : public tactic { m_vars.reset(); collect_occs p; p(*g, m_vars); - if (m_vars.empty() || recfun::util(m()).has_defs()) { + if (m_vars.empty() || recfun::util(m()).has_rec_defs()) { result.push_back(g.get()); // did not increase depth since it didn't do anything. return; diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp deleted file mode 100644 index ba9b5d752b9..00000000000 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ /dev/null @@ -1,576 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - reduce_invertible_tactic.cpp - -Abstract: - - Reduce invertible variables. - -Author: - - Nuno Lopes (nlopes) 2018-6-30 - Nikolaj Bjorner (nbjorner) - -Notes: - - 1. Walk through top-level uninterpreted constants. - ---*/ - -#include "ast/bv_decl_plugin.h" -#include "ast/arith_decl_plugin.h" -#include "ast/ast_pp.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/rewriter/th_rewriter.h" -#include "tactic/tactic.h" -#include "tactic/core/reduce_invertible_tactic.h" -#include "tactic/core/collect_occs.h" -#include "ast/converters/generic_model_converter.h" -#include - -namespace { -class reduce_invertible_tactic : public tactic { - ast_manager& m; - bv_util m_bv; - arith_util m_arith; - -public: - reduce_invertible_tactic(ast_manager & m): - m(m), - m_bv(m), - m_arith(m) - {} - - char const* name() const override { return "reduce_invertible"; } - - tactic * translate(ast_manager & m) override { - return alloc(reduce_invertible_tactic, m); - } - - void operator()(goal_ref const & g, goal_ref_buffer & result) override { - tactic_report report("reduce-invertible", *g); - bool change = true; - while (change) { - change = false; - m_inverted.reset(); - m_parents.reset(); - collect_parents(g); - collect_occs occs; - obj_hashtable vars; - generic_model_converter_ref mc; - occs(*g, vars); - expr_safe_replace sub(m); - expr_ref new_v(m); - expr * p; - for (expr* v : vars) { - if (is_invertible(v, p, new_v, &mc)) { - mark_inverted(p); - sub.insert(p, new_v); - TRACE("invertible_tactic", tout << mk_pp(p, m) << " " << new_v << "\n";); - change = true; - break; - } - } - reduce_q_rw rw(*this); - unsigned sz = g->size(); - for (unsigned idx = 0; !g->inconsistent() && idx < sz; idx++) { - checkpoint(); - expr* f = g->form(idx); - expr_ref f_new(m); - sub(f, f_new); - rw(f_new, f_new); - if (f == f_new) continue; - proof_ref new_pr(m); - if (g->proofs_enabled()) { - proof * pr = g->pr(idx); - new_pr = m.mk_rewrite(f, f_new); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, f_new, new_pr, g->dep(idx)); - } - if (mc) g->add(mc.get()); - TRACE("invertible_tactic", g->display(tout);); - g->inc_depth(); - } - result.push_back(g.get()); - CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout);); - } - - void cleanup() override {} - -private: - void checkpoint() { - tactic::checkpoint(m); - } - - bool is_bv_neg(expr * e) { - if (m_bv.is_bv_neg(e)) - return true; - - expr *a, *b; - if (m_bv.is_bv_mul(e, a, b)) { - return m_bv.is_allone(a) || m_bv.is_allone(b); - } - return false; - } - - expr_mark m_inverted; - void mark_inverted(expr *p) { - ptr_buffer todo; - todo.push_back(p); - while (!todo.empty()) { - p = todo.back(); - todo.pop_back(); - if (!m_inverted.is_marked(p)) { - m_inverted.mark(p, true); - if (is_app(p)) { - for (expr* arg : *to_app(p)) { - todo.push_back(arg); - } - } - else if (is_quantifier(p)) { - todo.push_back(to_quantifier(p)->get_expr()); - } - } - } - } - - // store one parent of expression, or null if multiple - struct parents { - parents(): m_p(0) {} - uintptr_t m_p; - - void set(expr * e) { - SASSERT((uintptr_t)e != 1); - if (!m_p) m_p = (uintptr_t)e; - else m_p = 1; - } - - expr * get() const { - return m_p == 1 ? nullptr : (expr*)m_p; - } - }; - svector m_parents; - struct parent_collector { - reduce_invertible_tactic& c; - parent_collector(reduce_invertible_tactic& c):c(c) {} - void operator()(app* n) { - for (expr* arg : *n) { - c.m_parents.reserve(arg->get_id() + 1); - c.m_parents[arg->get_id()].set(n); - } - } - - void operator()(var* v) { - c.m_parents.reserve(v->get_id() + 1); - } - - void operator()(quantifier* q) {} - }; - - void collect_parents(goal_ref const& g) { - parent_collector proc(*this); - expr_fast_mark1 visited; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - checkpoint(); - quick_for_each_expr(proc, visited, g->form(i)); - } - } - - void ensure_mc(generic_model_converter_ref* mc) { - if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible"); - } - - bool is_full_domain_var(expr* v, rational& model) { - auto f = is_app(v) ? to_app(v)->get_decl() : nullptr; - if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0) - return false; - - switch (f->get_decl_kind()) { - case OP_BADD: - case OP_BSUB: - model = rational::zero(); - return true; - - case OP_BAND: - model = rational::power_of_two(m_bv.get_bv_size(v)) - rational::one(); - return true; - - case OP_BMUL: - model = rational::one(); - return true; - - case OP_BSDIV: - case OP_BSDIV0: - case OP_BSDIV_I: - case OP_BUDIV: - case OP_BUDIV0: - case OP_BUDIV_I: - default: - return false; - } - } - - bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) { - rational mdl; - if (!is_full_domain_var(v, mdl)) - return false; - - rational r; - app* a = to_app(v); - expr* fst_arg = a->get_arg(0); - - for (expr* arg : *a) - if (!m_parents[arg->get_id()].get()) - return false; - - if (is_var(fst_arg)) { - for (expr* arg : *a) { - if (!is_var(arg)) - return false; - if (to_var(arg)->get_idx() >= max_var) - return false; - } - } - else { - if (!is_uninterp_const(fst_arg)) - return false; - bool first = true; - for (expr* arg : *a) { - if (!is_app(arg)) - return false; - if (is_uninterp_const(arg)) - continue; - if (m_bv.is_numeral(arg, r) && r == mdl) { - if (first || mdl.is_zero()) { - first = false; - continue; - } - else - return false; - } - return false; - } - } - - if (mc) { - ensure_mc(mc); - expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m); - for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) { - expr* arg = a->get_arg(i); - if (m_bv.is_numeral(arg)) - continue; - (*mc)->add(arg, num); - } - } - new_v = fst_arg; - return true; - } - - // TBD: could be made to be recursive, by walking multiple layers of parents. - - bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) { - rational r; - if (m_parents.size() <= v->get_id()) { - return false; - } - p = m_parents[v->get_id()].get(); - if (!p || m_inverted.is_marked(p) || (mc && !is_ground(p))) { - return false; - } - - if (m_bv.is_bv_xor(p) || - m_bv.is_bv_not(p) || - is_bv_neg(p)) { - if (mc) { - ensure_mc(mc); - (*mc)->add(v, p); - } - new_v = v; - return true; - } - - if (rewrite_unconstr(p, new_v, mc, max_var)) - return true; - - if (m_bv.is_bv_add(p)) { - if (mc) { - ensure_mc(mc); - // if we solve for v' := v + t - // then the value for v is v' - t - expr_ref def(v, m); - for (expr* arg : *to_app(p)) { - if (arg != v) def = m_bv.mk_bv_sub(def, arg); - } - (*mc)->add(v, def); - } - new_v = v; - return true; - } - - if (m_bv.is_bv_mul(p)) { - expr_ref rest(m); - for (expr* arg : *to_app(p)) { - if (arg != v) { - if (rest) - rest = m_bv.mk_bv_mul(rest, arg); - else - rest = arg; - } - } - if (!rest) return false; - - // so far just support numeral - if (!m_bv.is_numeral(rest, r)) - return false; - - // create case split on - // divisbility of 2 - // v * t -> - // if t = 0, set v' := 0 and the solution for v is 0. - // otherwise, - // let i be the position of the least bit of t set to 1 - // then extract[sz-1:i](v) ++ zero[i-1:0] is the invertible of v * t - // thus - // extract[i+1:0](t) = 1 ++ zero[i-1:0] -> extract[sz-1:i](v) ++ zero[i-1:0] - // to reproduce the original v from t - // solve for v*t = extract[sz-1:i](v') ++ zero[i-1:0] - // using values for t and v' - // thus let t' = t / 2^i - // and t'' = the multiplicative inverse of t' - // then t'' * v' * t = t'' * v' * t' * 2^i = v' * 2^i = extract[sz-1:i](v') ++ zero[i-1:0] - // so t'' *v' works - // - unsigned sz = m_bv.get_bv_size(p); - expr_ref bit1(m_bv.mk_numeral(1, 1), m); - - - unsigned sh = 0; - while (r.is_pos() && r.is_even()) { - r /= rational(2); - ++sh; - } - if (r.is_pos() && sh > 0) - new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh)); - else - new_v = v; - if (mc && !r.is_zero()) { - ensure_mc(mc); - expr_ref def(m); - rational inv_r; - VERIFY(r.mult_inverse(sz, inv_r)); - def = m_bv.mk_bv_mul(m_bv.mk_numeral(inv_r, sz), v); - (*mc)->add(v, def); - TRACE("invertible_tactic", tout << def << "\n";); - } - return true; - } - if (m_bv.is_bv_sub(p)) { - // TBD - } - if (m_bv.is_bv_udivi(p)) { - // TBD - } - // sdivi, sremi, uremi, smodi - // TBD - - if (m_arith.is_mul(p) && m_arith.is_real(p)) { - expr_ref rest(m); - for (expr* arg : *to_app(p)) { - if (arg != v) { - if (rest) - rest = m_arith.mk_mul(rest, arg); - else - rest = arg; - } - } - if (!rest) return false; - if (!m_arith.is_numeral(rest, r) || r.is_zero()) - return false; - expr_ref zero(m_arith.mk_real(0), m); - new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v); - if (mc) { - ensure_mc(mc); - expr_ref def(m_arith.mk_div(v, rest), m); - (*mc)->add(v, def); - } - return true; - } - - - expr* e1 = nullptr, *e2 = nullptr; - - // v / t unless t != 0 - if (m_arith.is_div(p, e1, e2) && e1 == v && m_arith.is_numeral(e2, r) && !r.is_zero()) { - new_v = v; - if (mc) { - ensure_mc(mc); - (*mc)->add(v, m_arith.mk_mul(e1, e2)); - } - return true; - } - - if (m.is_eq(p, e1, e2)) { - TRACE("invertible_tactic", tout << mk_pp(v, m) << "\n";); - if (mc && has_diagonal(e1)) { - ensure_mc(mc); - new_v = m.mk_fresh_const("eq", m.mk_bool_sort()); - SASSERT(v == e1 || v == e2); - expr* other = (v == e1) ? e2 : e1; - (*mc)->hide(new_v); - (*mc)->add(v, m.mk_ite(new_v, other, mk_diagonal(other))); - return true; - } - else if (mc) { - // diagonal functions for other types depend on theory. - return false; - } - else if (is_var(v) && is_non_singleton_sort(v->get_sort())) { - new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort()); - return true; - } - } - - // - // v <= u - // => u + 1 == 0 or delta - // v := delta ? u : u + 1 - // - if (m_bv.is_bv_ule(p, e1, e2) && e1 == v && mc) { - ensure_mc(mc); - unsigned sz = m_bv.get_bv_size(e2); - expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m); - expr_ref succ_e2(m_bv.mk_bv_add(e2, m_bv.mk_numeral(1, sz)), m); - new_v = m.mk_or(delta, m.mk_eq(succ_e2, m_bv.mk_numeral(0, sz))); - (*mc)->hide(delta); - (*mc)->add(v, m.mk_ite(delta, e2, succ_e2)); - return true; - } - - // - // u <= v - // => u == 0 or delta - // v := delta ? u : u - 1 - // - if (m_bv.is_bv_ule(p, e1, e2) && e2 == v && mc) { - ensure_mc(mc); - unsigned sz = m_bv.get_bv_size(e1); - expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m); - expr_ref pred_e1(m_bv.mk_bv_sub(e1, m_bv.mk_numeral(1, sz)), m); - new_v = m.mk_or(delta, m.mk_eq(e1, m_bv.mk_numeral(0, sz))); - (*mc)->hide(delta); - (*mc)->add(v, m.mk_ite(delta, e1, pred_e1)); - return true; - } - return false; - } - - bool has_diagonal(expr* e) { - return - m_bv.is_bv(e) || - m.is_bool(e) || - m_arith.is_int_real(e); - } - - expr * mk_diagonal(expr* e) { - if (m_bv.is_bv(e)) return m_bv.mk_bv_not(e); - if (m.is_bool(e)) return m.mk_not(e); - if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e); - if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e); - UNREACHABLE(); - return e; - } - - bool is_non_singleton_sort(sort* s) { - if (m.is_uninterp(s)) return false; - sort_size sz = s->get_num_elements(); - if (sz.is_finite() && sz.size() == 1) return false; - return true; - } - - struct reduce_q_rw_cfg : public default_rewriter_cfg { - ast_manager& m; - reduce_invertible_tactic& t; - - reduce_q_rw_cfg(reduce_invertible_tactic& t): m(t.m), t(t) {} - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - if (is_lambda(old_q)) return false; - if (has_quantifiers(new_body)) return false; - ref_buffer vars(m); - ptr_buffer new_sorts; - unsigned n = old_q->get_num_decls(); - for (unsigned i = 0; i < n; ++i) { - sort* srt = old_q->get_decl_sort(i); - vars.push_back(m.mk_var(n - i - 1, srt)); - new_sorts.push_back(srt); - } - // for each variable, collect parents, - // ensure they are in unique location and not under other quantifiers. - // if they are invertible, then produce inverting expression. - // - expr_safe_replace sub(m); - t.m_parents.reset(); - t.m_inverted.reset(); - expr_ref new_v(m); - expr * p; - - { - parent_collector proc(t); - expr_fast_mark1 visited; - quick_for_each_expr(proc, visited, new_body); - } - bool has_new_var = false; - for (unsigned i = 0; i < vars.size(); ++i) { - var* v = vars[i]; - if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr, vars.size())) { - TRACE("invertible_tactic", tout << mk_pp(v, m) << " " << mk_pp(p, m) << "\n";); - t.mark_inverted(p); - sub.insert(p, new_v); - new_sorts[i] = new_v->get_sort(); - has_new_var |= new_v != v; - } - } - if (has_new_var) { - sub(new_body, result); - result = m.mk_quantifier(old_q->get_kind(), new_sorts.size(), new_sorts.data(), old_q->get_decl_names(), result, old_q->get_weight()); - result_pr = nullptr; - return true; - } - if (!sub.empty()) { - sub(new_body, result); - result = m.update_quantifier(old_q, old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns, result); - result_pr = nullptr; - return true; - } - return false; - } - - bool occurs_under_nested_q(var* v, expr* body) { - return has_quantifiers(body); - } - }; - - struct reduce_q_rw : rewriter_tpl { - reduce_q_rw_cfg m_cfg; - public: - reduce_q_rw(reduce_invertible_tactic& t): - rewriter_tpl(t.m, false, m_cfg), - m_cfg(t) {} - }; -}; -} - -tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const &) { - return alloc(reduce_invertible_tactic, m); -} diff --git a/src/tactic/core/reduce_invertible_tactic.h b/src/tactic/core/reduce_invertible_tactic.h deleted file mode 100644 index d40bf8a59d4..00000000000 --- a/src/tactic/core/reduce_invertible_tactic.h +++ /dev/null @@ -1,32 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - reduce_invertible_tactic.h - -Abstract: - - Reduce invertible variables. - -Author: - - Nuno Lopes (nlopes) 2018-6-30 - Nikolaj Bjorner (nbjorner) - -Notes: - ---*/ - -#pragma once -#include "util/params.h" - -class tactic; -class ast_manager; - -tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const & p = params_ref()); - -/* - ADD_TACTIC("reduce-invertible", "reduce invertible variable occurrences.", "mk_reduce_invertible_tactic(m, p)") -*/ - diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index 56e27ee9ac8..4190378396b 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -15,6 +15,7 @@ Module Name: Nikolaj Bjorner (nbjorner) 2022-11-2. --*/ +#pragma once #include "tactic/tactic.h" #include "ast/simplifiers/dependent_expr_state.h"