From 2828126b725362ee08daf0cf8a774d0b09cc3dcb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 3 Oct 2017 10:20:49 -0700 Subject: [PATCH 1/8] add cancellation checks Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 2 + src/util/lp/lp_primal_core_solver_tableau.h | 45 ++++++++++++--------- src/util/lp/lp_settings.h | 3 +- 3 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 1ed30bd70..6d2cbea7d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -417,6 +417,8 @@ public: for (unsigned i : m_rows_with_changed_bounds.m_index) { calculate_implied_bounds_for_row(i, bp); + if (settings().get_cancel_flag()) + return; } m_rows_with_changed_bounds.clear(); if (!use_tableau()) { diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index 5c7d4d2c2..d2b8c1a26 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -176,25 +176,34 @@ unsigned lp_primal_core_solver::solve_with_tableau() { default: break; // do nothing } - } while (this->get_status() != FLOATING_POINT_ERROR - && - this->get_status() != UNBOUNDED - && - this->get_status() != OPTIMAL - && - this->get_status() != INFEASIBLE - && - this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements - && - this->total_iterations() <= this->m_settings.max_total_number_of_iterations - && - !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); + } while (this->get_status() != FLOATING_POINT_ERROR + && + this->get_status() != UNBOUNDED + && + this->get_status() != OPTIMAL + && + this->get_status() != INFEASIBLE + && + this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements + && + this->total_iterations() <= this->m_settings.max_total_number_of_iterations + && + !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) + && + m_settings.get_cancel_flag() == false); + + if (m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); + } - SASSERT(this->get_status() == FLOATING_POINT_ERROR - || - this->current_x_is_feasible() == false - || - this->calc_current_x_is_feasible_include_non_basis()); + SASSERT( + this->get_status() == FLOATING_POINT_ERROR + || + this->get_status() == CANCELLED + || + this->current_x_is_feasible() == false + || + this->calc_current_x_is_feasible_include_non_basis()); return this->total_iterations(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 70a9f1504..a7e6e2665 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -61,7 +61,8 @@ enum lp_status { TIME_EXHAUSTED, ITERATIONS_EXHAUSTED, EMPTY, - UNSTABLE + UNSTABLE, + CANCELLED }; // when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only From fd3d785a5b41715a5a1c61ea03038c550483030e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Oct 2017 14:49:45 -0700 Subject: [PATCH 2/8] add this-> Signed-off-by: Lev Nachmanson --- src/util/lp/lp_primal_core_solver_tableau.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index d2b8c1a26..0c56f0ab9 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -190,10 +190,10 @@ unsigned lp_primal_core_solver::solve_with_tableau() { && !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) && - m_settings.get_cancel_flag() == false); + this->m_settings.get_cancel_flag() == false); - if (m_settings.get_cancel_flag()) { - this->set_status(CANCELLED); + if (this->m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); } SASSERT( From 6268ff1fa13d283c9b4b0461f2b4423509a554ee Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 5 Oct 2017 18:10:20 +0100 Subject: [PATCH 3/8] dom_simplify improvements with Nikolaj --- src/tactic/core/dom_simplify_tactic.cpp | 129 ++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 19 +++- 2 files changed, 102 insertions(+), 46 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index d4a3031cd..85b7fd9d6 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -95,13 +95,16 @@ void expr_dominators::compute_dominators() { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); - expr * new_idom = p[0], * idom2 = 0; - for (unsigned j = 1; j < p.size(); ++j) { - if (m_doms.find(p[j], idom2)) { + expr * new_idom = 0, *idom2 = 0; + for (unsigned j = 0; j < p.size(); ++j) { + if (!new_idom) { + m_doms.find(p[j], new_idom); + } + else if (m_doms.find(p[j], idom2)) { new_idom = intersect(new_idom, idom2); } } - if (!m_doms.find(child, idom2) || idom2 != new_idom) { + if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { m_doms.insert(child, new_idom); change = true; } @@ -113,7 +116,7 @@ void expr_dominators::extract_tree() { for (auto const& kv : m_doms) { add_edge(m_tree, kv.m_value, kv.m_key); } -} +} void expr_dominators::compile(expr * e) { reset(); @@ -147,9 +150,9 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) { } void dom_simplify_tactic::operator()( - goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; @@ -162,33 +165,41 @@ void dom_simplify_tactic::operator()( } void dom_simplify_tactic::cleanup() { - m_trail.reset(); - m_args.reset(); - m_args2.reset(); - m_result.reset(); - m_dominators.reset(); + m_trail.reset(); + m_args.reset(); + m_args2.reset(); + m_result.reset(); + m_dominators.reset(); } expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref r(m); - expr * c = 0, * t = 0, * e = 0; + expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); expr_ref new_c = simplify(c); if (m.is_true(new_c)) { r = simplify(t); - } - else if (m.is_false(new_c) || !assert_expr(new_c, false)) { + } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { r = simplify(e); - } - else { - expr_ref new_t = simplify(t); + } else { + for (expr * child : tree(ite)) { + if (is_subexpr(child, t) && !is_subexpr(child, e)) { + simplify(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { return new_t; } - expr_ref new_e = simplify(e); + for (expr * child : tree(ite)) { + if (is_subexpr(child, e) && !is_subexpr(child, t)) { + simplify(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_e = simplify(e); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -197,7 +208,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { } else { TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";); - r = m.mk_ite(new_c, new_t, new_c); + r = m.mk_ite(new_c, new_t, new_e); } } return r; @@ -224,11 +235,8 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { r = simplify_or(to_app(e)); } else { - expr_dominators::tree_t const& t = m_dominators.get_tree(); - if (auto children = t.find_core(e)) { - for (expr * child : children->get_data().m_value) { - simplify(child); - } + for (expr * child : tree(e)) { + simplify(child); } if (is_app(e)) { m_args.reset(); @@ -251,27 +259,33 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { expr_ref r(m); unsigned old_lvl = scope_level(); - m_args.reset(); + + auto is_subexpr_arg = [&](expr * child, expr * except) { + if (!is_subexpr(child, except)) + return false; + for (expr * arg : *e) { + if (arg != except && is_subexpr(child, arg)) + return false; + } + return true; + }; + + expr_ref_vector args(m); for (expr * arg : *e) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); + for (expr * child : tree(arg)) { + if (is_subexpr_arg(child, arg)) { + simplify(child); + } + } + r = simplify(arg); + args.push_back(r); + if (!assert_expr(simplify(arg), !is_and)) { + r = is_and ? m.mk_false() : m.mk_true(); + return r; } - m_args.push_back(r); } pop(scope_level() - old_lvl); - m_args.reverse(); - m_args2.reset(); - for (expr * arg : m_args) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); - } - m_args2.push_back(r); - } - pop(scope_level() - old_lvl); - m_args2.reverse(); - r = is_and ? mk_and(m_args2) : mk_or(m_args2); + r = is_and ? mk_and(args) : mk_or(args); return r; } @@ -332,11 +346,36 @@ void dom_simplify_tactic::simplify_goal(goal& g) { SASSERT(scope_level() == 0); } +bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { + if (a == b) + return true; + + bool r; + if (m_subexpr_cache.find(a, b, r)) + return r; + + for (expr * e : tree(b)) { + if (is_subexpr(a, e)) { + m_subexpr_cache.insert(a, b, true); + return true; + } + } + m_subexpr_cache.insert(a, b, false); + return false; +} + +ptr_vector const & dom_simplify_tactic::tree(expr * e) { + if (auto p = m_dominators.get_tree().find_core(e)) + return p->get_data().get_value(); + return m_empty; +} + // ---------------------- // expr_substitution_simplifier bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) { + m_scoped_substitution.push(); expr* tt; if (!sign) { update_substitution(t, 0); @@ -439,3 +478,7 @@ void expr_substitution_simplifier::compute_depth(expr* e) { m_expr2depth.insert(e, d + 1); } } + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p)); +} diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 2fa79dd1d..9fe59de23 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -23,6 +23,8 @@ Notes: #include "ast/ast.h" #include "ast/expr_substitution.h" #include "tactic/tactic.h" +#include "tactic/tactical.h" +#include "util/obj_pair_hashtable.h" class expr_dominators { @@ -89,6 +91,8 @@ private: unsigned m_scope_level; unsigned m_depth; unsigned m_max_depth; + ptr_vector m_empty; + obj_pair_map m_subexpr_cache; expr_ref simplify(expr* t); expr_ref simplify_ite(app * ite); @@ -97,9 +101,13 @@ private: expr_ref simplify_and_or(bool is_and, app * ite); void simplify_goal(goal& g); - expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(r, r)) r = t; return expr_ref(r, m); } + bool is_subexpr(expr * a, expr * b); + + expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); } void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } + ptr_vector const & tree(expr * e); + unsigned scope_level() { return m_scope_level; } void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); } @@ -156,8 +164,13 @@ public: SASSERT(m_subst.empty()); return alloc(expr_substitution_simplifier, m); } - - }; + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* +ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)") +*/ + #endif From f59cf2452d9a335785bd1691dbf04b93973193d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Oct 2017 22:20:31 +0100 Subject: [PATCH 4/8] #1284 build problems Signed-off-by: Nikolaj Bjorner --- src/tactic/core/CMakeLists.txt | 2 + src/tactic/core/dom_simplify_tactic.cpp | 1 + src/tactic/core/dom_simplify_tactic.h | 53 +++++++++++++------------ 3 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index f192b4fa6..16778d8dd 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -7,6 +7,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp der_tactic.cpp distribute_forall_tactic.cpp + dom_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp injectivity_tactic.cpp @@ -32,6 +33,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.h der_tactic.h distribute_forall_tactic.h + dom_simplify_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h injectivity_tactic.h diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 85b7fd9d6..bba27cf46 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -188,6 +188,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { simplify(child); } } + pop(scope_level() - old_lvl); expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 9fe59de23..825a173bf 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -58,32 +58,35 @@ public: }; +class dom_simplifier { + public: + dom_simplifier() {} + + virtual ~dom_simplifier() {} + /** + \brief assert_expr performs an implicit push + */ + virtual bool assert_expr(expr * t, bool sign) = 0; + + /** + \brief apply simplification. + */ + virtual void operator()(expr_ref& r) = 0; + + /** + \brief pop scopes accumulated from assertions. + */ + virtual void pop(unsigned num_scopes) = 0; + + virtual dom_simplifier * translate(ast_manager & m) = 0; + +}; + class dom_simplify_tactic : public tactic { public: - class simplifier { - public: - virtual ~simplifier() {} - /** - \brief assert_expr performs an implicit push - */ - virtual bool assert_expr(expr * t, bool sign) = 0; - - /** - \brief apply simplification. - */ - virtual void operator()(expr_ref& r) = 0; - - /** - \brief pop scopes accumulated from assertions. - */ - virtual void pop(unsigned num_scopes) = 0; - - virtual simplifier * translate(ast_manager & m); - - }; private: ast_manager& m; - simplifier* m_simplifier; + dom_simplifier* m_simplifier; params_ref m_params; expr_ref_vector m_trail, m_args, m_args2; obj_map m_result; @@ -115,7 +118,7 @@ private: void init(goal& g); public: - dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()): + dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m), m_simplifier(s), m_params(p), m_trail(m), m_args(m), m_args2(m), m_dominators(m), @@ -138,7 +141,7 @@ public: virtual void cleanup(); }; -class expr_substitution_simplifier : public dom_simplify_tactic::simplifier { +class expr_substitution_simplifier : public dom_simplifier { ast_manager& m; expr_substitution m_subst; scoped_expr_substitution m_scoped_substitution; @@ -160,7 +163,7 @@ public: virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); } - virtual simplifier * translate(ast_manager & m) { + virtual dom_simplifier * translate(ast_manager & m) { SASSERT(m_subst.empty()); return alloc(expr_substitution_simplifier, m); } From eac659f748fc3209fca947556d94d9b08a3c8c82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 11:34:14 +0100 Subject: [PATCH 5/8] deal with empty set of post-orders Signed-off-by: Nikolaj Bjorner --- src/muz/rel/karr_relation.cpp | 4 ++-- .../transforms/dl_mk_interp_tail_simplifier.cpp | 4 ++-- src/smt/theory_lra.cpp | 4 ++-- src/tactic/core/dom_simplify_tactic.cpp | 14 ++++++++------ src/tactic/core/dom_simplify_tactic.h | 4 ++-- 5 files changed, 16 insertions(+), 14 deletions(-) diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index 572d5e8d5..c8a489d69 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -111,8 +111,8 @@ namespace datalog { void filter_interpreted(app* cond) { rational one(1), mone(-1); - expr* e1, *e2, *en; - var* v, *w; + expr* e1 = 0, *e2 = 0, *en = 0; + var* v = 0, *w = 0; rational n1, n2; expr_ref_vector conjs(m); flatten_and(cond, conjs); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 30505a5e8..7bd35b4ef 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -398,8 +398,8 @@ namespace datalog { } bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) { - if (!m_context.get_params ().xform_tail_simplifier_pve ()) - return false; + if (!m_context.get_params ().xform_tail_simplifier_pve ()) + return false; unsigned u_len = r->get_uninterpreted_tail_size(); unsigned len = r->get_tail_size(); if (u_len == len) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0bb76cd90..7fec6f836 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -721,7 +721,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; @@ -862,7 +862,7 @@ namespace smt { void relevant_eh(app* n) { TRACE("arith", tout << mk_pp(n, m) << "\n";); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; if (a.is_mod(n, n1, n2)) mk_idiv_mod_axioms(n1, n2); else if (a.is_rem(n, n1, n2)) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index bba27cf46..17262a9d6 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -90,8 +90,8 @@ void expr_dominators::compute_dominators() { bool change = true; while (change) { change = false; - SASSERT(m_post2expr.back() == e); - for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) { + SASSERT(m_post2expr.empty() || m_post2expr.back() == e); + for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); @@ -167,7 +167,6 @@ void dom_simplify_tactic::operator()( void dom_simplify_tactic::cleanup() { m_trail.reset(); m_args.reset(); - m_args2.reset(); m_result.reset(); m_dominators.reset(); } @@ -180,9 +179,11 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref new_c = simplify(c); if (m.is_true(new_c)) { r = simplify(t); - } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { + } + else if (m.is_false(new_c) || !assert_expr(new_c, false)) { r = simplify(e); - } else { + } + else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { simplify(child); @@ -254,6 +255,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; + m_subexpr_cache.reset(); return r; } @@ -361,7 +363,7 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { return true; } } - m_subexpr_cache.insert(a, b, false); + m_subexpr_cache.insert(a, b, false); return false; } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 825a173bf..c62651c5c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -88,7 +88,7 @@ private: ast_manager& m; dom_simplifier* m_simplifier; params_ref m_params; - expr_ref_vector m_trail, m_args, m_args2; + expr_ref_vector m_trail, m_args; obj_map m_result; expr_dominators m_dominators; unsigned m_scope_level; @@ -120,7 +120,7 @@ private: public: dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m), m_simplifier(s), m_params(p), - m_trail(m), m_args(m), m_args2(m), + m_trail(m), m_args(m), m_dominators(m), m_scope_level(0), m_depth(0), m_max_depth(1024) {} From 6df628edc7043a08dd11eae3d2ab8d44e07a172c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 11:45:29 +0100 Subject: [PATCH 6/8] pin elements in expr2depth Signed-off-by: Nikolaj Bjorner --- src/smt/smt_implied_equalities.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- src/tactic/bv/bv_bounds_tactic.cpp | 6 ++++-- src/tactic/core/dom_simplify_tactic.cpp | 2 ++ src/tactic/core/dom_simplify_tactic.h | 3 ++- 5 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 7d54e714e..d021708fc 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -284,7 +284,7 @@ namespace smt { } lbool reduce_cond(model_ref& model, expr* e) { - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) { if (e1 == e2) { return l_true; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 7fec6f836..292d2ab0d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -689,7 +689,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index d2cd0d66c..1f0bb8473 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -70,11 +70,13 @@ struct interval { if (is_wrapped()) { // l >= b.l >= b.h >= h return b.is_wrapped() && h <= b.h && l >= b.l; - } else if (b.is_wrapped()) { + } + else if (b.is_wrapped()) { // b.l > b.h >= h >= l // h >= l >= b.l > b.h return h <= b.h || l >= b.l; - } else { + } + else { // return l >= b.l && h <= b.h; } diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 17262a9d6..08037fe18 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -430,6 +430,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) { if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { compute_depth(lhs); compute_depth(rhs); + m_trail.push_back(lhs); + m_trail.push_back(rhs); if (is_gt(lhs, rhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); m_scoped_substitution.insert(lhs, rhs, pr); diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index c62651c5c..25fb7c24f 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -146,6 +146,7 @@ class expr_substitution_simplifier : public dom_simplifier { expr_substitution m_subst; scoped_expr_substitution m_scoped_substitution; obj_map m_expr2depth; + expr_ref_vector m_trail; // move from asserted_formulas to here.. void compute_depth(expr* e); @@ -153,7 +154,7 @@ class expr_substitution_simplifier : public dom_simplifier { unsigned depth(expr* e) { return m_expr2depth[e]; } public: - expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {} + expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {} virtual ~expr_substitution_simplifier() {} virtual bool assert_expr(expr * t, bool sign); From cb548404bc1ad5a55628e1dd23fc4efe69de8856 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 12:08:37 +0100 Subject: [PATCH 7/8] bail out dominators after log number of steps Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 1227 ++++++++++++++--------- src/tactic/core/dom_simplify_tactic.cpp | 25 +- src/tactic/core/dom_simplify_tactic.h | 8 +- 3 files changed, 792 insertions(+), 468 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 1f0bb8473..2d5eb216a 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -18,6 +18,7 @@ Author: #include "tactic/bv/bv_bounds_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" +#include "tactic/core/dom_simplify_tactic.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" #include @@ -29,509 +30,825 @@ static uint64 uMaxInt(unsigned sz) { namespace { -struct interval { - // l < h: [l, h] - // l > h: [0, h] U [l, UMAX_INT] - uint64 l, h; - unsigned sz; - bool tight; + struct interval { + // l < h: [l, h] + // l > h: [0, h] U [l, UMAX_INT] + uint64 l, h; + unsigned sz; + bool tight; - interval() {} - interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { - // canonicalize full set - if (is_wrapped() && l == h + 1) { - this->l = 0; - this->h = uMaxInt(sz); - } - SASSERT(invariant()); - } - - bool invariant() const { - return l <= uMaxInt(sz) && h <= uMaxInt(sz) && - (!is_wrapped() || l != h+1); - } - - bool is_full() const { return l == 0 && h == uMaxInt(sz); } - bool is_wrapped() const { return l > h; } - bool is_singleton() const { return l == h; } - - bool operator==(const interval& b) const { - SASSERT(sz == b.sz); - return l == b.l && h == b.h && tight == b.tight; - } - bool operator!=(const interval& b) const { return !(*this == b); } - - bool implies(const interval& b) const { - if (b.is_full()) - return true; - if (is_full()) - return false; - - if (is_wrapped()) { - // l >= b.l >= b.h >= h - return b.is_wrapped() && h <= b.h && l >= b.l; - } - else if (b.is_wrapped()) { - // b.l > b.h >= h >= l - // h >= l >= b.l > b.h - return h <= b.h || l >= b.l; - } - else { - // - return l >= b.l && h <= b.h; - } - } - - /// return false if intersection is unsat - bool intersect(const interval& b, interval& result) const { - if (is_full() || *this == b) { - result = b; - return true; - } - if (b.is_full()) { - result = *this; - return true; + interval() {} + interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + // canonicalize full set + if (is_wrapped() && l == h + 1) { + this->l = 0; + this->h = uMaxInt(sz); + } + SASSERT(invariant()); } - if (is_wrapped()) { - if (b.is_wrapped()) { - if (h >= b.l) { - result = b; - } else if (b.h >= l) { - result = *this; + bool invariant() const { + return l <= uMaxInt(sz) && h <= uMaxInt(sz) && + (!is_wrapped() || l != h+1); + } + + bool is_full() const { return l == 0 && h == uMaxInt(sz); } + bool is_wrapped() const { return l > h; } + bool is_singleton() const { return l == h; } + + bool operator==(const interval& b) const { + SASSERT(sz == b.sz); + return l == b.l && h == b.h && tight == b.tight; + } + bool operator!=(const interval& b) const { return !(*this == b); } + + bool implies(const interval& b) const { + if (b.is_full()) + return true; + if (is_full()) + return false; + + if (is_wrapped()) { + // l >= b.l >= b.h >= h + return b.is_wrapped() && h <= b.h && l >= b.l; + } + else if (b.is_wrapped()) { + // b.l > b.h >= h >= l + // h >= l >= b.l > b.h + return h <= b.h || l >= b.l; + } + else { + // + return l >= b.l && h <= b.h; + } + } + + /// return false if intersection is unsat + bool intersect(const interval& b, interval& result) const { + if (is_full() || *this == b) { + result = b; + return true; + } + if (b.is_full()) { + result = *this; + return true; + } + + if (is_wrapped()) { + if (b.is_wrapped()) { + if (h >= b.l) { + result = b; + } else if (b.h >= l) { + result = *this; + } else { + result = interval(std::max(l, b.l), std::min(h, b.h), sz); + } } else { - result = interval(std::max(l, b.l), std::min(h, b.h), sz); + return b.intersect(*this, result); + } + } + else if (b.is_wrapped()) { + // ... b.h ... l ... h ... b.l .. + if (h < b.l && l > b.h) { + return false; + } + // ... l ... b.l ... h ... + if (h >= b.l && l <= b.h) { + result = b; + } else if (h >= b.l) { + result = interval(b.l, h, sz); + } else { + // ... l .. b.h .. h .. b.l ... + SASSERT(l <= b.h); + result = interval(l, std::min(h, b.h), sz); } } else { - return b.intersect(*this, result); - } - } else if (b.is_wrapped()) { - // ... b.h ... l ... h ... b.l .. - if (h < b.l && l > b.h) { - return false; - } - // ... l ... b.l ... h ... - if (h >= b.l && l <= b.h) { - result = b; - } else if (h >= b.l) { - result = interval(b.l, h, sz); - } else { - // ... l .. b.h .. h .. b.l ... - SASSERT(l <= b.h); - result = interval(l, std::min(h, b.h), sz); - } - } else { - if (l > b.h || h < b.l) - return false; + if (l > b.h || h < b.l) + return false; - // 0 .. l.. l' ... h ... h' - result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); - } - return true; - } - - /// return false if negation is empty - bool negate(interval& result) const { - if (!tight) { - result = interval(0, uMaxInt(sz), true); + // 0 .. l.. l' ... h ... h' + result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); + } return true; } - if (is_full()) - return false; - if (l == 0) { - result = interval(h + 1, uMaxInt(sz), sz); - } else if (uMaxInt(sz) == h) { - result = interval(0, l - 1, sz); - } else { - result = interval(h + 1, l - 1, sz); + /// return false if negation is empty + bool negate(interval& result) const { + if (!tight) { + result = interval(0, uMaxInt(sz), true); + return true; + } + + if (is_full()) + return false; + if (l == 0) { + result = interval(h + 1, uMaxInt(sz), sz); + } else if (uMaxInt(sz) == h) { + result = interval(0, l - 1, sz); + } else { + result = interval(h + 1, l - 1, sz); + } + return true; } - return true; - } -}; + }; #ifdef _TRACE -std::ostream& operator<<(std::ostream& o, const interval& I) { - o << "[" << I.l << ", " << I.h << "]"; - return o; -} -#endif - - -struct undo_bound { - expr* e; - interval b; - bool fresh; - undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} -}; - -class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { - typedef obj_map map; - typedef obj_map expr_set; - typedef obj_map expr_cnt; - - ast_manager& m; - params_ref m_params; - bool m_propagate_eq; - bv_util m_bv; - vector m_scopes; - map m_bound; - svector m_expr_vars; - svector m_bound_exprs; - - bool is_number(expr *e, uint64& n, unsigned& sz) const { - rational r; - if (m_bv.is_numeral(e, r, sz) && sz <= 64) { - n = r.get_uint64(); - return true; - } - return false; - } - - bool is_bound(expr *e, expr*& v, interval& b) const { - uint64 n; - expr *lhs, *rhs; - unsigned sz; - - if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C ule x <=> x uge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, uMaxInt(sz), sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x ule C - b = interval(0, n, sz, true); - v = lhs; - return true; - } - } else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C sle x <=> x sge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, (1ull << (sz-1)) - 1, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x sle C - b = interval(1ull << (sz-1), n, sz, true); - v = lhs; - return true; - } - } else if (m.is_eq(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, n, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { - b = interval(n, n, sz, true); - v = lhs; - return true; - } - } - return false; - } - -#if 0 - expr_set* get_expr_vars(expr* t) { - unsigned id = t->get_id(); - m_expr_vars.reserve(id + 1); - expr_set*& entry = m_expr_vars[id]; - if (entry) - return entry; - - expr_set* set = alloc(expr_set); - entry = set; - - if (!m_bv.is_numeral(t)) - set->insert(t, true); - - if (!is_app(t)) - return set; - - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_set* set_arg = get_expr_vars(a->get_arg(i)); - for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert(I->m_key, true); - } - } - return set; + std::ostream& operator<<(std::ostream& o, const interval& I) { + o << "[" << I.l << ", " << I.h << "]"; + return o; } #endif -#if 0 - expr_cnt* get_expr_bounds(expr* t) { - unsigned id = t->get_id(); - m_bound_exprs.reserve(id + 1); - expr_cnt*& entry = m_bound_exprs[id]; - if (entry) - return entry; - expr_cnt* set = alloc(expr_cnt); - entry = set; - - if (!is_app(t)) - return set; - - interval b; + struct undo_bound { expr* e; - if (is_bound(t, e, b)) { - set->insert_if_not_there2(e, 0)->get_data().m_value++; + interval b; + bool fresh; + undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} + }; + + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; } - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); - for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } } + return false; + } + +#if 0 + expr_set* get_expr_vars(expr* t) { + unsigned id = t->get_id(); + m_expr_vars.reserve(id + 1); + expr_set*& entry = m_expr_vars[id]; + if (entry) + return entry; + + expr_set* set = alloc(expr_set); + entry = set; + + if (!m_bv.is_numeral(t)) + set->insert(t, true); + + if (!is_app(t)) + return set; + + app* a = to_app(t); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_set* set_arg = get_expr_vars(a->get_arg(i)); + for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert(I->m_key, true); + } + } + return set; } - return set; - } #endif -public: - bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - updt_params(p); - } +#if 0 + expr_cnt* get_expr_bounds(expr* t) { + unsigned id = t->get_id(); + m_bound_exprs.reserve(id + 1); + expr_cnt*& entry = m_bound_exprs[id]; + if (entry) + return entry; - virtual void updt_params(params_ref const & p) { - m_propagate_eq = p.get_bool("propagate_eq", false); - } + expr_cnt* set = alloc(expr_cnt); + entry = set; - static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); - } + if (!is_app(t)) + return set; - virtual ~bv_bounds_simplifier() { - for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { - dealloc(m_expr_vars[i]); - } - for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { - dealloc(m_bound_exprs[i]); - } - } - - virtual bool assert_expr(expr * t, bool sign) { - while (m.is_not(t, t)) { - sign = !sign; - } - - interval b; - expr* t1; - if (is_bound(t, t1, b)) { - SASSERT(!m_bv.is_numeral(t1)); - if (sign) - VERIFY(b.negate(b)); - - TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); - map::obj_map_entry* e = m_bound.find_core(t1); - if (e) { - interval& old = e->get_data().m_value; - interval intr; - if (!old.intersect(b, intr)) - return false; - if (old == intr) - return true; - m_scopes.insert(undo_bound(t1, old, false)); - old = intr; - } else { - m_bound.insert(t1, b); - m_scopes.insert(undo_bound(t1, interval(), true)); - } - } - return true; - } - - virtual bool simplify(expr* t, expr_ref& result) { - expr* t1; - interval b; - - if (m_bound.find(t, b) && b.is_singleton()) { - result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); - return true; - } - - if (!m.is_bool(t)) - return false; - - bool sign = false; - while (m.is_not(t, t)) { - sign = !sign; - } - - if (!is_bound(t, t1, b)) - return false; - - if (sign && b.tight) { - sign = false; - if (!b.negate(b)) { - result = m.mk_false(); - return true; - } - } - - interval ctx, intr; - result = 0; - - if (b.is_full() && b.tight) { - result = m.mk_true(); - } else if (m_bound.find(t1, ctx)) { - if (ctx.implies(b)) { - result = m.mk_true(); - } else if (!b.intersect(ctx, intr)) { - result = m.mk_false(); - } else if (m_propagate_eq && intr.is_singleton()) { - result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), - m.get_sort(t1))); - } - } - - CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); - if (sign && result != 0) - result = m.mk_not(result); - return result != 0; - } - - // check if t contains v - ptr_vector todo; - bool contains(expr* t, expr* v) { - ast_fast_mark1 mark; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } - if (t == v) { - todo.reset(); - return true; - } - mark.mark(t); - - if (!is_app(t)) { - continue; - } - app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - bool contains_bound(expr* t) { - ast_fast_mark1 mark1; - ast_fast_mark2 mark2; - - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark1.is_marked(t)) { - continue; - } - mark1.mark(t); - - if (!is_app(t)) { - continue; - } interval b; expr* e; if (is_bound(t, e, b)) { - if (mark2.is_marked(e)) { - todo.reset(); - return true; - } - mark2.mark(e); - if (m_bound.contains(e)) { - todo.reset(); - return true; - } + set->insert_if_not_there2(e, 0)->get_data().m_value++; } app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - virtual bool may_simplify(expr* t) { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); + for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + } + } + return set; } #endif - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); + public: + bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); } - if (contains_bound(t)) { - return true; + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif - return false; - } - virtual void pop(unsigned num_scopes) { - TRACE("bv", tout << "pop: " << num_scopes << "\n";); - if (m_scopes.empty()) - return; - unsigned target = m_scopes.size() - num_scopes; - if (target == 0) { - m_bound.reset(); - m_scopes.reset(); - return; + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); } - for (unsigned i = m_scopes.size()-1; i >= target; --i) { - undo_bound& undo = m_scopes[i]; - SASSERT(m_bound.contains(undo.e)); - if (undo.fresh) { - m_bound.erase(undo.e); - } else { - m_bound.insert(undo.e, undo.b); + + virtual ~bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); } } - m_scopes.shrink(target); - } - virtual simplifier * translate(ast_manager & m) { - return alloc(bv_bounds_simplifier, m, m_params); - } + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } - virtual unsigned scope_level() const { - return m_scopes.size(); - } -}; + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual bool simplify(expr* t, expr_ref& result) { + expr* t1; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return true; + } + + if (!m.is_bool(t)) + return false; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return false; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + result = m.mk_false(); + return true; + } + } + + interval ctx, intr; + result = 0; + + if (b.is_full() && b.tight) { + result = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + result = m.mk_true(); + } else if (!b.intersect(ctx, intr)) { + result = m.mk_false(); + } else if (m_propagate_eq && intr.is_singleton()) { + result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + + CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); + if (sign && result != 0) + result = m.mk_not(result); + return result != 0; + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } +#endif + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) { + return b.is_full() || m_bound.contains(t1); + } + + if (contains_bound(t)) { + return true; + } +#if 0 + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } +#endif + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual simplifier * translate(ast_manager & m) { + return alloc(bv_bounds_simplifier, m, m_params); + } + + virtual unsigned scope_level() const { + return m_scopes.size(); + } + }; + + + class dom_bv_bounds_simplifier : public dom_simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; + } + + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } + } + return false; + } + + + public: + dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); + } + + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); + } + + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); + } + + virtual ~dom_bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); + } + } + + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } + + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual void operator()(expr_ref& r) { + expr* t1, * t = r; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + r = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return; + } + + if (!m.is_bool(t)) + return; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + r = m.mk_false(); + return; + } + } + + interval ctx, intr; + bool unchanged = false; + if (b.is_full() && b.tight) { + r = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + r = m.mk_true(); + } else if (!b.intersect(ctx, intr)) { + r = m.mk_false(); + } else if (m_propagate_eq && intr.is_singleton()) { + r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + else { + unchanged = true; + } + + CTRACE("bv", !unchanged, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); + if (sign && unchanged) + r = m.mk_not(r); + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } +#endif + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) { + return b.is_full() || m_bound.contains(t1); + } + + if (contains_bound(t)) { + return true; + } +#if 0 + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } +#endif + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual dom_simplifier * translate(ast_manager & m) { + return alloc(dom_bv_bounds_simplifier, m, m_params); + } + + virtual unsigned scope_level() const { + return m_scopes.size(); + } + }; } tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p)); } + +tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p)); +} diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 08037fe18..d38324db9 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -83,11 +83,12 @@ expr* expr_dominators::intersect(expr* x, expr * y) { return x; } -void expr_dominators::compute_dominators() { +bool expr_dominators::compute_dominators() { expr * e = m_root; SASSERT(m_doms.empty()); m_doms.insert(e, e); bool change = true; + unsigned iterations = 1; while (change) { change = false; SASSERT(m_post2expr.empty() || m_post2expr.back() == e); @@ -109,7 +110,12 @@ void expr_dominators::compute_dominators() { change = true; } } + iterations *= 2; + if (change && iterations > m_post2expr.size()) { + return false; + } } + return true; } void expr_dominators::extract_tree() { @@ -118,17 +124,18 @@ void expr_dominators::extract_tree() { } } -void expr_dominators::compile(expr * e) { +bool expr_dominators::compile(expr * e) { reset(); m_root = e; compute_post_order(); - compute_dominators(); + if (!compute_dominators()) return false; extract_tree(); + return true; } -void expr_dominators::compile(unsigned sz, expr * const* es) { +bool expr_dominators::compile(unsigned sz, expr * const* es) { expr_ref e(m.mk_and(sz, es), m); - compile(e); + return compile(e); } void expr_dominators::reset() { @@ -293,14 +300,14 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { } -void dom_simplify_tactic::init(goal& g) { +bool dom_simplify_tactic::init(goal& g) { expr_ref_vector args(m); unsigned sz = g.size(); for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i)); expr_ref fml = mk_and(args); m_result.reset(); m_trail.reset(); - m_dominators.compile(fml); + return m_dominators.compile(fml); } void dom_simplify_tactic::simplify_goal(goal& g) { @@ -312,7 +319,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change = false; // go forwards - init(g); + if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { expr_ref r = simplify(g.form(i)); @@ -329,7 +336,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { pop(scope_level()); // go backwards - init(g); + if (!init(g)) return; sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 25fb7c24f..6e5833cdb 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -45,14 +45,14 @@ private: void compute_post_order(); expr* intersect(expr* x, expr * y); - void compute_dominators(); + bool compute_dominators(); void extract_tree(); public: expr_dominators(ast_manager& m): m(m), m_root(m) {} - void compile(expr * e); - void compile(unsigned sz, expr * const* es); + bool compile(expr * e); + bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); @@ -115,7 +115,7 @@ private: void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); } - void init(goal& g); + bool init(goal& g); public: dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): From 755ca46df65209f275966886acc968ea02533992 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 12:15:41 +0100 Subject: [PATCH 8/8] adding bv_bounds tactic dominator style Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 58 +++++------------------------- 1 file changed, 9 insertions(+), 49 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 2d5eb216a..44f920840 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -560,7 +560,7 @@ namespace { bool is_bound(expr *e, expr*& v, interval& b) const { uint64 n; expr *lhs = 0, *rhs = 0; - unsigned sz; + unsigned sz = 0; if (m_bv.is_bv_ule(e, lhs, rhs)) { if (is_number(lhs, n, sz)) { // C ule x <=> x uge C @@ -689,25 +689,27 @@ namespace { } interval ctx, intr; - bool unchanged = false; + bool was_updated = true; if (b.is_full() && b.tight) { r = m.mk_true(); } else if (m_bound.find(t1, ctx)) { if (ctx.implies(b)) { r = m.mk_true(); - } else if (!b.intersect(ctx, intr)) { + } + else if (!b.intersect(ctx, intr)) { r = m.mk_false(); - } else if (m_propagate_eq && intr.is_singleton()) { + } + else if (m_propagate_eq && intr.is_singleton()) { r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), m.get_sort(t1))); } } else { - unchanged = true; + was_updated = false; } - CTRACE("bv", !unchanged, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); - if (sign && unchanged) + CTRACE("bv", was_updated, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); + if (sign && was_updated) r = m.mk_not(r); } @@ -773,45 +775,6 @@ namespace { return false; } - virtual bool may_simplify(expr* t) { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; - } -#endif - - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); - } - - if (contains_bound(t)) { - return true; - } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif - return false; - } - virtual void pop(unsigned num_scopes) { TRACE("bv", tout << "pop: " << num_scopes << "\n";); if (m_scopes.empty()) @@ -838,9 +801,6 @@ namespace { return alloc(dom_bv_bounds_simplifier, m, m_params); } - virtual unsigned scope_level() const { - return m_scopes.size(); - } }; }