diff --git a/azure-pipelines.yml b/azure-pipelines.yml index f338a5d98..382c2efc9 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -202,7 +202,7 @@ jobs: setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env' setupCmd3: 'set /P JlCxxDir= 0) { unsigned d = ch & 0xF; if (d < 10) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index bbe212453..05df8186e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10079,7 +10079,7 @@ def FPs(names, fpsort, ctx=None): >>> x.ebits() 8 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) - fpMul(RNE(), fpAdd(RNE(), x, y), z) + x + y * z """ ctx = _get_ctx(ctx) if isinstance(names, str): @@ -10186,9 +10186,9 @@ def fpAdd(rm, a, b, ctx=None): >>> x = FP('x', s) >>> y = FP('y', s) >>> fpAdd(rm, x, y) - fpAdd(RNE(), x, y) - >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ x + y + >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ + fpAdd(RTZ(), x, y) >>> fpAdd(rm, x, y).sort() FPSort(8, 24) """ @@ -10203,7 +10203,7 @@ def fpSub(rm, a, b, ctx=None): >>> x = FP('x', s) >>> y = FP('y', s) >>> fpSub(rm, x, y) - fpSub(RNE(), x, y) + x - y >>> fpSub(rm, x, y).sort() FPSort(8, 24) """ @@ -10218,7 +10218,7 @@ def fpMul(rm, a, b, ctx=None): >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMul(rm, x, y) - fpMul(RNE(), x, y) + x * y >>> fpMul(rm, x, y).sort() FPSort(8, 24) """ @@ -10233,7 +10233,7 @@ def fpDiv(rm, a, b, ctx=None): >>> x = FP('x', s) >>> y = FP('y', s) >>> fpDiv(rm, x, y) - fpDiv(RNE(), x, y) + x / y >>> fpDiv(rm, x, y).sort() FPSort(8, 24) """ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 50b9e5a4d..7bb732a5d 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2250,7 +2250,9 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar if (type_error) { std::ostringstream buffer; buffer << "Wrong number of arguments (" << num_args - << ") passed to function " << mk_pp(decl, *this); + << ") passed to function " << mk_pp(decl, *this) << " "; + for (unsigned i = 0; i < num_args; ++i) + buffer << "\narg: " << mk_pp(args[i], *this) << "\n"; throw ast_exception(std::move(buffer).str()); } app * r = nullptr; diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 1cb17900f..37531d936 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -430,6 +430,9 @@ public: } app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args); } app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } + app * mk_concat(expr_ref_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } + app * mk_concat(ptr_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } + app * mk_concat(ptr_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args); } app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args); } app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args); } diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index 6d4b1b618..8f756e061 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -44,8 +44,10 @@ public: bool empty() const { return m_subst.empty(); } unsigned size() const { return m_subst.size(); } void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr); + void insert(expr* s, expr* def, expr_dependency* def_dep) { insert(s, def, nullptr, def_dep); } void erase(expr * s); - expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; } + expr* find(expr* s) { return m_subst[s]; } + expr_dependency* dep(expr* s) { return (*m_subst_dep)[s]; } bool find(expr * s, expr * & def, proof * & def_pr); bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep); bool contains(expr * s); @@ -57,6 +59,10 @@ public: std::ostream& display(std::ostream& out); }; +inline std::ostream& operator<<(std::ostream& out, expr_substitution& s) { + return s.display(out); +} + class scoped_expr_substitution { expr_substitution& m_subst; expr_ref_vector m_trail; diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 54e176fc5..0790b418d 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -64,15 +64,22 @@ bool has_skolem_functions(expr * n) { return false; } -subterms::subterms(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {} -subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) {if (e) m_es.push_back(e); } -subterms::iterator subterms::begin() { return iterator(*this, true); } -subterms::iterator subterms::end() { return iterator(*this, false); } -subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) { - if (!start) m_es.reset(); +subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {} +subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); } +subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); } +subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); } +subterms::iterator::iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) { + if (!esp) + m_esp = &m_es; + else + m_esp->reset(); + if (!m_visitedp) + m_visitedp = &m_visited; + if (start) + m_esp->append(f.m_es.size(), f.m_es.data()); } expr* subterms::iterator::operator*() { - return m_es.back(); + return m_esp->back(); } subterms::iterator subterms::iterator::operator++(int) { iterator tmp = *this; @@ -80,27 +87,29 @@ subterms::iterator subterms::iterator::operator++(int) { return tmp; } subterms::iterator& subterms::iterator::operator++() { - expr* e = m_es.back(); - m_visited.mark(e, true); + expr* e = m_esp->back(); + // IF_VERBOSE(0, verbose_stream() << e->get_ref_count() << "\n"); + SASSERT(e->get_ref_count() > 0); + m_visitedp->mark(e, true); if (is_app(e)) for (expr* arg : *to_app(e)) - m_es.push_back(arg); + m_esp->push_back(arg); else if (is_quantifier(e) && m_include_bound) - m_es.push_back(to_quantifier(e)->get_expr()); + m_esp->push_back(to_quantifier(e)->get_expr()); - while (!m_es.empty() && m_visited.is_marked(m_es.back())) - m_es.pop_back(); + while (!m_esp->empty() && m_visitedp->is_marked(m_esp->back())) + m_esp->pop_back(); return *this; } bool subterms::iterator::operator==(iterator const& other) const { // ignore state of visited - if (other.m_es.size() != m_es.size()) { + if (other.m_esp->size() != m_esp->size()) { return false; } - for (unsigned i = m_es.size(); i-- > 0; ) { - if (m_es.get(i) != other.m_es.get(i)) + for (unsigned i = m_esp->size(); i-- > 0; ) { + if (m_esp->get(i) != other.m_esp->get(i)) return false; } return true; diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index b724bed86..99a0f6b9d 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -170,15 +170,20 @@ bool has_skolem_functions(expr * n); class subterms { bool m_include_bound = false; expr_ref_vector m_es; - subterms(expr_ref const& e, bool include_bound); - subterms(expr_ref_vector const& es, bool include_bound); + ptr_vector* m_esp = nullptr; + expr_mark* m_vp = nullptr; + subterms(expr_ref const& e, bool include_bound, ptr_vector* esp, expr_mark* vp); + subterms(expr_ref_vector const& es, bool include_bound, ptr_vector* esp, expr_mark* vp); public: + ~subterms() { if (m_vp) m_vp->reset(); } class iterator { - bool m_include_bound = false; - expr_ref_vector m_es; - expr_mark m_visited; + bool m_include_bound = false; + ptr_vector m_es; + ptr_vector* m_esp = nullptr; + expr_mark m_visited; + expr_mark* m_visitedp = nullptr; public: - iterator(subterms& f, bool start); + iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start); expr* operator*(); iterator operator++(int); iterator& operator++(); @@ -186,11 +191,10 @@ public: bool operator!=(iterator const& other) const; }; - - static subterms all(expr_ref const& e) { return subterms(e, true); } - static subterms ground(expr_ref const& e) { return subterms(e, false); } - static subterms all(expr_ref_vector const& e) { return subterms(e, true); } - static subterms ground(expr_ref_vector const& e) { return subterms(e, false); } + static subterms all(expr_ref const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); } + static subterms ground(expr_ref const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } + static subterms all(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); } + static subterms ground(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } iterator begin(); iterator end(); }; diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index d0398543b..a35956454 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -22,6 +22,7 @@ Notes: #include "ast/normal_forms/nnf.h" #include "ast/normal_forms/nnf_params.hpp" #include "ast/used_vars.h" +#include "ast/ast_util.h" #include "ast/well_sorted.h" #include "ast/act_cache.h" #include "ast/rewriter/var_subst.h" @@ -137,7 +138,7 @@ class skolemizer { if (is_sk_hack(p)) { expr * sk_hack = to_app(p)->get_arg(0); if (q->get_kind() == forall_k) // check whether is in negative/positive context. - tmp = m.mk_or(body, m.mk_not(sk_hack)); // negative context + tmp = m.mk_or(body, mk_not(m, sk_hack)); // negative context else tmp = m.mk_and(body, sk_hack); // positive context body = tmp; @@ -148,7 +149,7 @@ class skolemizer { p = nullptr; if (m_proofs_enabled) { if (q->get_kind() == forall_k) - p = m.mk_skolemization(m.mk_not(q), m.mk_not(r)); + p = m.mk_skolemization(mk_not(m, q), mk_not(m, r)); else p = m.mk_skolemization(q, r); } @@ -388,7 +389,7 @@ struct nnf::imp { } void skip(expr * t, bool pol) { - expr * r = pol ? t : m.mk_not(t); + expr * r = pol ? t : mk_not(m, t); m_result_stack.push_back(r); if (proofs_enabled()) { m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r)); @@ -639,7 +640,7 @@ struct nnf::imp { m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); if (!fr.m_pol) - n2 = m.mk_not(n2); + n2 = mk_not(m, n2); m_result_stack.push_back(n2); if (proofs_enabled()) { if (!fr.m_pol) { diff --git a/src/ast/occurs.cpp b/src/ast/occurs.cpp index 21e7f5906..2bcd98396 100644 --- a/src/ast/occurs.cpp +++ b/src/ast/occurs.cpp @@ -74,3 +74,46 @@ bool occurs(func_decl * d, expr * n) { return false; } +void mark_occurs(ptr_vector& to_check, expr* v, expr_mark& occ) { + expr_fast_mark2 visited; + occ.mark(v, true); + visited.mark(v, true); + while (!to_check.empty()) { + expr* e = to_check.back(); + if (visited.is_marked(e)) { + to_check.pop_back(); + continue; + } + if (is_app(e)) { + bool does_occur = false; + bool all_visited = true; + for (expr* arg : *to_app(e)) { + if (!visited.is_marked(arg)) { + to_check.push_back(arg); + all_visited = false; + } + else + does_occur |= occ.is_marked(arg); + } + if (all_visited) { + occ.mark(e, does_occur); + visited.mark(e, true); + to_check.pop_back(); + } + } + else if (is_quantifier(e)) { + expr* body = to_quantifier(e)->get_expr(); + if (visited.is_marked(body)) { + visited.mark(e, true); + occ.mark(e, occ.is_marked(body)); + to_check.pop_back(); + } + else + to_check.push_back(body); + } + else { + visited.mark(e, true); + to_check.pop_back(); + } + } +} \ No newline at end of file diff --git a/src/ast/occurs.h b/src/ast/occurs.h index 15a33ddf5..7475a292c 100644 --- a/src/ast/occurs.h +++ b/src/ast/occurs.h @@ -18,8 +18,8 @@ Revision History: --*/ #pragma once -class expr; -class func_decl; +#include "util/vector.h" +#include "ast/ast.h" /** \brief Return true if n1 occurs in n2 @@ -31,4 +31,9 @@ bool occurs(expr * n1, expr * n2); */ bool occurs(func_decl * d, expr * n); +/** +* \brief Mark sub-expressions of to_check by whether v occurs in these. +*/ +void mark_occurs(ptr_vector& to_check, expr* v, expr_mark& occurs); + diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index bf865b393..558488592 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -442,17 +442,18 @@ namespace recfun { return promise_def(&u(), d); } - void plugin::inherit(decl_plugin* other, ast_translation& tr) { - for (auto [k, v] : static_cast(other)->m_defs) { + void plugin::inherit(decl_plugin* _other, ast_translation& tr) { + plugin* other = static_cast(_other); + for (auto [k, v] : other->m_defs) { func_decl_ref f(tr(k), tr.to()); if (m_defs.contains(f)) continue; def* d = v->copy(u(), tr); m_defs.insert(f, d); for (case_def & c : d->get_cases()) - m_case_defs.insert(c.get_decl(), &c); - + m_case_defs.insert(c.get_decl(), &c); } + m_has_rec_defs = other->m_has_rec_defs; } promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { @@ -473,6 +474,7 @@ namespace recfun { } void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { + m_has_rec_defs |= !is_macro; u().set_definition(r, d, is_macro, n_vars, vars, rhs); for (case_def & c : d.get_def()->get_cases()) m_case_defs.insert(c.get_decl(), &c); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 8e1279c0a..c369e2827 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -165,6 +165,7 @@ namespace recfun { mutable scoped_ptr m_util; def_map m_defs; // function->def case_def_map m_case_defs; // case_pred->def + bool m_has_rec_defs = false; ast_manager & m() { return *m_manager; } @@ -200,6 +201,7 @@ namespace recfun { bool has_def(func_decl* f) const { return m_defs.contains(f); } bool has_defs() const; + bool has_rec_defs() const { return m_has_rec_defs; } def const& get_def(func_decl* f) const { return *(m_defs[f]); } promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); } def& get_def(func_decl* f) { return *(m_defs[f]); } @@ -249,6 +251,8 @@ namespace recfun { //has_defs(); } + bool has_rec_defs() const { return m_plugin->has_rec_defs(); } + //get_num_args(); \ - for (unsigned j = 0; j < sz; j++) { \ - expr * arg_arg = to_app(arg)->get_arg(j); \ + for (expr * arg_arg : *to_app(arg)) { \ push_new_arg(arg_arg, new_args, neg_lits, pos_lits); \ } \ } \ diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index a25a0f8a3..2cec0b2ce 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -20,6 +20,7 @@ Notes: #include "ast/ast.h" #include "ast/rewriter/rewriter.h" +#include "ast/rewriter/hoist_rewriter.h" #include "util/params.h" /** @@ -50,6 +51,7 @@ Notes: */ class bool_rewriter { ast_manager & m_manager; + hoist_rewriter m_hoist; bool m_flat_and_or; bool m_local_ctx; bool m_elim_and; @@ -78,7 +80,7 @@ class bool_rewriter { void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits); public: - bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); } + bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { updt_params(p); } ast_manager & m() const { return m_manager; } family_id get_fid() const { return m().get_basic_family_id(); } bool is_eq(expr * t) const { return m().is_eq(t); } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index a04436e63..209f7a13b 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -1513,11 +1513,14 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re bool fused_numeral = false; bool expanded = false; bool fused_extract = false; + bool eq_args = true; for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; expr * prev = nullptr; - if (i > 0) + if (i > 0) { prev = new_args.back(); + eq_args &= prev == arg; + } if (is_numeral(arg, v1, sz1) && prev != nullptr && is_numeral(prev, v2, sz2)) { v2 *= rational::power_of_two(sz1); v2 += v1; @@ -1526,10 +1529,8 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re fused_numeral = true; } else if (m_flat && m_util.is_concat(arg)) { - unsigned num2 = to_app(arg)->get_num_args(); - for (unsigned j = 0; j < num2; j++) { - new_args.push_back(to_app(arg)->get_arg(j)); - } + for (expr* arg2 : *to_app(arg)) + new_args.push_back(arg2); expanded = true; } else if (m_util.is_extract(arg) && @@ -1539,8 +1540,8 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re m_util.get_extract_low(prev) == m_util.get_extract_high(arg) + 1) { // (concat (extract[h1,l1] a) (extract[h2,l2] a)) --> (extract[h1,l2] a) if l1 == h2+1 expr * new_arg = m_mk_extract(m_util.get_extract_high(prev), - m_util.get_extract_low(arg), - to_app(arg)->get_arg(0)); + m_util.get_extract_low(arg), + to_app(arg)->get_arg(0)); new_args.pop_back(); new_args.push_back(new_arg); fused_extract = true; @@ -1549,14 +1550,26 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re new_args.push_back(arg); } } - if (!fused_numeral && !expanded && !fused_extract) + if (!fused_numeral && !expanded && !fused_extract) { + expr* x, *y, *z; + if (eq_args) { + if (m().is_ite(new_args.back(), x, y, z)) { + ptr_buffer args1, args2; + for (expr* arg : new_args) + args1.push_back(y), args2.push_back(z); + result = m().mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2)); + return BR_REWRITE2; + } + } return BR_FAILED; + + } SASSERT(!new_args.empty()); if (new_args.size() == 1) { result = new_args.back(); return fused_extract ? BR_REWRITE1 : BR_DONE; } - result = m_util.mk_concat(new_args.size(), new_args.data()); + result = m_util.mk_concat(new_args); if (fused_extract) return BR_REWRITE2; else if (expanded) @@ -2013,6 +2026,19 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { return BR_REWRITE2; } + expr* x, *y, *z; + if (m().is_ite(arg, x, y, z) && m_util.is_numeral(y, val, bv_size)) { + val = bitwise_not(bv_size, val); + result = m().mk_ite(x, m_util.mk_numeral(val, bv_size), m_util.mk_bv_not(z)); + return BR_REWRITE2; + } + + if (m().is_ite(arg, x, y, z) && m_util.is_numeral(z, val, bv_size)) { + val = bitwise_not(bv_size, val); + result = m().mk_ite(x, m_util.mk_bv_not(y), m_util.mk_numeral(val, bv_size)); + return BR_REWRITE2; + } + if (m_bvnot_simpl) { expr *s(nullptr), *t(nullptr); if (m_util.is_bv_mul(arg, s, t)) { diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index 4fa83bed0..1007261ae 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -25,6 +25,11 @@ void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_p operator()(t, result, result_pr, result_dep); } +void expr_replacer::operator()(expr* t, expr_ref& result, expr_dependency_ref& result_dep) { + proof_ref result_pr(m()); + operator()(t, result, result_pr, result_dep); +} + void expr_replacer::operator()(expr * t, expr_ref & result) { proof_ref pr(m()); operator()(t, result, pr); diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index 82982adff..96418f00b 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -34,9 +34,12 @@ public: virtual void set_substitution(expr_substitution * s) = 0; virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & deps) = 0; - virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr); - virtual void operator()(expr * t, expr_ref & result); - virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } + void operator()(expr* t, expr_ref& result, expr_dependency_ref& deps); + void operator()(expr * t, expr_ref & result, proof_ref & result_pr); + void operator()(expr * t, expr_ref & result); + void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } + void operator()(expr_ref_vector& v) { expr_ref t(m()); for (unsigned i = 0; i < v.size(); ++i) (*this)(v.get(i), t), v[i] = t; } + std::pair replace_with_dep(expr* t) { expr_ref r(m()); expr_dependency_ref d(m()); (*this)(t, r, d); return { r, d }; } virtual unsigned get_num_steps() const { return 0; } virtual void reset() = 0; diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index 4116945f0..40ad4604a 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -13,8 +13,6 @@ Author: Nikolaj Bjorner (nbjorner) 2019-2-4 -Notes: - --*/ @@ -25,19 +23,17 @@ Notes: hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p): - m_manager(m), m_args1(m), m_args2(m), m_subst(m) { + m(m), m_args1(m), m_args2(m), m_subst(m) { updt_params(p); } br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) { - if (num_args < 2) { + if (num_args < 2) return BR_FAILED; - } - for (unsigned i = 0; i < num_args; ++i) { - if (!is_and(es[i], nullptr)) { + + for (unsigned i = 0; i < num_args; ++i) + if (!is_and(es[i], nullptr)) return BR_FAILED; - } - } bool turn = false; m_preds1.reset(); @@ -52,12 +48,10 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & VERIFY(is_and(es[0], args[turn])); expr* e1, *e2; for (expr* e : *(args[turn])) { - if (m().is_eq(e, e1, e2)) { + if (m.is_eq(e, e1, e2)) (*uf)[turn].merge(mk_var(e1), mk_var(e2)); - } - else { + else (*preds)[turn].insert(e); - } } unsigned round = 0; for (unsigned j = 1; j < num_args; ++j) { @@ -72,44 +66,39 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & VERIFY(is_and(es[j], args[turn])); for (expr* e : *args[turn]) { - if (m().is_eq(e, e1, e2)) { + if (m.is_eq(e, e1, e2)) { m_es.push_back(e1); m_uf0.merge(mk_var(e1), mk_var(e2)); } - else if ((*preds)[last].contains(e)) { + else if ((*preds)[last].contains(e)) (*preds)[turn].insert(e); - } } - if ((*preds)[turn].empty() && m_es.empty()) { + if ((*preds)[turn].empty() && m_es.empty()) return BR_FAILED; - } m_eqs.reset(); for (expr* e : m_es) { - if (m_mark.is_marked(e)) { + if (m_mark.is_marked(e)) continue; - } unsigned u = mk_var(e); unsigned v = u; m_roots.reset(); do { m_mark.mark(e); unsigned r = (*uf)[last].find(v); - if (m_roots.find(r, e2)) { - m_eqs.push_back(std::make_pair(e, e2)); - } - else { + if (m_roots.find(r, e2)) + m_eqs.push_back({e, e2}); + else m_roots.insert(r, e); - } v = m_uf0.next(v); e = mk_expr(v); } while (u != v); } reset((*uf)[turn]); - for (auto const& p : m_eqs) - (*uf)[turn].merge(mk_var(p.first), mk_var(p.second)); + for (auto const& [e1, e2] : m_eqs) + (*uf)[turn].merge(mk_var(e1), mk_var(e2)); if ((*preds)[turn].empty() && m_eqs.empty()) return BR_FAILED; } @@ -118,25 +107,23 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & return BR_DONE; } // p & eqs & (or fmls) - expr_ref_vector fmls(m()); + expr_ref_vector fmls(m); m_subst.reset(); for (expr * p : (*preds)[turn]) { expr* q = nullptr; - if (m().is_not(p, q)) { - m_subst.insert(q, m().mk_false()); - } - else { - m_subst.insert(p, m().mk_true()); - } + if (m.is_not(p, q)) + m_subst.insert(q, m.mk_false()); + else + m_subst.insert(p, m.mk_true()); fmls.push_back(p); } for (auto& p : m_eqs) { - if (m().is_value(p.first)) + if (m.is_value(p.first)) std::swap(p.first, p.second); m_subst.insert(p.first, p.second); - fmls.push_back(m().mk_eq(p.first, p.second)); + fmls.push_back(m.mk_eq(p.first, p.second)); } - expr_ref ors(::mk_or(m(), num_args, es), m()); + expr_ref ors(::mk_or(m, num_args, es), m); m_subst(ors); fmls.push_back(ors); result = mk_and(fmls); @@ -146,9 +133,8 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & unsigned hoist_rewriter::mk_var(expr* e) { unsigned v = 0; - if (m_expr2var.find(e, v)) { + if (m_expr2var.find(e, v)) return v; - } m_uf1.mk_var(); v = m_uf2.mk_var(); SASSERT(v == m_var2expr.size()); @@ -158,15 +144,14 @@ unsigned hoist_rewriter::mk_var(expr* e) { } expr_ref hoist_rewriter::hoist_predicates(obj_hashtable const& preds, unsigned num_args, expr* const* es) { - expr_ref result(m()); - expr_ref_vector args(m()), fmls(m()); + expr_ref result(m); + expr_ref_vector args(m), fmls(m); for (unsigned i = 0; i < num_args; ++i) { VERIFY(is_and(es[i], &m_args1)); fmls.reset(); - for (expr* e : m_args1) { + for (expr* e : m_args1) if (!preds.contains(e)) fmls.push_back(e); - } args.push_back(::mk_and(fmls)); } fmls.reset(); @@ -188,19 +173,18 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c } bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) { - if (m().is_and(e)) { + if (m.is_and(e)) { if (args) { args->reset(); args->append(to_app(e)->get_num_args(), to_app(e)->get_args()); } return true; } - if (m().is_not(e, e) && m().is_or(e)) { + if (m.is_not(e, e) && m.is_or(e)) { if (args) { args->reset(); - for (expr* arg : *to_app(e)) { - args->push_back(::mk_not(m(), arg)); - } + for (expr* arg : *to_app(e)) + args->push_back(::mk_not(m, arg)); } return true; } diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h index 2c627ad59..cc83bfa56 100644 --- a/src/ast/rewriter/hoist_rewriter.h +++ b/src/ast/rewriter/hoist_rewriter.h @@ -26,7 +26,7 @@ Notes: #include "util/obj_hashtable.h" class hoist_rewriter { - ast_manager & m_manager; + ast_manager & m; expr_ref_vector m_args1, m_args2; obj_hashtable m_preds1, m_preds2; basic_union_find m_uf1, m_uf2, m_uf0; @@ -34,11 +34,9 @@ class hoist_rewriter { svector> m_eqs; u_map m_roots; expr_safe_replace m_subst; - obj_map m_expr2var; - ptr_vector m_var2expr; - expr_mark m_mark; - - br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); + obj_map m_expr2var; + ptr_vector m_var2expr; + expr_mark m_mark; bool is_and(expr* e, expr_ref_vector* args); @@ -52,12 +50,12 @@ class hoist_rewriter { public: hoist_rewriter(ast_manager & m, params_ref const & p = params_ref()); - ast_manager& m() const { return m_manager; } - family_id get_fid() const { return m().get_basic_family_id(); } - bool is_eq(expr * t) const { return m().is_eq(t); } + family_id get_fid() const { return m.get_basic_family_id(); } + bool is_eq(expr * t) const { return m.is_eq(t); } void updt_params(params_ref const & p) {} static void get_param_descrs(param_descrs & r) {} br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); }; struct hoist_rewriter_cfg : public default_rewriter_cfg { diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 96b69dbc3..9604f6d16 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -924,6 +924,11 @@ void th_rewriter::get_param_descrs(param_descrs & r) { rewriter_params::collect_param_descrs(r); } +void th_rewriter::set_flat_and_or(bool f) { + m_imp->cfg().m_b_rw.set_flat_and_or(f); +} + + th_rewriter::~th_rewriter() { dealloc(m_imp); } diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index e432678a4..b84164abc 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -38,6 +38,9 @@ public: void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); + + void set_flat_and_or(bool f); + unsigned get_cache_size() const; unsigned get_num_steps() const; diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index dc7aa6fb6..ef04cc433 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -4,6 +4,7 @@ z3_add_component(simplifiers euf_completion.cpp extract_eqs.cpp model_reconstruction_trail.cpp + solve_context_eqs.cpp solve_eqs.cpp COMPONENT_DEPENDENCIES euf diff --git a/src/ast/simplifiers/bv_slice.cpp b/src/ast/simplifiers/bv_slice.cpp index f39fa932e..75e0a890c 100644 --- a/src/ast/simplifiers/bv_slice.cpp +++ b/src/ast/simplifiers/bv_slice.cpp @@ -109,12 +109,12 @@ namespace bv { }; if (lo > 0 && !b.contains(lo)) { b.insert(lo); - if (m_num_scopes > 0) + if (num_scopes() > 0) m_trail.push(remove_set(b, lo)); } if (hi + 1 < sz && !b.contains(hi + 1)) { b.insert(hi + 1); - if (m_num_scopes > 0) + if (num_scopes() > 0) m_trail.push(remove_set(b, hi+ 1)); } } diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h index 9d6d8625e..f789bf332 100644 --- a/src/ast/simplifiers/dependent_expr.h +++ b/src/ast/simplifiers/dependent_expr.h @@ -68,6 +68,12 @@ public: m_fml = nullptr; m_dep = nullptr; } + + ast_manager& get_manager() const { return m; } + + expr* fml() const { return m_fml; } + + expr_dependency* dep() const { return m_dep; } std::tuple operator()() const { return { m_fml, m_dep }; diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 32ad59681..27dcf82e0 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -34,6 +34,8 @@ Author: #include "util/params.h" #include "ast/converters/model_converter.h" #include "ast/simplifiers/dependent_expr.h" +#include "ast/simplifiers/model_reconstruction_trail.h" + /** @@ -46,6 +48,12 @@ public: virtual dependent_expr const& operator[](unsigned i) = 0; virtual void update(unsigned i, dependent_expr const& j) = 0; virtual bool inconsistent() = 0; + virtual model_reconstruction_trail& model_trail() = 0; + + trail_stack m_trail; + void push() { m_trail.push_scope(); } + void pop(unsigned n) { m_trail.pop_scope(n); } + }; /** @@ -55,20 +63,21 @@ class dependent_expr_simplifier { protected: ast_manager& m; dependent_expr_state& m_fmls; - unsigned m_qhead = 0; // pointer into last processed formula in m_fmls - unsigned m_num_scopes = 0; - trail_stack m_trail; - void advance_qhead(unsigned sz) { if (m_num_scopes > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; } + trail_stack& m_trail; + unsigned m_qhead = 0; // pointer into last processed formula in m_fmls + + unsigned num_scopes() const { return m_trail.get_num_scopes(); } + + void advance_qhead(unsigned sz) { if (num_scopes() > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; } public: - dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s) {} + dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {} virtual ~dependent_expr_simplifier() {} - virtual void push() { m_num_scopes++; m_trail.push_scope(); } - virtual void pop(unsigned n) { m_num_scopes -= n; m_trail.pop_scope(n); } + virtual void push() { } + virtual void pop(unsigned n) { } virtual void reduce() = 0; virtual void collect_statistics(statistics& st) const {} virtual void reset_statistics() {} virtual void updt_params(params_ref const& p) {} - virtual model_converter_ref get_model_converter() { return model_converter_ref(); } }; /** diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index e5b328d7f..e1360fa0b 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -213,7 +213,7 @@ namespace euf { old_value = nullptr; } }; - if (m_num_scopes > 0) + if (num_scopes() > 0) m_trail.push(vtrail(m_canonical, n->get_id())); m_canonical.setx(n->get_id(), e); m_epochs.setx(n->get_id(), m_epoch, 0); diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index 1e9b576e1..f6c914fab 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -29,22 +29,36 @@ namespace euf { class basic_extract_eq : public extract_eq { ast_manager& m; bool m_ite_solver = true; + bool m_allow_bool = true; + public: basic_extract_eq(ast_manager& m) : m(m) {} + virtual void set_allow_booleans(bool f) { + m_allow_bool = f; + } + + void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { auto [f, d] = e(); expr* x, * y; if (m.is_eq(f, x, y)) { + if (x == y) + return; + if (!m_allow_bool && m.is_bool(x)) + return; if (is_uninterp_const(x)) - eqs.push_back(dependent_eq(to_app(x), expr_ref(y, m), d)); + eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(y, m), d)); if (is_uninterp_const(y)) - eqs.push_back(dependent_eq(to_app(y), expr_ref(x, m), d)); + eqs.push_back(dependent_eq(e.fml(), to_app(y), expr_ref(x, m), d)); } expr* c, * th, * el, * x1, * y1, * x2, * y2; if (m_ite_solver && m.is_ite(f, c, th, el)) { if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) { + if (!m_allow_bool && m.is_bool(x1)) + return; + if (x1 == y2 && is_uninterp_const(x1)) std::swap(x2, y2); if (x2 == y2 && is_uninterp_const(x2)) @@ -52,13 +66,15 @@ namespace euf { if (x2 == y1 && is_uninterp_const(x2)) std::swap(x1, y1); if (x1 == x2 && is_uninterp_const(x1)) - eqs.push_back(dependent_eq(to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d)); + eqs.push_back(dependent_eq(e.fml(), to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d)); } } + if (!m_allow_bool) + return; if (is_uninterp_const(f)) - eqs.push_back(dependent_eq(to_app(f), expr_ref(m.mk_true(), m), d)); + eqs.push_back(dependent_eq(e.fml(), to_app(f), expr_ref(m.mk_true(), m), d)); if (m.is_not(f, x) && is_uninterp_const(x)) - eqs.push_back(dependent_eq(to_app(x), expr_ref(m.mk_false(), m), d)); + eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(m.mk_false(), m), d)); } void updt_params(params_ref const& p) { @@ -76,7 +92,7 @@ namespace euf { // solve u mod r1 = y -> u = r1*mod!1 + y - void solve_mod(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + void solve_mod(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { expr* u, * z; rational r1, r2; if (!a.is_mod(x, u, z)) @@ -87,7 +103,11 @@ namespace euf { return; expr_ref term(m); term = a.mk_add(a.mk_mul(z, m.mk_fresh_const("mod", a.mk_int())), y); - solve_eq(u, term, d, eqs); + + if (is_uninterp_const(u)) + eqs.push_back(dependent_eq(orig, to_app(u), term, d)); + else + solve_eq(orig, u, term, d, eqs); } /*** @@ -96,7 +116,7 @@ namespace euf { * -1*x + Y = Z -> x = Y - Z * a*x + Y = Z -> x = (Z - Y)/a for is-real(x) */ - void solve_add(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { if (!a.is_add(x)) return; expr* u, * z; @@ -115,18 +135,18 @@ namespace euf { for (expr* arg : *to_app(x)) { if (is_uninterp_const(arg)) { mk_term(i); - eqs.push_back(dependent_eq(to_app(arg), term, d)); + eqs.push_back(dependent_eq(orig, to_app(arg), term, d)); } else if (a.is_mul(arg, u, z) && a.is_numeral(u, r) && is_uninterp_const(z)) { if (r == -1) { mk_term(i); term = a.mk_uminus(term); - eqs.push_back(dependent_eq(to_app(z), term, d)); + eqs.push_back(dependent_eq(orig, to_app(z), term, d)); } else if (a.is_real(arg) && r != 0) { mk_term(i); term = a.mk_div(term, u); - eqs.push_back(dependent_eq(to_app(z), term, d)); + eqs.push_back(dependent_eq(orig, to_app(z), term, d)); } } else if (a.is_real(arg) && a.is_mul(arg)) { @@ -155,7 +175,7 @@ namespace euf { } mk_term(i); term = a.mk_div(term, a.mk_mul(args.size(), args.data())); - eqs.push_back(dependent_eq(to_app(xarg), term, d)); + eqs.push_back(dependent_eq(orig, to_app(xarg), term, d)); } } ++i; @@ -165,7 +185,7 @@ namespace euf { /*** * Solve for x * Y = Z, where Y != 0 -> x = Z / Y */ - void solve_mul(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + void solve_mul(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { if (!a.is_mul(x)) return; rational r; @@ -175,6 +195,8 @@ namespace euf { ++i; if (!is_uninterp_const(arg)) continue; + if (!a.is_real(arg)) + continue; unsigned j = 0; bool nonzero = true; for (expr* arg2 : *to_app(x)) { @@ -193,7 +215,7 @@ namespace euf { args.push_back(arg2); } term = a.mk_div(y, a.mk_mul(args)); - eqs.push_back(dependent_eq(to_app(arg), term, d)); + eqs.push_back(dependent_eq(orig, to_app(arg), term, d)); } } @@ -214,22 +236,24 @@ namespace euf { } } - void solve_eq(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { - solve_add(x, y, d, eqs); - solve_mod(x, y, d, eqs); - solve_mul(x, y, d, eqs); + void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + solve_add(orig, x, y, d, eqs); + solve_mod(orig, x, y, d, eqs); + solve_mul(orig, x, y, d, eqs); } public: + arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m) {} + void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { if (!m_enabled) return; auto [f, d] = e(); expr* x, * y; if (m.is_eq(f, x, y) && a.is_int_real(x)) { - solve_eq(x, y, d, eqs); - solve_eq(y, x, d, eqs); + solve_eq(f, x, y, d, eqs); + solve_eq(f, y, x, d, eqs); } } @@ -237,10 +261,8 @@ namespace euf { if (!m_enabled) return; m_nonzero.reset(); - for (unsigned i = 0; i < fmls.size(); ++i) { - auto [f, d] = fmls[i](); - add_pos(f); - } + for (unsigned i = 0; i < fmls.size(); ++i) + add_pos(fmls[i].fml()); } diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h index 00f96f59b..77b866613 100644 --- a/src/ast/simplifiers/extract_eqs.h +++ b/src/ast/simplifiers/extract_eqs.h @@ -18,6 +18,8 @@ Author: #pragma once + +#include "ast/ast_pp.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/rewriter/th_rewriter.h" #include "ast/expr_substitution.h" @@ -27,10 +29,11 @@ Author: namespace euf { struct dependent_eq { - app* var; - expr_ref term; + expr* orig; // original expression that encoded equation + app* var; // isolated variable + expr_ref term; // defined term expr_dependency* dep; - dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {} + dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {} }; typedef vector dep_eq_vector; @@ -41,8 +44,13 @@ namespace euf { virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0; virtual void pre_process(dependent_expr_state& fmls) {} virtual void updt_params(params_ref const& p) {} + virtual void set_allow_booleans(bool f) {} }; void register_extract_eqs(ast_manager& m, scoped_ptr_vector& ex); } + +inline std::ostream& operator<<(std::ostream& out, euf::dependent_eq const& eq) { + return out << mk_pp(eq.var, eq.term.m()) << " = " << eq.term << "\n"; +} diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 2e8eab0e6..3d7774cb4 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -21,24 +21,84 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector rp = mk_default_expr_replacer(m, false); + add_vars(d, free_vars); + + added.push_back(d); + + for (auto& t : m_trail) { + if (!t->m_active) + continue; + + // updates that have no intersections with current variables are skipped + if (!t->intersects(free_vars)) + continue; + + // loose entries that intersect with free vars are deleted from the trail + // and their removed formulas are added to the resulting constraints. + if (t->is_loose()) { + added.append(t->m_removed); + for (auto r : t->m_removed) + add_vars(r, free_vars); + m_trail_stack.push(value_trail(t->m_active)); + t->m_active = false; + continue; + } + + rp->set_substitution(t->m_subst.get()); + // rigid entries: + // apply substitution to added in case of rigid model convertions + for (auto& d : added) { + auto [f, dep1] = d(); + auto [g, dep2] = rp->replace_with_dep(f); + d = dependent_expr(m, g, m.mk_join(dep1, dep2)); + } + } } /** * retrieve the current model converter corresponding to chaining substitutions from the trail. */ model_converter_ref model_reconstruction_trail::get_model_converter() { - model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); + + + // // walk the trail from the back // add substitutions from the back to the generic model converter // after they have been normalized using a global replace that replaces // substituted variables by their terms. - NOT_IMPLEMENTED_YET(); - return mc; + // + + scoped_ptr rp = mk_default_expr_replacer(m, false); + expr_substitution subst(m, true, false); + rp->set_substitution(&subst); + generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); + bool first = true; + for (unsigned i = m_trail.size(); i-- > 0; ) { + auto* t = m_trail[i]; + if (!t->m_active) + continue; + + if (first) { + first = false; + for (auto const& [v, def] : t->m_subst->sub()) { + expr_dependency* dep = t->m_subst->dep(v); + subst.insert(v, def, dep); + mc->add(v, def); + } + continue; + } + + for (auto const& [v, def] : t->m_subst->sub()) { + auto [new_def, new_dep] = rp->replace_with_dep(def); + expr_dependency* dep = t->m_subst->dep(v); + new_dep = m.mk_join(dep, new_dep); + subst.insert(v, new_def, new_dep); + mc->add(v, new_def); + } + + } + return model_converter_ref(mc.get()); } diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index eeaf786d9..c9b42bc92 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -24,33 +24,64 @@ Author: #pragma once #include "util/scoped_ptr_vector.h" +#include "util/trail.h" +#include "ast/for_each_expr.h" #include "ast/rewriter/expr_replacer.h" #include "ast/simplifiers/dependent_expr.h" #include "ast/converters/model_converter.h" class model_reconstruction_trail { - ast_manager& m; + struct entry { + scoped_ptr m_subst; + vector m_removed; + bool m_active = true; + + entry(expr_substitution* s, vector const& rem) : + m_subst(s), m_removed(rem) {} + + bool is_loose() const { return !m_removed.empty(); } + + bool intersects(ast_mark const& free_vars) const { + for (auto const& [k, v] : m_subst->sub()) + if (free_vars.is_marked(k)) + return true; + return false; + } + - struct model_reconstruction_trail_entry { - scoped_ptr m_replace; - vector m_removed; - model_reconstruction_trail_entry(expr_replacer* r, vector const& rem) : - m_replace(r), m_removed(rem) {} }; - scoped_ptr_vector m_trail; - unsigned_vector m_limit; + ast_manager& m; + trail_stack& m_trail_stack; + scoped_ptr_vector m_trail; + + void add_vars(dependent_expr const& d, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager()))) + free_vars.mark(t, true); + } + + bool intersects(ast_mark const& free_vars, dependent_expr const& d) { + expr_ref term(d.fml(), d.get_manager()); + auto iter = subterms::all(term); + return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); }); + } + + bool intersects(ast_mark const& free_vars, vector const& added) { + return any_of(added, [&](dependent_expr const& d) { return intersects(free_vars, d); }); + } public: - model_reconstruction_trail(ast_manager& m) : m(m) {} + model_reconstruction_trail(ast_manager& m, trail_stack& tr): + m(m), m_trail_stack(tr) {} /** - * add a new substitution to the stack + * add a new substitution to the trail */ - void push(expr_replacer* r, vector const& removed) { - m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed)); + 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)); } /** @@ -63,18 +94,5 @@ public: * retrieve the current model converter corresponding to chaining substitutions from the trail. */ model_converter_ref get_model_converter(); - - /** - * push a context. Portions of the trail added within a context are removed after a context pop. - */ - void push() { - m_limit.push_back(m_trail.size()); - } - - void pop(unsigned n) { - unsigned old_sz = m_limit[m_limit.size() - n]; - m_trail.resize(old_sz); - m_limit.shrink(m_limit.size() - n); - } }; diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp new file mode 100644 index 000000000..37836db27 --- /dev/null +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -0,0 +1,239 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_context_eqs.cpp + +Abstract: + + simplifier for solving equations within a context + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +Notes: + +The variable v is solved based on expression e. +Check that every occurrence of v uses e in conjunctive context. + +Walk formulas containing v in as and-or. +Equalities that occur within at least one alternation of or are +considered as candidates. + +To constrain how formulas are traversed, first +label sub-expressions that contain v. An equality eq is safe for v +if every occurrence of v occurs in the same conjunctive context as eq. + +--*/ + +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/occurs.h" +#include "ast/simplifiers/solve_context_eqs.h" +#include "ast/simplifiers/solve_eqs.h" + +namespace euf { + + + solve_context_eqs::solve_context_eqs(solve_eqs& s): m(s.m), m_fmls(s.m_fmls), m_solve_eqs(s) {} + + bool solve_context_eqs::is_safe_eq(expr* e) { + m_and_pos.reset(); m_and_neg.reset(); m_or_pos.reset(); m_or_neg.reset(); + for (unsigned i = 0; i < m_fmls.size(); ++i) + if (!is_safe_eq(m_fmls[i].fml(), e)) + return false; + return true; + } + + /** + * Check if some conjunction of f contains equality 'e'. + * If this is not the case, then check that every conjunct that contains v + * recursively contains a disjunction that contains 'e'. + */ + bool solve_context_eqs::is_safe_eq(unsigned recursion_depth, expr* f, bool sign, expr* e) { + if (!contains_v(f)) + return true; + signed_expressions conjuncts; + if (contains_conjunctively(f, sign, e, conjuncts)) + return true; + if (recursion_depth > 3) + return false; + return all_of(conjuncts, [&](std::pair const& p) { return is_disjunctively_safe(recursion_depth, p.second, p.first, e); }); + } + + /* + * Every disjunction in f that contains v also contains the equation e. + */ + bool solve_context_eqs::is_disjunctively_safe(unsigned recursion_depth, expr* f0, bool sign, expr* e) { + signed_expressions todo; + todo.push_back({sign, f0}); + while (!todo.empty()) { + auto [s, f] = todo.back(); + todo.pop_back(); + if (s && m_or_neg.is_marked(f)) + continue; + if (!s && m_or_pos.is_marked(f)) + continue; + if (s) + m_or_neg.mark(f, true); + else + m_or_pos.mark(f, true); + if (!s && f == e) + continue; + else if (!contains_v(f)) + continue; + else if (s && m.is_and(f)) + for (auto* arg : *to_app(f)) + todo.push_back({s, arg}); + else if (!s && m.is_or(f)) + for (auto* arg : *to_app(f)) + todo.push_back({s, arg}); + else if (m.is_not(f, f)) + todo.push_back({!s, f}); + else if (!is_conjunction(s, f)) + return false; + else if (!is_safe_eq(recursion_depth + 1, f, s, e)) + return false; + } + return true; + } + + bool solve_context_eqs::is_conjunction(bool sign, expr* f) const { + if (!sign && m.is_and(f)) + return true; + if (sign && m.is_or(f)) + return true; + return false; + } + + /** + * Determine whether some conjunction in f contains e. + * If no conjunction contains e, then return the set of conjunctions that contain v. + */ + bool solve_context_eqs::contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts) { + signed_expressions todo; + todo.push_back({sign, f}); + while (!todo.empty()) { + auto [s, f] = todo.back(); + todo.pop_back(); + if (!s && f == e) + return true; + if (!s && m_and_pos.is_marked(f)) + continue; + if (s && m_and_neg.is_marked(f)) + continue; + if (s) + m_and_neg.mark(f, true); + else + m_and_pos.mark(f, true); + if (!contains_v(f)) + continue; + if (!s && m.is_and(f)) + for (auto* arg : *to_app(f)) + todo.push_back({false, arg}); + else if (s && m.is_or(f)) + for (auto* arg : *to_app(f)) + todo.push_back({true, arg}); + else if (m.is_not(f, f)) + todo.push_back({!s, f}); + else + conjuncts.push_back({s, f}); + } + return false; + } + + void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) { + expr_mark visited; + for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i) + collect_nested_equalities(m_fmls[i], visited, eqs); + + std::stable_sort(eqs.begin(), eqs.end(), [&](dependent_eq const& e1, dependent_eq const& e2) { + return e1.var->get_id() < e2.var->get_id(); }); + unsigned j = 0; + expr* last_var = nullptr; + for (auto const& eq : eqs) { + + SASSERT(!m.is_bool(eq.var)); + + if (eq.var != last_var) { + + m_contains_v.reset(); + + // first check if v is in term. If it is, then the substitution candidate is unsafe + m_todo.push_back(eq.term); + mark_occurs(m_todo, eq.var, m_contains_v); + SASSERT(m_todo.empty()); + last_var = eq.var; + if (m_contains_v.is_marked(eq.term)) + continue; + + // then mark occurrences + for (unsigned i = 0; i < m_fmls.size(); ++i) + m_todo.push_back(m_fmls[i].fml()); + mark_occurs(m_todo, eq.var, m_contains_v); + SASSERT(m_todo.empty()); + } + else if (m_contains_v.is_marked(eq.term)) + continue; + + // subject to occurrences, check if equality is safe + if (is_safe_eq(eq.orig)) + eqs[j++] = eq; + } + eqs.shrink(j); + TRACE("solve_eqs", + for (auto const& eq : eqs) + tout << eq << "\n"); + } + + void solve_context_eqs::collect_nested_equalities(dependent_expr const& df, expr_mark& visited, dep_eq_vector& eqs) { + + svector> todo; + todo.push_back({ false, 0, df.fml()}); + + // even depth is conjunctive context, odd is disjunctive + // when alternating between conjunctive and disjunctive context, increment depth. + auto inc_or = [](unsigned depth) { + return (0 == depth % 2) ? depth + 1 : depth; + }; + auto inc_and = [](unsigned depth) { + return (0 == depth % 2) ? depth : depth + 1; + }; + + while (!todo.empty()) { + auto [s, depth, f] = todo.back(); + todo.pop_back(); + if (visited.is_marked(f)) + continue; + visited.mark(f, true); + if (s && m.is_and(f)) { + for (auto* arg : *to_app(f)) + todo.push_back({ s, inc_or(depth), arg }); + } + else if (!s && m.is_or(f)) { + for (auto* arg : *to_app(f)) + todo.push_back({ s, inc_or(depth), arg }); + } + if (!s && m.is_and(f)) { + for (auto* arg : *to_app(f)) + todo.push_back({ s, inc_and(depth), arg }); + } + else if (s && m.is_or(f)) { + for (auto* arg : *to_app(f)) + todo.push_back({ s, inc_and(depth), arg }); + } + else if (m.is_not(f, f)) + todo.push_back({ !s, depth, f }); + else if (!s && 1 == depth % 2) { + for (extract_eq* ex : m_solve_eqs.m_extract_plugins) { + ex->set_allow_booleans(false); + ex->get_eqs(dependent_expr(m, f, df.dep()), eqs); + ex->set_allow_booleans(true); + } + } + } + } +} diff --git a/src/ast/simplifiers/solve_context_eqs.h b/src/ast/simplifiers/solve_context_eqs.h new file mode 100644 index 000000000..8332d3a73 --- /dev/null +++ b/src/ast/simplifiers/solve_context_eqs.h @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_context_eqs.h + +Abstract: + + simplifier for solving equations within a context + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/simplifiers/extract_eqs.h" + +namespace euf { + + class solve_eqs; + + + class solve_context_eqs { + + ast_manager& m; + dependent_expr_state& m_fmls; + solve_eqs& m_solve_eqs; + expr_mark m_and_pos, m_and_neg, m_or_pos, m_or_neg; + expr_mark m_contains_v; + ptr_vector m_todo; + + typedef svector> signed_expressions; + + bool contains_v(expr* f) const { return m_contains_v.is_marked(f); } + bool is_safe_eq(expr* e); + bool is_safe_eq(unsigned recursion_depth, expr* f, bool sign, expr* e); + bool is_safe_eq(expr* f, expr* e) { return is_safe_eq(0, f, false, e); } + bool is_disjunctively_safe(unsigned recursion_depth, expr* f, bool sign, expr* e); + bool contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts); + bool is_conjunction(bool sign, expr* f) const; + + void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs); + + public: + + solve_context_eqs(solve_eqs& s); + + void collect_nested_equalities(dep_eq_vector& eqs); + + }; +} diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 6b2a27d2d..e6ee36410 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -20,25 +20,35 @@ Author: #include "ast/ast_util.h" #include "ast/for_each_expr.h" #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/occurs.h" #include "ast/recfun_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" #include "ast/simplifiers/solve_eqs.h" +#include "ast/simplifiers/solve_context_eqs.h" #include "ast/converters/generic_model_converter.h" #include "params/tactic_params.hpp" namespace euf { + + void solve_eqs::get_eqs(dep_eq_vector& eqs) { + for (extract_eq* ex : m_extract_plugins) + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + ex->get_eqs(m_fmls[i], eqs); + } + // initialize graph that maps variable ids to next ids void solve_eqs::extract_dep_graph(dep_eq_vector& eqs) { m_var2id.reset(); m_id2var.reset(); m_next.reset(); unsigned sz = 0; - for (auto const& [v, t, d] : eqs) + for (auto const& [orig, v, t, d] : eqs) sz = std::max(sz, v->get_id()); m_var2id.resize(sz + 1, UINT_MAX); - for (auto const& [v, t, d] : eqs) { + for (auto const& [orig, v, t, d] : eqs) { if (is_var(v) || !can_be_var(v)) continue; m_var2id[v->get_id()] = m_id2var.size(); @@ -60,16 +70,17 @@ namespace euf { m_id2level.reset(); m_id2level.resize(m_id2var.size(), UINT_MAX); m_subst_ids.reset(); - m_subst = alloc(expr_substitution, m, false, false); + + m_subst = alloc(expr_substitution, m, true, false); auto is_explored = [&](unsigned id) { return m_id2level[id] != UINT_MAX; }; auto is_safe = [&](unsigned lvl, expr* t) { - for (auto* e : subterms::all(expr_ref(t, m))) + for (auto* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited)) if (is_var(e) && m_id2level[var2id(e)] < lvl) - return false; + return false; return true; }; @@ -89,14 +100,17 @@ namespace euf { todo.pop_back(); if (is_explored(j)) continue; - m_id2level[id] = curr_level++; + + m_id2level[j] = curr_level++; for (auto const& eq : m_next[j]) { - auto const& [v, t, d] = eq; + auto const& [orig, v, t, d] = eq; + SASSERT(j == var2id(v)); if (!is_safe(curr_level, t)) continue; + SASSERT(!occurs(v, t)); m_next[j][0] = eq; - m_subst_ids.push_back(id); - for (expr* e : subterms::all(expr_ref(t, m))) + m_subst_ids.push_back(j); + for (expr* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited)) if (is_var(e) && !is_explored(var2id(e))) todo.push_back(var2id(e)); break; @@ -105,31 +119,25 @@ namespace euf { } } - void solve_eqs::add_subst(dependent_eq const& eq) { - SASSERT(can_be_var(eq.var)); - m_subst->insert(eq.var, eq.term, nullptr, eq.dep); - ++m_stats.m_num_elim_vars; - } - void solve_eqs::normalize() { - scoped_ptr rp = mk_default_expr_replacer(m, true); - m_subst->reset(); + if (m_subst_ids.empty()) + return; + scoped_ptr rp = mk_default_expr_replacer(m, false); rp->set_substitution(m_subst.get()); std::sort(m_subst_ids.begin(), m_subst_ids.end(), [&](unsigned u, unsigned v) { return m_id2level[u] > m_id2level[v]; }); - expr_dependency_ref new_dep(m); - expr_ref new_def(m); - proof_ref new_pr(m); - for (unsigned id : m_subst_ids) { if (!m.inc()) - break; - auto const& [v, def, dep] = m_next[id][0]; - rp->operator()(def, new_def, new_pr, new_dep); + return; + auto const& [orig, v, def, dep] = m_next[id][0]; + auto [new_def, new_dep] = rp->replace_with_dep(def); m_stats.m_num_steps += rp->get_num_steps() + 1; + ++m_stats.m_num_elim_vars; new_dep = m.mk_join(dep, new_dep); - m_subst->insert(v, new_def, new_pr, new_dep); + IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(v, m) << " -> " << mk_bounded_pp(new_def, m) << "\n"); + m_subst->insert(v, new_def, new_dep); + SASSERT(can_be_var(v)); // we updated the substitution, but we don't need to reset rp // because all cached values there do not depend on v. } @@ -141,22 +149,27 @@ namespace euf { expr* def = m_subst->find(eq.var); tout << mk_pp(eq.var, m) << "\n----->\n" << mk_pp(def, m) << "\n\n"; }); + + } - void solve_eqs::apply_subst() { + void solve_eqs::apply_subst(vector& old_fmls) { if (!m.inc()) return; - scoped_ptr rp = mk_default_expr_replacer(m, true); + if (m_subst_ids.empty()) + return; + + scoped_ptr rp = mk_default_expr_replacer(m, false); rp->set_substitution(m_subst.get()); - expr_ref new_f(m); - proof_ref new_pr(m); - expr_dependency_ref new_dep(m); + for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { auto [f, d] = m_fmls[i](); - rp->operator()(f, new_f, new_pr, new_dep); + auto [new_f, new_dep] = rp->replace_with_dep(f); + m_rewriter(new_f); if (new_f == f) continue; new_dep = m.mk_join(d, new_dep); + old_fmls.push_back(m_fmls[i]); m_fmls.update(i, dependent_expr(m, new_f, new_dep)); } } @@ -166,37 +179,60 @@ namespace euf { for (extract_eq* ex : m_extract_plugins) ex->pre_process(m_fmls); - // TODO add a loop. + + unsigned count = 0; + vector old_fmls; dep_eq_vector eqs; - get_eqs(eqs); - extract_dep_graph(eqs); - extract_subst(); - apply_subst(); + do { + old_fmls.reset(); + m_subst_ids.reset(); + eqs.reset(); + get_eqs(eqs); + extract_dep_graph(eqs); + extract_subst(); + normalize(); + apply_subst(old_fmls); + ++count; + save_subst({}); + } + while (!m_subst_ids.empty() && count < 20 && m.inc()); + + if (!m.inc()) + return; + + if (m_config.m_context_solve) { + old_fmls.reset(); + m_subst_ids.reset(); + eqs.reset(); + solve_context_eqs context_solve(*this); + context_solve.collect_nested_equalities(eqs); + extract_dep_graph(eqs); + extract_subst(); + normalize(); + apply_subst(old_fmls); + save_subst(old_fmls); + } + advance_qhead(m_fmls.size()); } + void solve_eqs::save_subst(vector const& old_fmls) { + if (!m_subst->empty()) + m_fmls.model_trail().push(m_subst.detach(), old_fmls); + } + void solve_eqs::filter_unsafe_vars() { m_unsafe_vars.reset(); recfun::util rec(m); for (func_decl* f : rec.get_rec_funs()) - for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m))) + for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m), &m_todo, &m_visited)) m_unsafe_vars.mark(term); } - typedef generic_model_converter gmc; - - model_converter_ref solve_eqs::get_model_converter() { - model_converter_ref mc = alloc(gmc, m, "solve-eqs"); - for (unsigned id : m_subst_ids) { - auto* v = m_id2var[id]; - static_cast(mc.get())->add(v, m_subst->find(v)); - } - return mc; - } - solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_rewriter(m) { register_extract_eqs(m, m_extract_plugins); + m_rewriter.set_flat_and_or(false); } void solve_eqs::updt_params(params_ref const& p) { diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h index 49cd90ca2..c3cacbec9 100644 --- a/src/ast/simplifiers/solve_eqs.h +++ b/src/ast/simplifiers/solve_eqs.h @@ -26,6 +26,9 @@ Author: namespace euf { class solve_eqs : public dependent_expr_simplifier { + + friend class solve_context_eqs; + struct stats { unsigned m_num_steps = 0; unsigned m_num_elim_vars = 0; @@ -35,50 +38,43 @@ namespace euf { unsigned m_max_occs = UINT_MAX; }; - th_rewriter m_rewriter; - scoped_ptr_vector m_extract_plugins; - unsigned_vector m_var2id, m_id2level, m_subst_ids; - ptr_vector m_id2var; - vector m_next; - scoped_ptr m_subst; - expr_mark m_unsafe_vars; // expressions that cannot be replaced stats m_stats; config m_config; - - void add_subst(dependent_eq const& eq); + th_rewriter m_rewriter; + scoped_ptr_vector m_extract_plugins; + unsigned_vector m_var2id; // app->get_id() |-> small numeral + ptr_vector m_id2var; // small numeral |-> app + unsigned_vector m_id2level; // small numeral |-> level in substitution ordering + unsigned_vector m_subst_ids; // sorted list of small numeral by level + vector m_next; // adjacency list for solved equations + scoped_ptr m_subst; // current substitution + expr_mark m_unsafe_vars; // expressions that cannot be replaced + ptr_vector m_todo; + expr_mark m_visited; bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; } unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; } - - void get_eqs(dep_eq_vector& eqs) { - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) - get_eqs(m_fmls[i], eqs); - } - - void get_eqs(dependent_expr const& f, dep_eq_vector& eqs) { - for (extract_eq* ex : m_extract_plugins) - ex->get_eqs(f, eqs); - } - - void filter_unsafe_vars(); bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); } + void get_eqs(dep_eq_vector& eqs); + void filter_unsafe_vars(); void extract_subst(); void extract_dep_graph(dep_eq_vector& eqs); void normalize(); - void apply_subst(); + void apply_subst(vector& old_fmls); + void save_subst(vector const& old_fmls); + public: solve_eqs(ast_manager& m, dependent_expr_state& fmls); - void push() override { dependent_expr_simplifier::push(); } - void pop(unsigned n) override { dependent_expr_simplifier::pop(n); } + void reduce() override; void updt_params(params_ref const& p) override; + void collect_statistics(statistics& st) const override; - model_converter_ref get_model_converter() override; }; } diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 030d88d71..d748dca63 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -286,9 +286,8 @@ public: dtoken read_num() { - while(isdigit(m_curr_char)) { + while (isdigit(m_curr_char)) save_and_next(); - } return TK_NUM; } @@ -781,15 +780,29 @@ protected: symbol td1(td); expr_ref v1(m), v2(m); sort* s = nullptr; - dtoken tok2 = m_lexer->next_token(); - if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) { - return unexpected(tok2, "built-in infix operator"); + uint64_t num1(0), num3(0); + if (tok1 == TK_NUM) { + char const* data = m_lexer->get_token_data(); + rational num(data); + if (!num.is_uint64()) + return unexpected(tok1, "integer expected"); + num1 = num.get_uint64(); } + dtoken tok2 = m_lexer->next_token(); + if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) + return unexpected(tok2, "built-in infix operator"); dtoken tok3 = m_lexer->next_token(); td = m_lexer->get_token_data(); - if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td))) { + if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td))) return unexpected(tok3, "identifier"); + if (tok3 == TK_NUM) { + char const* data = m_lexer->get_token_data(); + rational num(data); + if (!num.is_uint64()) + return unexpected(tok1, "integer expected"); + num3 = num.get_uint64(); } + symbol td2(td); if (tok1 == TK_ID) { @@ -805,18 +818,21 @@ protected: if (!v1 && !v2) { return unexpected(tok3, "at least one argument should be a variable"); } - if (v1) { + if (v1) s = v1->get_sort(); - } - else { + else s = v2->get_sort(); - } - if (!v1) { + + if (tok1 == TK_NUM) + v1 = mk_symbol_const(num1, s); + + if (tok3 == TK_NUM) + v2 = mk_symbol_const(num3, s); + + if (!v1) v1 = mk_const(td1, s); - } - if (!v2) { + if (!v2) v2 = mk_const(td2, s); - } switch(tok2) { case TK_EQ: @@ -1126,8 +1142,11 @@ protected: if (m_arith.is_int(s)) return m_arith.mk_numeral(rational(el, rational::ui64()), s); else if (m_decl_util.try_get_size(s, sz)) { - if (el >= sz) - throw default_exception("numeric value out of bounds of domain"); + if (el >= sz) { + std::ostringstream ous; + ous << "numeric value " << el << " is out of bounds of domain size " << sz; + throw default_exception(ous.str()); + } return m_decl_util.mk_numeral(el, s); } else { diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 4f7342590..b8b51c0c6 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -244,12 +244,10 @@ namespace spacer { } void iuc_solver::elim_proxies (expr_ref_vector &v) { - expr_ref f = mk_and (v); scoped_ptr rep = mk_expr_simp_replacer (m); rep->set_substitution (&m_elim_proxies_sub); - (*rep)(f); - v.reset(); - flatten_and(f, v); + (*rep)(v); + flatten_and(v); } void iuc_solver::get_iuc(expr_ref_vector &core) { diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp index fc812c4f5..e41347c2b 100644 --- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp +++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_term_ite_tactic.h" tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5895643bd..66a391cb8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -31,6 +31,7 @@ Notes: #include "tactic/tactic.h" #include "tactic/arith/lia2card_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" diff --git a/src/params/bool_rewriter_params.pyg b/src/params/bool_rewriter_params.pyg index 85583cbca..c8d7ddbb7 100644 --- a/src/params/bool_rewriter_params.pyg +++ b/src/params/bool_rewriter_params.pyg @@ -1,8 +1,9 @@ def_module_params(module_name='rewriter', class_name='bool_rewriter_params', export=True, - params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), - ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), + params=(("ite_extra_rules", BOOL, True, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), + ("flat", BOOL, True, "create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor"), + ("flat_and_or", BOOL, True, "create nary applications for and,or"), ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), ('elim_ite', BOOL, True, "eliminate ite in favor of and/or"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 512ec8424..646299567 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -46,7 +46,7 @@ namespace sat { else if (s == symbol("static")) m_restart = RS_STATIC; else - throw sat_param_exception("invalid restart strategy"); + throw sat_param_exception("invalid restart strategy. Use ema (default), luby, geometric, static"); m_fast_glue_avg = p.restart_emafastglue(); m_slow_glue_avg = p.restart_emaslowglue(); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e29a7bcc2..e9aeaddbb 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -353,10 +353,8 @@ namespace sat { void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); } bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); } bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); } - unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); } void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); } void mark_visited(bool_var v) { mark_visited(literal(v, false)); } - void inc_visited(bool_var v) { m_visited.inc_visited(v); } bool all_distinct(literal_vector const& lits); bool all_distinct(clause const& cl); diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index a2bc381e4..ad3d3818c 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -147,18 +147,22 @@ namespace smt { for (auto& info : m_trail) { expr_ref fact = mk_or(info.m_clause); proof* pr = info.m_proof; + expr* args[2] = { pr, fact }; + unsigned num_args = 2, offset = 0; + if (!pr) + offset = 1; switch (info.m_status) { case status::assumption: - ps.push_back(m.mk_assumption_add(pr, fact)); + ps.push_back(m.mk_app(symbol("assumption"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::lemma: - ps.push_back(m.mk_lemma_add(pr, fact)); + ps.push_back(m.mk_app(symbol("lemma"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::th_assumption: - ps.push_back(m.mk_th_assumption_add(pr, fact)); + ps.push_back(m.mk_app(symbol("th-assumption"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::th_lemma: - ps.push_back(m.mk_th_lemma_add(pr, fact)); + ps.push_back(m.mk_app(symbol("th-lemma"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::deleted: ps.push_back(m.mk_redundant_del(fact)); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 2483b2ca4..63848418f 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1593,6 +1593,18 @@ namespace smt { TRACE("gate_clause", tout << mk_ll_pp(pr, m);); mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); } + else if (m_clause_proof.on_clause_active()) { + ptr_buffer new_lits; + for (unsigned i = 0; i < num_lits; i++) { + literal l = lits[i]; + bool_var v = l.var(); + expr * atom = m_bool_var2expr[v]; + new_lits.push_back(l.sign() ? m.mk_not(atom) : atom); + } + // expr* fact = m.mk_or(new_lits); + proof* pr = m.mk_app(symbol("tseitin"), new_lits.size(), new_lits.data(), m.mk_proof_sort()); + mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); + } else { mk_clause(num_lits, lits, nullptr); } diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 416275275..515a51a17 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -102,9 +102,8 @@ namespace smt { void theory_recfun::relevant_eh(app * n) { SASSERT(ctx.relevancy()); // TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); - if (u().is_defined(n) && u().has_defs()) { + if (u().is_defined(n) && u().has_defs()) push_case_expand(n); - } } void theory_recfun::push_scope_eh() { @@ -418,7 +417,7 @@ namespace smt { } void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { - if (u().has_defs() || !m_disabled_guards.empty()) { + if (u().has_rec_defs() || !m_disabled_guards.empty()) { app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); TRACEFN("add_theory_assumption " << dlimit); assumptions.push_back(dlimit); diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 90c84e7ee..2b20ebd80 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -306,7 +306,7 @@ void asserted_formulas::reduce() { if (!invoke(m_flatten_clauses)) return; // if (!invoke(m_propagate_values)) return; - IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done :num-exprs " << get_total_size() << ")\n";); TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); TRACE("macros", m_macro_manager.display(tout);); @@ -327,8 +327,8 @@ unsigned asserted_formulas::get_formulas_last_level() const { bool asserted_formulas::invoke(simplify_fmls& s) { if (!s.should_apply()) return true; - IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";); s(); + IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << " :num-exprs " << get_total_size() << ")\n";); IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); CASSERT("well_sorted",check_well_sorted()); @@ -514,9 +514,9 @@ void asserted_formulas::simplify_fmls::operator()() { void asserted_formulas::reduce_and_solve() { - IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";); flush_cache(); // collect garbage m_reduce_asserted_formulas(); + IF_VERBOSE(10, verbose_stream() << "(smt.reduced " << get_total_size() << ")\n";); } diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index e57510d4f..38d2699f0 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -49,6 +49,7 @@ z3_add_component(core_tactics reduce_invertible_tactic.h simplify_tactic.h solve_eqs_tactic.h + solve_eqs2_tactic.h special_relations_tactic.h split_clause_tactic.h symmetry_reduce_tactic.h diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h index 91b3875ae..c1edc43b1 100644 --- a/src/tactic/core/solve_eqs2_tactic.h +++ b/src/tactic/core/solve_eqs2_tactic.h @@ -29,10 +29,15 @@ public: } }; -inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs2"); +inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs"); } +#if 1 +inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return mk_solve_eqs2_tactic(m, p); +} +#endif /* ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)") diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 3e338b57e..be5db427b 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -425,6 +425,7 @@ class solve_eqs_tactic : public tactic { else pr = m().mk_modus_ponens(g.pr(idx), pr); } + IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(var, m()) << " -> " << mk_bounded_pp(def, m()) << "\n"); m_subst->insert(var, def, pr, g.dep(idx)); } @@ -479,52 +480,11 @@ class solve_eqs_tactic : public tactic { ptr_vector m_todo; void mark_occurs(expr_mark& occ, goal const& g, expr* v) { - expr_fast_mark2 visited; - occ.mark(v, true); - visited.mark(v, true); - for (unsigned j = 0; j < g.size(); ++j) { - m_todo.push_back(g.form(j)); - } - while (!m_todo.empty()) { - expr* e = m_todo.back(); - if (visited.is_marked(e)) { - m_todo.pop_back(); - continue; - } - if (is_app(e)) { - bool does_occur = false; - bool all_visited = true; - for (expr* arg : *to_app(e)) { - if (!visited.is_marked(arg)) { - m_todo.push_back(arg); - all_visited = false; - } - else { - does_occur |= occ.is_marked(arg); - } - } - if (all_visited) { - occ.mark(e, does_occur); - visited.mark(e, true); - m_todo.pop_back(); - } - } - else if (is_quantifier(e)) { - expr* body = to_quantifier(e)->get_expr(); - if (visited.is_marked(body)) { - visited.mark(e, true); - occ.mark(e, occ.is_marked(body)); - m_todo.pop_back(); - } - else { - m_todo.push_back(body); - } - } - else { - visited.mark(e, true); - m_todo.pop_back(); - } - } + SASSERT(m_todo.empty()); + for (unsigned j = 0; j < g.size(); ++j) + m_todo.push_back(g.form(j)); + ::mark_occurs(m_todo, v, occ); + SASSERT(m_todo.empty()); } expr_mark m_compatible_tried; @@ -661,9 +621,11 @@ class solve_eqs_tactic : public tactic { expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr; if (m().is_eq(arg, lhs, rhs) && !m().is_bool(lhs)) { if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) { + IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n"); insert_solution(g, idx, arg, var, def, pr); } else if (trivial_solve1(rhs, lhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) { + IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n"); insert_solution(g, idx, arg, var, def, pr); } else { @@ -1022,6 +984,10 @@ class solve_eqs_tactic : public tactic { unsigned get_num_eliminated_vars() const { return m_num_eliminated_vars; } + + void collect_statistics(statistics& st) { + st.update("solve eqs elim vars", get_num_eliminated_vars()); + } // // TBD: rewrite the tactic to first apply a topological sorting that @@ -1031,6 +997,8 @@ class solve_eqs_tactic : public tactic { // void operator()(goal_ref const & g, goal_ref_buffer & result) { model_converter_ref mc; + std::function coll = [&](statistics& st) { collect_statistics(st); }; + statistics_report sreport(coll); tactic_report report("solve_eqs", *g); TRACE("goal", g->display(tout);); m_produce_models = g->models_enabled(); @@ -1074,6 +1042,8 @@ class solve_eqs_tactic : public tactic { g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); + + } }; @@ -1107,7 +1077,6 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { (*m_imp)(in, result); - report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars()); } void cleanup() override { @@ -1126,7 +1095,7 @@ public: } void collect_statistics(statistics & st) const override { - st.update("eliminated vars", m_imp->get_num_eliminated_vars()); + m_imp->collect_statistics(st); } void reset_statistics() override { @@ -1135,6 +1104,7 @@ public: }; -tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p) { + +tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true)); } diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index d65a33046..2da8f181f 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -22,10 +22,17 @@ Revision History: class ast_manager; class tactic; -tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()); + +tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref()); + +#if 0 +inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return mk_solve_eqs1_tactic(m, p); +} +#endif /* - ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs_tactic(m, p)") + ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)") */ diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index ae3635c77..90862f1a7 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -22,14 +22,21 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { ast_manager& m; params_ref m_params; std::string m_name; - ref m_factory; - scoped_ptr m_simp; + trail_stack m_trail; goal_ref m_goal; dependent_expr m_dep; + statistics m_st; + ref m_factory; + scoped_ptr m_simp; + scoped_ptr m_model_trail; void init() { - if (!m_simp) + if (!m_simp) { m_simp = m_factory->mk(m, m_params, *this); + m_st.reset(); + } + if (!m_model_trail) + m_model_trail = alloc(model_reconstruction_trail, m, m_trail); } public: @@ -39,7 +46,7 @@ public: m_params(p), m_name(name), m_factory(f), - m_simp(f->mk(m, p, *this)), + m_simp(nullptr), m_dep(m, m.mk_true(), nullptr) {} @@ -60,6 +67,10 @@ public: bool inconsistent() override { return m_goal->inconsistent(); } + + model_reconstruction_trail& model_trail() override { + return *m_model_trail; + } char const* name() const override { return m_name.c_str(); } @@ -75,29 +86,39 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { - if (in->proofs_enabled()) - throw tactic_exception("tactic does not support low level proofs"); + init(); + statistics_report sreport(*this); tactic_report report(name(), *in); m_goal = in.get(); - m_simp->reduce(); + if (!in->proofs_enabled()) + m_simp->reduce(); + m_goal->elim_true(); m_goal->inc_depth(); if (in->models_enabled()) - in->set(m_simp->get_model_converter().get()); - result.push_back(in.get()); + in->add(m_model_trail->get_model_converter().get()); + result.push_back(in.get()); + cleanup(); } void cleanup() override { + if (m_simp) + m_simp->collect_statistics(m_st); + m_simp = nullptr; + m_model_trail = nullptr; } void collect_statistics(statistics & st) const override { - if (m_simp) + if (m_simp) m_simp->collect_statistics(st); + else + st.copy(m_st); } void reset_statistics() override { if (m_simp) m_simp->reset_statistics(); + m_st.reset(); } }; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index e631c23e9..a09da60a9 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "ast/normal_forms/nnf.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/bv/bv_size_reduction_tactic.h" #include "tactic/bv/max_bv_sharing_tactic.h" #include "tactic/core/simplify_tactic.h" diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index acad15fd6..6d44addf0 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/bv/bit_blaster_tactic.h" diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp index 2f1879d58..9ca6b70ef 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.cpp +++ b/src/tactic/smtlogics/qfauflia_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/core/propagate_values_tactic.h" #include "tactic/arith/propagate_ineqs_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/smtlogics/smt_tactic.h" diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 1366b701e..90df4fe42 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/bv/bv1_blaster_tactic.h" @@ -39,6 +40,9 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { // conservative gaussian elimination. solve_eq_p.set_uint("solve_eqs_max_occs", 2); + params_ref flat_and_or_p = p; + flat_and_or_p.set_bool("flat_and_or", false); + params_ref simp2_p = p; simp2_p.set_bool("som", true); simp2_p.set_bool("pull_cheap_ite", true); @@ -47,15 +51,17 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { simp2_p.set_uint("local_ctx_limit", 10000000); simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som + simp2_p.set_bool("flat_and_or", false); params_ref hoist_p; hoist_p.set_bool("hoist_mul", true); hoist_p.set_bool("som", false); + hoist_p.set_bool("flat_and_or", false); return and_then( - mk_simplify_tactic(m), - mk_propagate_values_tactic(m), + using_params(mk_simplify_tactic(m), flat_and_or_p), + using_params(mk_propagate_values_tactic(m), flat_and_or_p), using_params(mk_solve_eqs_tactic(m), solve_eq_p), mk_elim_uncnstr_tactic(m), if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), @@ -87,6 +93,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); local_ctx_p.set_bool("flat", false); + local_ctx_p.set_bool("flat_and_or", false); params_ref solver_p; solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp index c86789ed0..5c1ba5f44 100644 --- a/src/tactic/smtlogics/qfidl_tactic.cpp +++ b/src/tactic/smtlogics/qfidl_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/core/propagate_values_tactic.h" #include "tactic/arith/propagate_ineqs_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/arith/normalize_bounds_tactic.h" #include "tactic/arith/fix_dl_var_tactic.h" diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index b8ebbd8a9..d116414ea 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -22,6 +22,7 @@ Notes: #include "tactic/arith/propagate_ineqs_tactic.h" #include "tactic/arith/normalize_bounds_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/arith/add_bounds_tactic.h" #include "tactic/arith/pb2bv_tactic.h" diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index 609107a48..d9f723d67 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/core/simplify_tactic.h" #include "tactic/core/symmetry_reduce_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/smtlogics/smt_tactic.h" diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index d93a17ce1..98e09b56a 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/bv/max_bv_sharing_tactic.h" #include "tactic/bv/bv_size_reduction_tactic.h" @@ -136,22 +137,23 @@ private: }; static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { - params_ref simp2_p = p; + params_ref simp2_p = p, flat_and_or_p = p; + flat_and_or_p.set_bool("flat_and_or", false); simp2_p.set_bool("pull_cheap_ite", true); simp2_p.set_bool("push_ite_bv", false); simp2_p.set_bool("local_ctx", true); simp2_p.set_uint("local_ctx_limit", 10000000); - simp2_p.set_bool("ite_extra_rules", true); simp2_p.set_bool("mul2concat", true); + simp2_p.set_bool("flat_and_or", false); params_ref ctx_simp_p; ctx_simp_p.set_uint("max_depth", 32); ctx_simp_p.set_uint("max_steps", 5000000); return and_then( - mk_simplify_tactic(m), - mk_propagate_values_tactic(m), + using_params(mk_simplify_tactic(m), flat_and_or_p), + using_params(mk_propagate_values_tactic(m), flat_and_or_p), if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))), //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p), mk_solve_eqs_tactic(m), @@ -163,8 +165,10 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { } static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { - return and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), + params_ref simp2_p = p, flat_and_or_p = p; + flat_and_or_p.set_bool("flat_and_or", false); + return and_then(using_params(mk_simplify_tactic(m), flat_and_or_p), + using_params(mk_propagate_values_tactic(m), flat_and_or_p), mk_solve_eqs_tactic(m), mk_elim_uncnstr_tactic(m), if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index daf020a14..3bf6b658d 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -20,6 +20,7 @@ Revision History: #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "qe/lite/qe_lite.h" #include "qe/qsat.h" diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index b1609ed85..8bf6efac5 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -75,6 +75,18 @@ void report_tactic_progress(char const * id, unsigned val) { } } +statistics_report::~statistics_report() { + statistics st; + if (m_tactic) + m_tactic->collect_statistics(st); + else if (m_collector) + m_collector(st); + if (st.size() == 0) + return; + IF_VERBOSE(TACTIC_VERBOSITY_LVL, st.display_smt2(verbose_stream())); +} + + void skip_tactic::operator()(goal_ref const & in, goal_ref_buffer& result) { result.push_back(in.get()); } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 0f55ea0fe..c43120943 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -115,6 +115,15 @@ public: void report_tactic_progress(char const * id, unsigned val); +class statistics_report { + tactic* m_tactic = nullptr; + std::function m_collector; +public: + statistics_report(tactic& t):m_tactic(&t) {} + statistics_report(std::function& coll): m_collector(coll) {} + ~statistics_report(); +}; + class skip_tactic : public tactic { public: void operator()(goal_ref const & in, goal_ref_buffer& result) override; diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index e8495c013..728e6397d 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" +#include "tactic/core/solve_eqs2_tactic.h" #include "tactic/core/distribute_forall_tactic.h" #include "tactic/core/der_tactic.h" #include "tactic/core/reduce_args_tactic.h" diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index befd0b8e9..fb8042dc7 100644 --- a/src/test/hashtable.cpp +++ b/src/test/hashtable.cpp @@ -26,8 +26,8 @@ Revision History: struct int_hash_proc { unsigned operator()(int x) const { return x * 3; } }; typedef int_hashtable > int_set; -typedef std::unordered_set > > safe_int_set; // typedef safe_int_set int_set; +typedef std::unordered_set safe_int_set; inline bool contains(int_set & h, int i) { // return h.find(i) != h.end(); diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 0cbe9e9f8..bc9017726 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -34,8 +34,8 @@ int mpn_manager::compare(mpn_digit const * a, unsigned lnga, trace(a, lnga); - unsigned j = max(lnga, lngb) - 1; - for (; j != -1u && res == 0; j--) { + unsigned j = max(lnga, lngb); + for (; j-- > 0 && res == 0;) { mpn_digit const & u_j = (j < lnga) ? a[j] : zero; mpn_digit const & v_j = (j < lngb) ? b[j] : zero; if (u_j > v_j) @@ -310,7 +310,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, mpn_double_digit q_hat, temp, r_hat; mpn_digit borrow; - for (unsigned j = m-1; j != -1u; j--) { + for (unsigned j = m; j-- > 0; ) { temp = (((mpn_double_digit)numer[j+n]) << DIGIT_BITS) | ((mpn_double_digit)numer[j+n-1]); q_hat = temp / (mpn_double_digit) denom[n-1]; r_hat = temp % (mpn_double_digit) denom[n-1]; @@ -388,7 +388,7 @@ char * mpn_manager::to_string(mpn_digit const * a, unsigned lng, char * buf, uns void mpn_manager::display_raw(std::ostream & out, mpn_digit const * a, unsigned lng) const { out << "["; - for (unsigned i = lng-1; i != -1u; i-- ) { out << a[i]; if (i != 0) out << "|"; } + for (unsigned i = lng; i-- > 0; ) { out << a[i]; if (i != 0) out << "|"; } out << "]"; } diff --git a/src/util/util.h b/src/util/util.h index ffd94629c..f15566258 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -25,6 +25,7 @@ Revision History: #include #include #include +#include #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -180,9 +181,8 @@ void display(std::ostream & out, const IT & begin, const IT & end, const char * template struct delete_proc { void operator()(T * ptr) { - if (ptr) { - dealloc(ptr); - } + if (ptr) + dealloc(ptr); } }; @@ -361,6 +361,22 @@ void fatal_error(int error_code); void set_fatal_error_handler(void (*pfn)(int error_code)); +template +bool any_of(S& set, T const& p) { + for (auto const& s : set) + if (p(s)) + return true; + return false; +} + +template +bool all_of(S& set, T const& p) { + for (auto const& s : set) + if (!p(s)) + return false; + return true; +} + /** \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]). it contains the current value. diff --git a/src/util/visit_helper.h b/src/util/visit_helper.h index 418e2715c..a11d7bdc6 100644 --- a/src/util/visit_helper.h +++ b/src/util/visit_helper.h @@ -45,5 +45,5 @@ public: m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1); } bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; } - unsigned num_visited(unsigned v) const { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; } + unsigned num_visited(unsigned v) { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; } }; \ No newline at end of file