From 25b0b1430c40d24f151756f84198b61d3091e272 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Jan 2023 12:42:20 -0800 Subject: [PATCH] move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532 --- src/ast/rewriter/arith_rewriter.cpp | 5 +- src/ast/simplifiers/CMakeLists.txt | 1 + .../simplifiers}/bound_manager.cpp | 19 +++---- .../arith => ast/simplifiers}/bound_manager.h | 4 +- src/ast/simplifiers/extract_eqs.cpp | 49 +++++++++++++++---- src/cmd_context/extra_cmds/dbg_cmds.cpp | 2 +- src/tactic/arith/CMakeLists.txt | 1 - src/tactic/arith/add_bounds_tactic.cpp | 5 +- src/tactic/arith/eq2bv_tactic.cpp | 5 +- src/tactic/arith/lia2card_tactic.cpp | 5 +- src/tactic/arith/lia2pb_tactic.cpp | 5 +- src/tactic/arith/nla2bv_tactic.cpp | 5 +- src/tactic/arith/normalize_bounds_tactic.cpp | 15 +++--- src/tactic/arith/pb2bv_model_converter.h | 2 +- src/tactic/arith/pb2bv_tactic.cpp | 10 ++-- .../fd_solver/bounded_int2bv_solver.cpp | 7 ++- src/tactic/smtlogics/qflia_tactic.cpp | 5 +- 17 files changed, 86 insertions(+), 59 deletions(-) rename src/{tactic/arith => ast/simplifiers}/bound_manager.cpp (95%) rename src/{tactic/arith => ast/simplifiers}/bound_manager.h (95%) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index c2a9b4cf4..15456d41e 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -23,9 +23,8 @@ Notes: #include "ast/ast_pp.h" seq_util& arith_rewriter_core::seq() { - if (!m_seq) { - m_seq = alloc(seq_util, m); - } + if (!m_seq) + m_seq = alloc(seq_util, m); return *m_seq; } diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index b807b00e3..bd39395c0 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(simplifiers SOURCES bit_blaster.cpp + bound_manager.cpp bv_slice.cpp card2bv.cpp demodulator_simplifier.cpp diff --git a/src/tactic/arith/bound_manager.cpp b/src/ast/simplifiers/bound_manager.cpp similarity index 95% rename from src/tactic/arith/bound_manager.cpp rename to src/ast/simplifiers/bound_manager.cpp index d6422abff..0770bf421 100644 --- a/src/tactic/arith/bound_manager.cpp +++ b/src/ast/simplifiers/bound_manager.cpp @@ -16,10 +16,11 @@ Author: Notes: --*/ -#include "tactic/arith/bound_manager.h" + #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" -#include "tactic/goal.h" +#include "ast/ast_translation.h" +#include "ast/simplifiers/bound_manager.h" bound_manager::bound_manager(ast_manager & m): m_util(m), @@ -103,7 +104,9 @@ bool bound_manager::is_numeral(expr* v, numeral& n, bool& is_int) { return m_util.is_numeral(v, n, is_int); } -void bound_manager::operator()(expr * f, expr_dependency * d) { +void bound_manager::operator()(expr * f, expr_dependency * d, proof* p) { + if (p) + return; TRACE("bound_manager", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";); expr * v; numeral n; @@ -243,16 +246,6 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) { return true; } -void bound_manager::operator()(goal const & g) { - if (g.proofs_enabled()) - return; - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - operator()(g.form(i), g.dep(i)); - } -} - - void bound_manager::reset() { m_bounded_vars.finalize(); m_lowers.finalize(); diff --git a/src/tactic/arith/bound_manager.h b/src/ast/simplifiers/bound_manager.h similarity index 95% rename from src/tactic/arith/bound_manager.h rename to src/ast/simplifiers/bound_manager.h index 6047dd36d..967ac2e04 100644 --- a/src/tactic/arith/bound_manager.h +++ b/src/ast/simplifiers/bound_manager.h @@ -21,7 +21,6 @@ Notes: #include "ast/ast.h" #include "ast/arith_decl_plugin.h" -class goal; class bound_manager { public: @@ -50,8 +49,7 @@ public: ast_manager & m() const { return m_util.get_manager(); } - void operator()(goal const & g); - void operator()(expr * n, expr_dependency * d = nullptr); + void operator()(expr * n, expr_dependency * d, proof* p); bool has_lower(expr * c, numeral & v, bool & strict) const { limit l; diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index 66ebef85c..37d92bcbb 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -21,6 +21,7 @@ Author: #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/simplifiers/extract_eqs.h" +#include "ast/simplifiers/bound_manager.h" #include "params/tactic_params.hpp" @@ -83,6 +84,7 @@ namespace euf { class arith_extract_eq : public extract_eq { ast_manager& m; arith_util a; + bound_manager m_bm; expr_ref_vector m_args, m_trail; expr_sparse_mark m_nonzero; bool m_enabled = true; @@ -107,6 +109,17 @@ namespace euf { solve_eq(orig, u, term, d, eqs); } + void solve_to_real(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + expr* z, *u; + rational r; + if (!a.is_to_real(x, z) || !is_uninterp_const(z)) + return; + if (a.is_to_real(y, u)) + eqs.push_back(dependent_eq(orig, to_app(z), expr_ref(u, m), d)); + else if (a.is_numeral(y, r) && r.is_int()) + eqs.push_back(dependent_eq(orig, to_app(z), expr_ref(a.mk_int(r), m), d)); + } + /*** * Solve * x + Y = Z -> x = Z - Y @@ -157,8 +170,8 @@ namespace euf { for (expr* yarg : *to_app(arg)) { ++k; nonzero = k == j || m_nonzero.is_marked(yarg) || (a.is_numeral(yarg, r) && r != 0); - if (!nonzero) - break; +if (!nonzero) +break; } if (!nonzero) continue; @@ -222,12 +235,12 @@ namespace euf { } void add_pos(expr* f) { - expr* lhs = nullptr, *rhs = nullptr; + expr* lhs = nullptr, * rhs = nullptr; rational val; - if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg()) - mark_nonzero(lhs); + if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg()) + mark_nonzero(lhs); else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_pos()) - mark_nonzero(lhs); + mark_nonzero(lhs); else if (m.is_not(f, f)) { if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_neg()) mark_nonzero(lhs); @@ -242,11 +255,12 @@ namespace euf { solve_add(orig, x, y, d, eqs); solve_mod(orig, x, y, d, eqs); solve_mul(orig, x, y, d, eqs); + solve_to_real(orig, x, y, d, eqs); } public: - arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m), m_trail(m) {} + arith_extract_eq(ast_manager& m) : m(m), a(m), m_bm(m), m_args(m), m_trail(m) {} void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { if (!m_enabled) @@ -257,6 +271,18 @@ namespace euf { solve_eq(f, x, y, d, eqs); solve_eq(f, y, x, d, eqs); } + bool str; + rational lo, hi; + if (a.is_le(f, x, y) && a.is_numeral(y, hi) && m_bm.has_lower(x, lo, str) && !str && lo == hi) { + expr_dependency_ref d2(m); + d2 = m.mk_join(d, m_bm.lower_dep(x)); + if (is_uninterp_const(x)) + eqs.push_back(dependent_eq(f, to_app(x), expr_ref(y, m), d2)); + else { + solve_eq(f, x, y, d2, eqs); + solve_eq(f, y, x, d2, eqs); + } + } } void pre_process(dependent_expr_state& fmls) override { @@ -264,8 +290,13 @@ namespace euf { return; m_nonzero.reset(); m_trail.reset(); - for (unsigned i = 0; i < fmls.qtail(); ++i) - add_pos(fmls[i].fml()); + m_bm.reset(); + for (unsigned i = 0; i < fmls.qtail(); ++i) { + auto [f, p, d] = fmls[i](); + add_pos(f); + m_bm(f, d, p); + } + } diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 278c0a205..b18d43528 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -26,7 +26,7 @@ Notes: #include "ast/ast_lt.h" #include "cmd_context/simplify_cmd.h" #include "ast/ast_smt2_pp.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/used_vars.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_util.h" diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt index d5c7557e6..11aa87242 100644 --- a/src/tactic/arith/CMakeLists.txt +++ b/src/tactic/arith/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(arith_tactics SOURCES add_bounds_tactic.cpp arith_bounds_tactic.cpp - bound_manager.cpp bound_propagator.cpp bv2int_rewriter.cpp bv2real_rewriter.cpp diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index a544c6810..3d9f0bd25 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -19,7 +19,7 @@ Revision History: #include "tactic/tactical.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_smt2_pp.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" struct is_unbounded_proc { struct found {}; @@ -41,7 +41,8 @@ struct is_unbounded_proc { bool is_unbounded(goal const & g) { ast_manager & m = g.m(); bound_manager bm(m); - bm(g); + for (unsigned i = 0; i < g.size(); ++i) + bm(g.form(i), g.dep(i), g.pr(i)); is_unbounded_proc proc(bm); return test(g, proc); } diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 1711a34ac..0b2630236 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "tactic/tactical.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" @@ -179,7 +179,8 @@ public: tactic_report report("eq2bv", *g); - m_bounds(*g); + for (unsigned i = 0; i < g->size(); ++i) + m_bounds(g->form(i), g->dep(i), g->pr(i)); if (m_bounds.inconsistent() || g->proofs_enabled()) { g->inc_depth(); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index cb6f6c228..f8cd3674a 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -24,7 +24,7 @@ Notes: #include "ast/ast_util.h" #include "ast/ast_pp_util.h" #include "tactic/tactical.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/converters/generic_model_converter.h" class lia2card_tactic : public tactic { @@ -180,7 +180,8 @@ public: tactic_report report("lia2card", *g); bound_manager bounds(m); - bounds(*g); + for (unsigned i = 0; i < g->size(); ++i) + bounds(g->form(i), g->dep(i), g->pr(i)); for (expr* x : bounds) { checkpoint(); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index f78e85621..450a7d25a 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "tactic/tactical.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/rewriter/th_rewriter.h" #include "ast/for_each_expr.h" #include "ast/converters/generic_model_converter.h" @@ -197,7 +197,8 @@ class lia2pb_tactic : public tactic { return; } - m_bm(*g); + for (unsigned i = 0; i < g->size(); ++i) + m_bm(g->form(i), g->dep(i), g->pr(i)); TRACE("lia2pb", m_bm.display(tout);); diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index cd37db402..c791841ec 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -28,7 +28,7 @@ Notes: #include "tactic/arith/bv2int_rewriter.h" #include "tactic/arith/bv2real_rewriter.h" #include "ast/converters/generic_model_converter.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "util/obj_pair_hashtable.h" #include "ast/ast_smt2_pp.h" @@ -89,7 +89,8 @@ class nla2bv_tactic : public tactic { ); tactic_report report("nla->bv", g); m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); - m_bounds(g); + for (unsigned i = 0; i < g.size(); ++i) + m_bounds(g.form(i), g.dep(i), g.pr(i)); collect_power2(g); switch (collect_vars(g)) { case has_num: diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index b20eaf53a..7c09703eb 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include "tactic/tactical.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/rewriter/th_rewriter.h" #include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" @@ -67,13 +67,11 @@ class normalize_bounds_tactic : public tactic { } bool has_lowers() { - bound_manager::iterator it = m_bm.begin(); - bound_manager::iterator end = m_bm.end(); - for (; it != end; ++it) { + for (auto* e : m_bm) { TRACE("normalize_bounds_tactic", rational val; bool strict; - tout << mk_ismt2_pp(*it, m) << " has_lower: " << m_bm.has_lower(*it, val, strict) << " val: " << val << "\n";); - if (is_target(*it)) + tout << mk_ismt2_pp(e, m) << " has_lower: " << m_bm.has_lower(e, val, strict) << " val: " << val << "\n";); + if (is_target(e)) return true; } return false; @@ -83,8 +81,9 @@ class normalize_bounds_tactic : public tactic { bool produce_models = in->models_enabled(); bool produce_proofs = in->proofs_enabled(); tactic_report report("normalize-bounds", *in); - - m_bm(*in); + + for (unsigned i = 0; i < in->size(); ++i) + m_bm(in->form(i), in->dep(i), in->pr(i)); if (!has_lowers()) { result.push_back(in.get()); diff --git a/src/tactic/arith/pb2bv_model_converter.h b/src/tactic/arith/pb2bv_model_converter.h index 2de873ba2..3477a2081 100644 --- a/src/tactic/arith/pb2bv_model_converter.h +++ b/src/tactic/arith/pb2bv_model_converter.h @@ -19,7 +19,7 @@ Notes: #pragma once #include "ast/converters/model_converter.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" class pb2bv_model_converter : public model_converter { typedef std::pair func_decl_pair; diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 5ff7425ba..507a54b6a 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -28,7 +28,7 @@ Notes: #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/pb2bv_rewriter.h" #include "tactic/tactical.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "ast/converters/generic_model_converter.h" #include "tactic/arith/pb2bv_model_converter.h" #include "tactic/arith/pb2bv_tactic.h" @@ -913,7 +913,9 @@ private: return; } - m_bm(*g); + unsigned size = g->size(); + for (unsigned i = 0; i < size; i++) + m_bm(g->form(i), g->dep(i), g->pr(i)); TRACE("pb2bv", m_bm.display(tout);); @@ -924,7 +926,6 @@ private: throw_tactic(p.e); } - unsigned size = g->size(); expr_ref_vector new_exprs(m); expr_dependency_ref_vector new_deps(m); @@ -1042,7 +1043,8 @@ struct is_pb_probe : public probe { try { ast_manager & m = g.m(); bound_manager bm(m); - bm(g); + for (unsigned i = 0; i < g.size(); i++) + bm(g.form(i), g.dep(i), g.pr(i)); arith_util a_util(m); pb_util pb(m); expr_fast_mark1 visited; diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 4ac82c0c2..317286e1e 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -23,7 +23,7 @@ Notes: #include "ast/converters/generic_model_converter.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "tactic/arith/bv2int_rewriter.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/bv_decl_plugin.h" @@ -330,9 +330,8 @@ private: if (m_assertions.empty()) return; m_flushed = true; bound_manager& bm = *m_bounds.back(); - for (expr* a : m_assertions) { - bm(a); - } + for (expr* a : m_assertions) + bm(a, nullptr, nullptr); TRACE("int2bv", bm.display(tout);); expr_safe_replace sub(m); accumulate_sub(sub); diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index b8ebbd8a9..e72a63087 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -32,14 +32,15 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "tactic/smtlogics/smt_tactic.h" #include "sat/tactic/sat_tactic.h" -#include "tactic/arith/bound_manager.h" +#include "ast/simplifiers/bound_manager.h" #include "tactic/arith/probe_arith.h" struct quasi_pb_probe : public probe { result operator()(goal const & g) override { bool found_non_01 = false; bound_manager bm(g.m()); - bm(g); + for (unsigned i = 0; i < g.size(); ++i) + bm(g.form(i), g.dep(i), g.pr(i)); rational l, u; bool st; for (expr * t : bm) { if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one()))