From 48a2d3d5b60cbaeee4d9dcce1670d6c2e261b981 Mon Sep 17 00:00:00 2001 From: trinhmt <17382958+trinhmt@users.noreply.github.com> Date: Tue, 2 Jun 2020 00:02:50 +0800 Subject: [PATCH 01/16] fix #4481 (#4484) --- src/smt/seq_eq_solver.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 0a5d5d597..ab83768c6 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -775,6 +775,10 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c for (unsigned i = 0; i < ls.size(); ++i) { if (eq_unit(ls[i], rs.back())) { bool same = true; + if (i == 0) { + m_overlap_lhs.insert(pair, true); + return true; + } // ls = rs' ++ y && rs = x ++ rs', diff = |x| if (rs.size() > i) { unsigned diff = rs.size() - (i + 1); @@ -817,6 +821,10 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c unsigned diff = ls.size()-1-i; if (eq_unit(ls[diff], rs[0])) { bool same = true; + if (i == 0) { + m_overlap_rhs.insert(pair, true); + return true; + } // ls = x ++ rs' && rs = rs' ++ y, diff = |x| if (rs.size() > i) { for (unsigned j = 1; same && j <= i; ++j) { @@ -973,19 +981,21 @@ bool theory_seq::branch_quat_variable(eq const& e) { bool cond = false; - // xs and ys cannot align - if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys)) - cond = true; // xs = ys and xs and ys cannot align except the case xs = ys - else if (xs == ys) { + if (xs == ys) { expr_ref_vector xs1(m), xs2(m); xs1.reset(); xs1.append(xs.size()-1, xs.c_ptr()+1); xs2.reset(); xs2.append(xs.size()-1, xs.c_ptr()); - if (!can_align_from_lhs(xs2, ys) && !can_align_from_rhs(xs1, ys)) + if (xs1.empty() || xs2.empty()) + cond = true; + else if (!can_align_from_lhs(xs2, ys) && !can_align_from_rhs(xs1, ys)) cond = true; } + // xs and ys cannot align + else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys)) + cond = true; if (cond) { literal_vector lits; From e634f2987c17159c563603b3650c9aef77749ef3 Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Mon, 1 Jun 2020 18:55:48 +0100 Subject: [PATCH 02/16] Ensuring correct 'set' call is used when setting 'smtlib2_log' (#4487) Signed-off-by: Andrew V. Jones --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e9eb003bc..5729fd68e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6470,7 +6470,7 @@ class Solver(Z3PPObject): self.solver = solver Z3_solver_inc_ref(self.ctx.ref(), self.solver) if logFile is not None: - self.set("solver.smtlib2_log", logFile) + self.set("smtlib2_log", logFile) def __del__(self): if self.solver is not None and self.ctx.ref() is not None: From e079af9d0d372e3490e034ace4cb323dac7a7ec1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 1 Jun 2020 19:51:39 +0100 Subject: [PATCH 03/16] add context::internalize() API that takes multiple expressions at once (#4488) --- src/smt/smt_context.h | 12 +++++--- src/smt/smt_internalizer.cpp | 57 +++++++++++++++++++++++------------ src/smt/theory_array_full.cpp | 2 +- src/smt/theory_bv.cpp | 26 ++++++++-------- src/smt/theory_fpa.cpp | 12 ++------ 5 files changed, 60 insertions(+), 49 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index a766ca1a5..d3fd26446 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -741,7 +741,12 @@ namespace smt { bool should_internalize_rec(expr* e) const; - void top_sort_expr(expr * n, svector & sorted_exprs); + void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector & sorted_exprs); + + void internalize_rec(expr * n, bool gate_ctx); + + void internalize_deep(expr * n); + void internalize_deep(expr* const* n, unsigned num_exprs); void assert_default(expr * n, proof * pr); @@ -868,6 +873,7 @@ namespace smt { void ensure_internalized(expr* e); void internalize(expr * n, bool gate_ctx); + void internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx); void internalize(expr * n, bool gate_ctx, unsigned generation); @@ -906,10 +912,6 @@ namespace smt { public: - void internalize_rec(expr * n, bool gate_ctx); - - void internalize_deep(expr * n); - // helper function for trail void undo_th_case_split(literal l); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 55018d3f1..a19898452 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -152,11 +152,9 @@ namespace smt { return visited; } - void context::top_sort_expr(expr * n, svector & sorted_exprs) { - ts_todo.reset(); + void context::top_sort_expr(expr* const* exprs, unsigned num_exprs, svector & sorted_exprs) { tcolors.reset(); fcolors.reset(); - ts_todo.push_back(expr_bool_pair(n, true)); while (!ts_todo.empty()) { expr_bool_pair & p = ts_todo.back(); expr * curr = p.first; @@ -166,12 +164,14 @@ namespace smt { set_color(tcolors, fcolors, curr, gate_ctx, Grey); ts_visit_children(curr, gate_ctx, ts_todo); break; - case Grey: + case Grey: { SASSERT(ts_visit_children(curr, gate_ctx, ts_todo)); set_color(tcolors, fcolors, curr, gate_ctx, Black); - if (n != curr && !m.is_not(curr)) + auto end = exprs + num_exprs; + if (std::find(exprs, end, curr) == end && !m.is_not(curr) && should_internalize_rec(curr)) sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx)); break; + } case Black: ts_todo.pop_back(); break; @@ -189,23 +189,33 @@ namespace smt { to_app(e)->get_family_id() == null_family_id || to_app(e)->get_family_id() == m.get_basic_family_id(); } - - void context::internalize_deep(expr* n) { - if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) { - // if the expression is deep, then execute topological sort to avoid - // stack overflow. - // a caveat is that theory internalizers do rely on recursive descent so - // internalization over these follows top-down - TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m);); - svector sorted_exprs; - top_sort_expr(n, sorted_exprs); - TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); - for (auto & kv : sorted_exprs) { - expr* e = kv.first; - if (should_internalize_rec(e)) - internalize_rec(e, kv.second); + + void context::internalize_deep(expr* const* exprs, unsigned num_exprs) { + ts_todo.reset(); + for (unsigned i = 0; i < num_exprs; ++i) { + expr * n = exprs[i]; + if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) { + // if the expression is deep, then execute topological sort to avoid + // stack overflow. + // a caveat is that theory internalizers do rely on recursive descent so + // internalization over these follows top-down + TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m);); + ts_todo.push_back(expr_bool_pair(n, true)); } } + + svector sorted_exprs; + top_sort_expr(exprs, num_exprs, sorted_exprs); + TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); + for (auto & kv : sorted_exprs) { + expr* e = kv.first; + SASSERT(should_internalize_rec(e)); + internalize_rec(e, kv.second); + } + } + void context::internalize_deep(expr* n) { + expr * v[1] = { n }; + internalize_deep(v, 1); } /** @@ -343,6 +353,13 @@ namespace smt { internalize_rec(n, gate_ctx); } + void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) { + internalize_deep(exprs, num_exprs); + for (unsigned i = 0; i < num_exprs; ++i) { + internalize_rec(exprs[i], gate_ctx); + } + } + void context::internalize_rec(expr * n, bool gate_ctx) { TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";); TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m) << "\n";); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index c6e4c106d..8679c4dd9 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -398,7 +398,7 @@ namespace smt { if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){ return; } - if (!ctx.e_internalized(n)) ctx.internalize(n, false);; + ctx.ensure_internalized(n); enode* node = ctx.get_enode(n); if (is_select(n)) { enode * arg = ctx.get_enode(n->get_arg(0)); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6e96b0b01..4ec312541 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "smt/smt_model_generator.h" #include "util/stats.h" +#include "util/vector.h" #define WATCH_DISEQ 0 @@ -142,9 +143,7 @@ namespace smt { } void theory_bv::process_args(app * n) { - for (expr* arg : *n) { - ctx.internalize(arg, false); - } + ctx.internalize(n->get_args(), n->get_num_args(), false); } enode * theory_bv::mk_enode(app * n) { @@ -312,13 +311,16 @@ namespace smt { unsigned sz = bits.size(); SASSERT(get_bv_size(n) == sz); m_bits[v].reset(); + + ptr_vector bits_exprs; + for (unsigned i = 0; i < sz; ++i) + bits_exprs.push_back(bits.get(i)); + ctx.internalize(bits_exprs.c_ptr(), sz, true); + for (unsigned i = 0; i < sz; i++) { expr * bit = bits.get(i); - expr_ref s_bit(m); - simplify_bit(bit, s_bit); - ctx.internalize(s_bit, true); - literal l = ctx.get_literal(s_bit.get()); - TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(s_bit, m) << "\n";); + literal l = ctx.get_literal(bit); + TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(bit, m) << "\n";); add_bit(v, l); } find_wpos(v); @@ -983,9 +985,7 @@ namespace smt { } bool theory_bv::internalize_carry(app * n, bool gate_ctx) { - ctx.internalize(n->get_arg(0), true); - ctx.internalize(n->get_arg(1), true); - ctx.internalize(n->get_arg(2), true); + ctx.internalize(n->get_args(), 3, true); bool is_new_var = false; bool_var v; if (!ctx.b_internalized(n)) { @@ -1016,9 +1016,7 @@ namespace smt { } bool theory_bv::internalize_xor3(app * n, bool gate_ctx) { - ctx.internalize(n->get_arg(0), true); - ctx.internalize(n->get_arg(1), true); - ctx.internalize(n->get_arg(2), true); + ctx.internalize(n->get_args(), 3, true); bool is_new_var = false; bool_var v; if (!ctx.b_internalized(n)) { diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7c97dbc52..dadff152a 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -415,9 +415,7 @@ namespace smt { if (ctx.b_internalized(atom)) return true; - unsigned num_args = atom->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(atom->get_arg(i), false); + ctx.internalize(atom->get_args(), atom->get_num_args(), false); literal l(ctx.mk_bool_var(atom)); ctx.set_var_theory(l.var(), get_id()); @@ -436,9 +434,7 @@ namespace smt { SASSERT(term->get_family_id() == get_family_id()); SASSERT(!ctx.e_internalized(term)); - unsigned num_args = term->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(term->get_arg(i), false); + ctx.internalize(term->get_args(), term->get_num_args(), false); enode * e = ctx.mk_enode(term, false, false, true); @@ -697,9 +693,7 @@ namespace smt { } enode* theory_fpa::ensure_enode(expr* e) { - if (!ctx.e_internalized(e)) { - ctx.internalize(e, false); - } + ctx.ensure_internalized(e); enode* n = ctx.get_enode(e); ctx.mark_as_relevant(n); return n; From f395c8643cee2ab698462975a6476653a21cd1e9 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 Jun 2020 14:55:44 -0400 Subject: [PATCH 04/16] z3str3: construct proper cex for str.at model construction --- src/smt/theory_str_mc.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 8ebd34245..9da3f3876 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -725,7 +725,10 @@ namespace smt { v.init(&get_context()); rational pos_value; bool pos_exists = v.get_value(pos, pos_value); - ENSURE(pos_exists); + if (!pos_exists) { + cex = m.mk_or(m_autil.mk_ge(pos, mk_int(0)), m_autil.mk_le(pos, mk_int(0))); + return false; + } TRACE("str_fl", tout << "reduce str.at: base=" << mk_pp(base, m) << ", pos=" << pos_value.to_string() << std::endl;); if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) { // return the empty string From 8849cef4b7ece99d83cb1f353149743270f4626c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2020 15:33:52 -0700 Subject: [PATCH 05/16] add stub for equality propagation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 541e90397..8775785b3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2357,6 +2357,10 @@ public: return m_imp.bound_is_interesting(j, kind, v); } + void add_eq(lpvar u, lpvar v, lp::explanation const& e) { + m_imp.add_eq(u, v, e); + } + void consume(rational const& v, lp::constraint_index j) override { m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs); m_imp.m_explanation.add_pair(j, v); @@ -2419,6 +2423,26 @@ public: } } + void add_eq(lpvar u, lpvar v, lp::explanation const& e) { + theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations + theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form + enode* n1 = get_enode(uv); + enode* n2 = get_enode(vv); + if (n1 == n2) + return; + reset_evidence(); + for (auto const& ev : e) + set_evidence(ev.ci(), m_core, m_eqs); + justification* js = ctx().mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), n1, n2)); + + std::function fn = [&]() { return m.mk_eq(n1->get_owner(), n2->get_owner()); }; + scoped_trace_stream _sts(th, fn); + ctx().assign_eq(n1, n2, eq_justification(js)); + } + + literal_vector m_core2; void assign(literal lit, literal_vector const& core, svector const& eqs, vector const& params) { From 7343783efef12b657d451729cab40ef3bc0fffd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2020 15:40:02 -0700 Subject: [PATCH 06/16] finetune Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8775785b3..1f7094886 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2424,11 +2424,13 @@ public: } void add_eq(lpvar u, lpvar v, lp::explanation const& e) { + if (ctx().inconsistent()) + return; theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form enode* n1 = get_enode(uv); enode* n2 = get_enode(vv); - if (n1 == n2) + if (n1->get_root() == n2->get_root()) return; reset_evidence(); for (auto const& ev : e) @@ -2442,7 +2444,6 @@ public: ctx().assign_eq(n1, n2, eq_justification(js)); } - literal_vector m_core2; void assign(literal lit, literal_vector const& core, svector const& eqs, vector const& params) { From 2da7a8dd704b0e2d334ed686ea59a2ef4a48a0bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2020 20:12:11 -0700 Subject: [PATCH 07/16] fix #4491 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 471cb7643..77ded074b 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -345,7 +345,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp continue; eqs.push_back(m().mk_eq(arg, zero)); } - result = m().mk_and(eqs); + result = m().mk_or(eqs); return BR_REWRITE2; } From 48f07932f7b41cbf9b4d5f0f8eed72e9fd15b892 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 00:40:54 -0700 Subject: [PATCH 08/16] reset zero before resetting nlsat #4493b Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 1 + src/smt/theory_lra.cpp | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 047a5daff..97c8a0b3f 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -52,6 +52,7 @@ struct solver::imp { */ lbool check() { SASSERT(need_check()); + m_zero = nullptr; m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); m_zero = alloc(scoped_anum, am()); m_term_set.clear(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1f7094886..ebf37daa1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3389,14 +3389,14 @@ public: if (t.is_term()) { m_todo_terms.push_back(std::make_pair(t, rational::one())); - + TRACE("nl_value", tout << t.to_string() << "\n";); TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; lp().print_term(lp().get_term(t), tout) << "\n";); m_nla->am().set(r, 0); while (!m_todo_terms.empty()) { rational wcoeff = m_todo_terms.back().second; - t = m_todo_terms.back().first; + t = m_todo_terms.back().first; m_todo_terms.pop_back(); lp::lar_term const& term = lp().get_term(t); TRACE("nl_value", lp().print_term(term, tout) << "\n";); From 29ce22cfb18d3b8964148c9224b4f5387203e4ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 00:57:49 -0700 Subject: [PATCH 09/16] fix #4493, use standard model evaluation for variables that have not been regiestered with solver (e.g., they are non-shared and unconstrained) Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ebf37daa1..659b6cec2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3389,7 +3389,7 @@ public: if (t.is_term()) { m_todo_terms.push_back(std::make_pair(t, rational::one())); - TRACE("nl_value", tout << t.to_string() << "\n";); + TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";); TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; lp().print_term(lp().get_term(t), tout) << "\n";); @@ -3427,7 +3427,7 @@ public: model_value_proc * mk_value(enode * n, model_generator & mg) { theory_var v = n->get_th_var(get_id()); expr* o = n->get_owner(); - if (use_nra_model()) { + if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, *m_a1); if (a.is_int(o) && !m_nla->am().is_int(an)) { return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o))); From 742be835031e824c371f64d6392442150c923c65 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Jun 2020 01:00:06 -0700 Subject: [PATCH 10/16] Lpbounds (#4492) * remove inheritance from bound propagation Signed-off-by: Lev Nachmanson * less inheritance Signed-off-by: Lev Nachmanson * less inheritance Signed-off-by: Lev Nachmanson * fix the build Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/bound_analyzer_on_row.h | 10 +-- src/math/lp/lar_solver.cpp | 96 ---------------------------- src/math/lp/lar_solver.h | 97 ++++++++++++++++++++++++++--- src/math/lp/lp_bound_propagator.cpp | 54 ---------------- src/math/lp/lp_bound_propagator.h | 69 +++++++++++++++----- src/smt/theory_lra.cpp | 62 +++++++++--------- src/smt/theory_lra.h | 2 + src/test/lp/lp.cpp | 5 -- 9 files changed, 185 insertions(+), 211 deletions(-) delete mode 100644 src/math/lp/lp_bound_propagator.cpp diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 34892c7e0..f40ae6038 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(lp SOURCES binary_heap_priority_queue.cpp binary_heap_upair_queue.cpp - lp_bound_propagator.cpp core_solver_pretty_printer.cpp dense_matrix.cpp eta_matrix.cpp diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 409dda96d..353859e63 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -24,14 +24,13 @@ Revision History: #include "util/vector.h" #include "math/lp/implied_bound.h" -#include "math/lp/lp_bound_propagator.h" #include "math/lp/test_bound_analyzer.h" namespace lp { -template // C plays a role of a container +template // C plays a role of a container, B - lp_bound_propagator class bound_analyzer_on_row { const C& m_row; - lp_bound_propagator & m_bp; + B & m_bp; unsigned m_row_or_term_index; int m_column_of_u; // index of an unlimited from above monoid // -1 means that such a value is not found, -2 means that at least two of such monoids were found @@ -45,7 +44,7 @@ public : unsigned bj, // basis column for the row const numeric_pair& rs, unsigned row_or_term_index, - lp_bound_propagator & bp) + B & bp) : m_row(it), m_bp(bp), @@ -55,11 +54,12 @@ public : m_rs(rs) {} + static void analyze_row(const C & row, unsigned bj, // basis column for the row const numeric_pair& rs, unsigned row_or_term_index, - lp_bound_propagator & bp) { + B & bp) { bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp); a.analyze(); // TBD: a.analyze_eq(); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 83a8619e3..f479b4d33 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -135,23 +135,6 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, return kind == be.kind() && rs_of_evidence == be.m_bound; } - -void lar_solver::analyze_new_bounds_on_row( - unsigned row_index, - lp_bound_propagator & bp) { - lp_assert(!use_tableau()); - unsigned j = m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row - - - bound_analyzer_on_row>::analyze_row( - m_mpq_lar_core_solver.get_pivot_row(), - j, - zero_of_type>(), - row_index, - bp - ); -// ra_pos.analyze(); -} bool lar_solver::row_has_a_big_num(unsigned i) const { for (const auto& c : A_r().m_rows[i]) { @@ -161,23 +144,6 @@ bool lar_solver::row_has_a_big_num(unsigned i) const { return false; } -void lar_solver::analyze_new_bounds_on_row_tableau( - unsigned row_index, - lp_bound_propagator & bp ) { - - if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation - || row_has_a_big_num(row_index)) - return; - lp_assert(use_tableau()); - - bound_analyzer_on_row>::analyze_row(A_r().m_rows[row_index], - null_ci, - zero_of_type>(), - row_index, - bp - ); -} - void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { // todo : create a map from term basic vars to the rows where they are used @@ -190,16 +156,6 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); } } - -void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) { - if (use_tableau()) { - analyze_new_bounds_on_row_tableau(i, bp); - } else { - m_mpq_lar_core_solver.calculate_pivot_row(i); - substitute_basis_var_in_terms_for_row(i); - analyze_new_bounds_on_row(i, bp); - } -} unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { if (!tv::is_term(j)) { @@ -213,64 +169,12 @@ unsigned lar_solver::map_term_index_to_column_index(unsigned j) const { SASSERT(tv::is_term(j)); return m_var_register.external_to_local(j); } - -void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) { - lp_assert(false); // not implemented -} - - -void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) { - unsigned i = ib.m_row_or_term_index; - int bound_sign = ib.m_is_lower_bound? 1: -1; - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; - unsigned bound_j = ib.m_j; - if (tv::is_term(bound_j)) { - bound_j = m_var_register.external_to_local(bound_j); - } - for (auto const& r : A_r().m_rows[i]) { - unsigned j = r.var(); - if (j == bound_j) continue; - mpq const& a = r.coeff(); - int a_sign = is_pos(a)? 1: -1; - int sign = j_sign * a_sign; - const ul_pair & ul = m_columns_to_ul_pairs[j]; - auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); - lp_assert(is_valid(witness)); - bp.consume(a, witness); - } - // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); -} // here i is just the term index bool lar_solver::term_is_used_as_row(unsigned i) const { SASSERT(i < m_terms.size()); return m_var_register.external_is_used(tv::mask_term(i)); } - -void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) { - for (unsigned i = 0; i < m_terms.size(); i++) { - if (term_is_used_as_row(i)) - continue; // this term is used a left side of a constraint, - // it was processed as a touched row if needed - propagate_bounds_on_a_term(*m_terms[i], bp, i); - } -} - -// goes over touched rows and tries to induce bounds -void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { - if (!use_tableau()) - return; // todo: consider to remove the restriction - - for (unsigned i : m_rows_with_changed_bounds) { - calculate_implied_bounds_for_row(i, bp); - if (settings().get_cancel_flag()) - return; - } - m_rows_with_changed_bounds.clear(); - if (!use_tableau()) { - propagate_bounds_on_terms(bp); - } -} lp_status lar_solver::get_status() const { return m_status; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 6216fafe2..82285a5e6 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -41,8 +41,8 @@ #include "math/lp/conversion_helper.h" #include "math/lp/int_solver.h" #include "math/lp/nra_solver.h" -#include "math/lp/lp_bound_propagator.h" #include "math/lp/lp_types.h" +#include "math/lp/lp_bound_propagator.h" namespace lp { @@ -161,15 +161,53 @@ class lar_solver : public column_namer { bool use_lu() const; bool sizes_are_correct() const; bool implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const; + template void analyze_new_bounds_on_row( unsigned row_index, - lp_bound_propagator & bp); + lp_bound_propagator& bp) { + lp_assert(!use_tableau()); + unsigned j = m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row + bound_analyzer_on_row, lp_bound_propagator>::analyze_row( + m_mpq_lar_core_solver.get_pivot_row(), + j, + zero_of_type>(), + row_index, + bp); + } + + template void analyze_new_bounds_on_row_tableau( unsigned row_index, - lp_bound_propagator & bp); + lp_bound_propagator & bp ) { + + if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation + || row_has_a_big_num(row_index)) + return; + lp_assert(use_tableau()); + + bound_analyzer_on_row, lp_bound_propagator>::analyze_row(A_r().m_rows[row_index], + null_ci, + zero_of_type>(), + row_index, + bp + ); + } + void substitute_basis_var_in_terms_for_row(unsigned i); - void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp); - void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset); + template + void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) { + if (use_tableau()) { + analyze_new_bounds_on_row_tableau(i, bp); + } else { + m_mpq_lar_core_solver.calculate_pivot_row(i); + substitute_basis_var_in_terms_for_row(i); + analyze_new_bounds_on_row(i, bp); + } + } + template + void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) { + NOT_IMPLEMENTED_YET(); + } static void clean_popped_elements(unsigned n, u_set& set); static void shrink_inf_set_after_pop(unsigned n, u_set & set); bool maximize_term_on_tableau(const lar_term & term, @@ -282,12 +320,55 @@ public: void get_infeasibility_explanation(explanation &) const; inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } - void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp); + template + void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) { + unsigned i = ib.m_row_or_term_index; + int bound_sign = ib.m_is_lower_bound? 1: -1; + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; + unsigned bound_j = ib.m_j; + if (tv::is_term(bound_j)) { + bound_j = m_var_register.external_to_local(bound_j); + } + for (auto const& r : A_r().m_rows[i]) { + unsigned j = r.var(); + if (j == bound_j) continue; + mpq const& a = r.coeff(); + int a_sign = is_pos(a)? 1: -1; + int sign = j_sign * a_sign; + const ul_pair & ul = m_columns_to_ul_pairs[j]; + auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); + lp_assert(is_valid(witness)); + bp.consume(a, witness); + } + } + // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); void activate(constraint_index ci); void random_update(unsigned sz, var_index const * vars); - void propagate_bounds_on_terms(lp_bound_propagator & bp); - void propagate_bounds_for_touched_rows(lp_bound_propagator & bp); + template + void propagate_bounds_on_terms(lp_bound_propagator & bp) { + for (unsigned i = 0; i < m_terms.size(); i++) { + if (term_is_used_as_row(i)) + continue; // this term is used a left side of a constraint, + // it was processed as a touched row if needed + propagate_bounds_on_a_term(*m_terms[i], bp, i); + } + } + template + void propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { + if (!use_tableau()) + return; // todo: consider to remove the restriction + + for (unsigned i : m_rows_with_changed_bounds) { + calculate_implied_bounds_for_row(i, bp); + if (settings().get_cancel_flag()) + return; + } + m_rows_with_changed_bounds.clear(); + if (!use_tableau()) { + propagate_bounds_on_terms(bp); + } + } bool is_fixed(column_index const& j) const { return column_is_fixed(j); } inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } bool external_is_used(unsigned) const; diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp deleted file mode 100644 index c07a60adb..000000000 --- a/src/math/lp/lp_bound_propagator.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson -*/ -#include "math/lp/lar_solver.h" -namespace lp { -lp_bound_propagator::lp_bound_propagator(lar_solver & ls): - m_lar_solver(ls) {} -column_type lp_bound_propagator::get_column_type(unsigned j) const { - return m_lar_solver.get_column_type(j); -} -const impq & lp_bound_propagator::get_lower_bound(unsigned j) const { - return m_lar_solver.get_lower_bound(j); -} -const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { - return m_lar_solver.get_upper_bound(j); -} -void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { - j = m_lar_solver.adjust_column_index_to_term_index(j); - - lconstraint_kind kind = is_low? GE : LE; - if (strict) - kind = static_cast(kind / 2); - - if (!bound_is_interesting(j, kind, v)) - return; - unsigned k; // index to ibounds - if (is_low) { - if (try_get_value(m_improved_lower_bounds, j, k)) { - auto & found_bound = m_ibounds[k]; - if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); - } - } else { - m_improved_lower_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); - } - } else { // the upper bound case - if (try_get_value(m_improved_upper_bounds, j, k)) { - auto & found_bound = m_ibounds[k]; - if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); - } - } else { - m_improved_upper_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); - } - } -} -} diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9b67162a9..9049b17b2 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -5,24 +5,65 @@ #pragma once #include "math/lp/lp_settings.h" namespace lp { -class lar_solver; +template class lp_bound_propagator { std::unordered_map m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_upper_bounds; - lar_solver & m_lar_solver; + T& m_imp; public: vector m_ibounds; -public: - lp_bound_propagator(lar_solver & ls); - column_type get_column_type(unsigned) const; - const impq & get_lower_bound(unsigned) const; - const impq & get_upper_bound(unsigned) const; - void try_add_bound(mpq const & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict); - void try_add_eq(lpvar x, lpvar y, unsigned row_or_term_index) {} // TBD - virtual bool bound_is_interesting(unsigned vi, - lp::lconstraint_kind kind, - const rational & bval) {return true;} - unsigned number_of_found_bounds() const { return m_ibounds.size(); } - virtual void consume(mpq const& v, lp::constraint_index j) = 0; + lp_bound_propagator(T& imp): m_imp(imp) {} + column_type get_column_type(unsigned j) const { + return m_imp.lp().get_column_type(j); + } + + const impq & get_lower_bound(unsigned j) const { + return m_imp.lp().get_lower_bound(j); + } + + const impq & get_upper_bound(unsigned j) const { + return m_imp.lp().get_upper_bound(j); + } + + void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { + j = m_imp.lp().adjust_column_index_to_term_index(j); + + lconstraint_kind kind = is_low? GE : LE; + if (strict) + kind = static_cast(kind / 2); + + if (!m_imp.bound_is_interesting(j, kind, v)) + return; + unsigned k; // index to ibounds + if (is_low) { + if (try_get_value(m_improved_lower_bounds, j, k)) { + auto & found_bound = m_ibounds[k]; + if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { + found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } else { + m_improved_lower_bounds[j] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + } + } else { // the upper bound case + if (try_get_value(m_improved_upper_bounds, j, k)) { + auto & found_bound = m_ibounds[k]; + if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { + found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } else { + m_improved_upper_bounds[j] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); + TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + } + } + } + + void consume(const mpq& a, constraint_index ci) { + m_imp.consume(a, ci); + } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 659b6cec2..5a966a324 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -328,9 +328,6 @@ class theory_lra::imp { enode* get_enode(expr* e) const { return ctx().get_enode(e); } expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } - lp::lar_solver& lp(){ return *m_solver.get(); } - const lp::lar_solver& lp() const { return *m_solver.get(); } - void init_solver() { if (m_solver) return; @@ -969,6 +966,9 @@ public: std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc()); } + lp::lar_solver& lp(){ return *m_solver.get(); } + const lp::lar_solver& lp() const { return *m_solver.get(); } + void init() { if (m_solver) return; @@ -2311,10 +2311,34 @@ public: // } // } + bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) { + theory_var v = lp().local_to_external(vi); + if (v == null_theory_var) { + return false; + } + if (m_bounds.size() <= static_cast(v) || m_unassigned_bounds[v] == 0) { + return false; + } + for (lp_api::bound* b : m_bounds[v]) { + if (ctx().get_assignment(b->get_bv()) == l_undef && + null_literal != is_bound_implied(kind, bval, *b)) { + return true; + } + } + return false; + } + + void consume(rational const& v, lp::constraint_index j) { + set_evidence(j, m_core, m_eqs); + m_explanation.add_pair(j, v); + } + + void propagate_bounds_with_lp_solver() { if (!should_propagate()) return; - local_bound_propagator bp(*this); + + lp::lp_bound_propagator bp(*this); lp().propagate_bounds_for_touched_rows(bp); @@ -2348,26 +2372,6 @@ public: } return false; } - - struct local_bound_propagator: public lp::lp_bound_propagator { - imp & m_imp; - local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {} - - bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) override { - return m_imp.bound_is_interesting(j, kind, v); - } - - void add_eq(lpvar u, lpvar v, lp::explanation const& e) { - m_imp.add_eq(u, v, e); - } - - void consume(rational const& v, lp::constraint_index j) override { - m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs); - m_imp.m_explanation.add_pair(j, v); - } - }; - - void propagate_lp_solver_bound(lp::implied_bound& be) { lpvar vi = be.m_j; theory_var v = lp().local_to_external(vi); @@ -2400,7 +2404,7 @@ public: first = false; reset_evidence(); m_explanation.clear(); - local_bound_propagator bp(*this); + lp::lp_bound_propagator bp(*this); lp().explain_implied_bound(be, bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); @@ -4024,7 +4028,9 @@ theory_var theory_lra::add_objective(app* term) { expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) { return m_imp->mk_ge(fm, v, val); } - - - } +template class lp::lp_bound_propagator; +template void lp::lar_solver::propagate_bounds_for_touched_rows(lp::lp_bound_propagator&); +template void lp::lar_solver::explain_implied_bound(lp::implied_bound&, lp::lp_bound_propagator&); +template void lp::lar_solver::calculate_implied_bounds_for_row(unsigned int, lp::lp_bound_propagator&); +template void lp::lar_solver::propagate_bounds_on_terms(lp::lp_bound_propagator&); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index c6e8dbfe7..2522f0e79 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -24,7 +24,9 @@ Revision History: namespace smt { class theory_lra : public theory, public theory_opt { + public: class imp; + private: imp* m_imp; public: diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ae843d59b..9d24d2787 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -313,11 +313,6 @@ void test_cn() { namespace lp { unsigned seed = 1; -class my_bound_propagator : public lp_bound_propagator { -public: - my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls) {} - void consume(mpq const& v, lp::constraint_index j) override {} -}; random_gen g_rand; static unsigned my_random() { From b9ecf2512f2e4016384fa2a911c57802214d4e60 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 2 Jun 2020 15:26:57 +0100 Subject: [PATCH 11/16] more tweaks to BV internalizer & remove dead code --- src/smt/theory_bv.cpp | 40 +++++++++++----------------------------- src/smt/theory_bv.h | 7 ++----- src/smt/theory_fpa.cpp | 2 +- 3 files changed, 14 insertions(+), 35 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 4ec312541..7378b291f 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -23,7 +23,6 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "smt/smt_model_generator.h" #include "util/stats.h" -#include "util/vector.h" #define WATCH_DISEQ 0 @@ -53,10 +52,15 @@ namespace smt { literal_vector & bits = m_bits[v]; TRACE("bv", tout << "v" << v << "\n";); bits.reset(); + m_bits_expr.reset(); + for (unsigned i = 0; i < bv_size; i++) { - app * bit = mk_bit2bool(owner, i); - ctx.internalize(bit, true); - bool_var b = ctx.get_bool_var(bit); + m_bits_expr.push_back(mk_bit2bool(owner, i)); + } + ctx.internalize(m_bits_expr.c_ptr(), bv_size, true); + + for (unsigned i = 0; i < bv_size; i++) { + bool_var b = ctx.get_bool_var(m_bits_expr[i]); bits.push_back(literal(b)); if (is_relevant && !ctx.is_relevant(b)) { ctx.mark_as_relevant(b); @@ -311,11 +315,11 @@ namespace smt { unsigned sz = bits.size(); SASSERT(get_bv_size(n) == sz); m_bits[v].reset(); + m_bits_expr.reset(); - ptr_vector bits_exprs; for (unsigned i = 0; i < sz; ++i) - bits_exprs.push_back(bits.get(i)); - ctx.internalize(bits_exprs.c_ptr(), sz, true); + m_bits_expr.push_back(bits.get(i)); + ctx.internalize(m_bits_expr.c_ptr(), sz, true); for (unsigned i = 0; i < sz; i++) { expr * bit = bits.get(i); @@ -742,28 +746,6 @@ namespace smt { TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \ } - -#define MK_BINARY_COND(NAME, BLAST_OP) \ - void theory_bv::NAME(app * n) { \ - SASSERT(!ctx.e_internalized(n)); \ - SASSERT(n->get_num_args() == 2); \ - process_args(n); \ - enode * e = mk_enode(n); \ - expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); \ - expr_ref cond(m), s_cond(m); \ - get_arg_bits(e, 0, arg1_bits); \ - get_arg_bits(e, 1, arg2_bits); \ - SASSERT(arg1_bits.size() == arg2_bits.size()); \ - m_bb.BLAST_OP(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, cond); \ - init_bits(e, bits); \ - simplify_bit(cond, s_cond); \ - ctx.internalize(s_cond, true); \ - literal l(ctx.get_literal(s_cond)); \ - ctx.mark_as_relevant(l); \ - ctx.mk_th_axiom(get_id(), 1, &l); \ - TRACE("bv", tout << mk_pp(cond, m) << "\n"; tout << l << "\n";); \ - } - void theory_bv::internalize_sub(app *n) { SASSERT(!ctx.e_internalized(n)); SASSERT(n->get_num_args() == 2); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 95fcd39fd..bf6a0425f 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef THEORY_BV_H_ -#define THEORY_BV_H_ +#pragma once #include "ast/rewriter/bit_blaster/bit_blaster.h" #include "util/trail.h" @@ -112,6 +111,7 @@ namespace smt { th_trail_stack m_trail_stack; th_union_find m_find; vector m_bits; // per var, the bits of a given variable. + ptr_vector m_bits_expr; svector m_wpos; // per var, watch position for fixed variable detection. vector m_zero_one_bits; // per var, see comment in the struct zero_one_bit bool_var2atom m_bool_var2atom; @@ -278,6 +278,3 @@ namespace smt { bool check_zero_one_bits(theory_var v); }; }; - -#endif /* THEORY_BV_H_ */ - diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index dadff152a..d3793b707 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -472,7 +472,7 @@ namespace smt { SASSERT(m_fpa_util.is_float(n->get_owner()) || m_fpa_util.is_rm(n->get_owner())); SASSERT(n->get_owner()->get_decl()->get_range() == s); - app_ref owner(n->get_owner(), m); + app * owner = n->get_owner(); if (!is_attached_to_var(n)) { attach_new_th_var(n); From 023b630b5a2b251346d5ce2ac47e692cd8edf820 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 2 Jun 2020 16:36:38 +0100 Subject: [PATCH 12/16] remove unused class fields in BV theory --- src/smt/theory_bv.cpp | 11 +++++------ src/smt/theory_bv.h | 8 ++++---- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 7378b291f..853961912 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -192,7 +192,7 @@ namespace smt { for (literal lit : bits) { expr_ref l(get_manager()); ctx.literal2expr(lit, l); - r.push_back(l); + r.push_back(std::move(l)); } } @@ -315,11 +315,8 @@ namespace smt { unsigned sz = bits.size(); SASSERT(get_bv_size(n) == sz); m_bits[v].reset(); - m_bits_expr.reset(); - for (unsigned i = 0; i < sz; ++i) - m_bits_expr.push_back(bits.get(i)); - ctx.internalize(m_bits_expr.c_ptr(), sz, true); + ctx.internalize(bits.c_ptr(), sz, true); for (unsigned i = 0; i < sz; i++) { expr * bit = bits.get(i); @@ -1163,7 +1160,7 @@ namespace smt { ctx.internalize(diff, true); literal arg = ctx.get_literal(diff); lits.push_back(arg); - exprs.push_back(diff); + exprs.push_back(std::move(diff)); } m_stats.m_num_diseq_dynamic++; if (m.has_trace_stream()) { @@ -1427,7 +1424,9 @@ namespace smt { m_find(*this), m_approximates_large_bvs(false) { memset(m_eq_activity, 0, sizeof(m_eq_activity)); +#if WATCH_DISEQ memset(m_diseq_activity, 0, sizeof(m_diseq_activity)); +#endif } theory_bv::~theory_bv() { diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index bf6a0425f..8d01071ff 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -124,11 +124,11 @@ namespace smt { value2var m_fixed_var_table; unsigned char m_eq_activity[256]; - unsigned char m_diseq_activity[256]; + //unsigned char m_diseq_activity[256]; svector> m_replay_diseq; - vector>> m_diseq_watch; - svector m_diseq_watch_trail; - unsigned_vector m_diseq_watch_lim; + //vector>> m_diseq_watch; + //svector m_diseq_watch_trail; + //unsigned_vector m_diseq_watch_lim; literal_vector m_tmp_literals; svector m_prop_queue; From 4ef480e2a59f682426017ac985309d1a415c3050 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 12:52:42 -0700 Subject: [PATCH 13/16] add op cache Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 26 +++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 35 +++++++++++++++++++++++++++++++ src/qe/qsat.cpp | 13 ++++++++---- src/smt/smt_case_split_queue.cpp | 4 ++-- src/smt/smt_context.cpp | 5 ++++- 5 files changed, 76 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 955d6f34b..ea0cb3156 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3849,3 +3849,29 @@ bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, } return true; } + +seq_rewriter::op_cache::op_cache(ast_manager& m): + m(m), + m_trail(m) +{} + +expr* seq_rewriter::op_cache::find(decl_kind op, expr* a, expr* b) { + op_entry e(op, a, b, nullptr); + m_table.find(e); + return e.r; +} + +void seq_rewriter::op_cache::insert(decl_kind op, expr* a, expr* b, expr* r) { + cleanup(); + if (a) m_trail.push_back(a); + if (b) m_trail.push_back(b); + if (r) m_trail.push_back(r); + m_table.insert(op_entry(op, a, b, r)); +} + +void seq_rewriter::op_cache::cleanup() { + if (m_table.size() >= m_max_cache_size) { + m_trail.reset(); + m_table.reset(); + } +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5519ee0fc..74f06f5f8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -127,6 +127,41 @@ class seq_rewriter { unknown_c }; + + class op_cache { + struct op_entry { + decl_kind k; + expr* a, *b, *r; + op_entry(decl_kind k, expr* a, expr* b, expr* r): k(k), a(a), b(b), r(r) {} + op_entry():k(0), a(nullptr), b(nullptr), r(nullptr) {} + }; + + struct hash_entry { + unsigned operator()(op_entry const& e) const { + return mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0); + } + }; + + struct eq_entry { + bool operator()(op_entry const& a, op_entry const& b) const { + return a.k == b.k && a.a == b.a && a.b == b.b; + } + }; + + typedef hashtable op_table; + + ast_manager& m; + unsigned m_max_cache_size { 10000 }; + expr_ref_vector m_trail; + op_table m_table; + void cleanup(); + + public: + op_cache(ast_manager& m); + expr* find(decl_kind op, expr* a, expr* b); + void insert(decl_kind op, expr* a, expr* b, expr* r); + }; + length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) { return compare_lengths(as.size(), as.c_ptr(), bs.size(), bs.c_ptr()); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 351363f0b..248344c21 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -563,7 +563,11 @@ namespace qe { m_solver->collect_statistics(st); } void reset_statistics() { - init(); + clear(); + } + void collect_statistics(statistics& st) { + if (m_solver) + m_solver->collect_statistics(st); } void clear() { @@ -735,6 +739,7 @@ namespace qe { m_fa.init(); m_ex.init(); } + /** \brief create a quantifier prefix formula. @@ -1334,8 +1339,8 @@ namespace qe { void collect_statistics(statistics & st) const override { st.copy(m_st); - m_fa.s().collect_statistics(st); - m_ex.s().collect_statistics(st); + m_fa.collect_statistics(st); + m_ex.collect_statistics(st); m_pred_abs.collect_statistics(st); st.update("qsat num rounds", m_stats.m_num_rounds); m_pred_abs.collect_statistics(st); @@ -1348,7 +1353,7 @@ namespace qe { } void cleanup() override { - reset(); + clear(); } void set_logic(symbol const & l) override { diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index ddb66ec33..d31f09d06 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1252,12 +1252,12 @@ namespace { namespace smt { case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) { if (ctx.relevancy_lvl() < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4f90bbcef..10b904c35 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -47,7 +47,7 @@ namespace smt { m_fparams(p), m_params(_p), m_setup(*this, p), - m_relevancy_lvl(p.m_relevancy_lvl), + m_relevancy_lvl(m_fparams.m_relevancy_lvl), m_asserted_formulas(m, p, _p), m_rewriter(m), m_qmanager(alloc(quantifier_manager, *this, p, _p)), @@ -95,6 +95,9 @@ namespace smt { m_last_search_failure(UNKNOWN), m_searching(false) { + std::cout << "create: " << m_fparams.m_relevancy_lvl << "\n"; + SASSERT(m_fparams.m_relevancy_lvl != 0); + SASSERT(m_scope_lvl == 0); SASSERT(m_base_lvl == 0); SASSERT(m_search_lvl == 0); From 320cd81140c69bab5dc080c5dedabcb82090db62 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 13:00:55 -0700 Subject: [PATCH 14/16] fix #4476 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 10b904c35..801d0a3e3 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -95,9 +95,6 @@ namespace smt { m_last_search_failure(UNKNOWN), m_searching(false) { - std::cout << "create: " << m_fparams.m_relevancy_lvl << "\n"; - SASSERT(m_fparams.m_relevancy_lvl != 0); - SASSERT(m_scope_lvl == 0); SASSERT(m_base_lvl == 0); SASSERT(m_search_lvl == 0); From e388055a338bbe9c4b76856be055e22dbae86717 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 13:13:32 -0700 Subject: [PATCH 15/16] connecting op-cache Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.h | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 74f06f5f8..83a662d56 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -114,19 +114,6 @@ public: \brief Cheap rewrite rules for seq constraints */ class seq_rewriter { - seq_util m_util; - arith_util m_autil; - re2automaton m_re2aut; - expr_ref_vector m_es, m_lhs, m_rhs; - bool m_coalesce_chars; - - enum length_comparison { - shorter_c, - longer_c, - same_length_c, - unknown_c - }; - class op_cache { struct op_entry { @@ -162,6 +149,22 @@ class seq_rewriter { void insert(decl_kind op, expr* a, expr* b, expr* r); }; + seq_util m_util; + arith_util m_autil; + re2automaton m_re2aut; + op_cache m_op_cache; + expr_ref_vector m_es, m_lhs, m_rhs; + bool m_coalesce_chars; + + enum length_comparison { + shorter_c, + longer_c, + same_length_c, + unknown_c + }; + + + length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) { return compare_lengths(as.size(), as.c_ptr(), bs.size(), bs.c_ptr()); } @@ -266,7 +269,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) { + m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) { } ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } From bfb5c95b9aa8d2d366160a89c27c12abe46c288c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 13:30:18 -0700 Subject: [PATCH 16/16] use op-cache for is-nullable Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 23 ++++++++++++++++------- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.h | 1 + 3 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ea0cb3156..61824f615 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2151,6 +2151,15 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) { return re_and(cond, re_with_empty); } +expr_ref seq_rewriter::is_nullable_rec(expr* r) { + expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr), m()); + if (!result) { + result = is_nullable(r); + m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result); + } + return result; +} + expr_ref seq_rewriter::is_nullable(expr* r) { SASSERT(m_util.is_re(r)); expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr; @@ -2158,14 +2167,14 @@ expr_ref seq_rewriter::is_nullable(expr* r) { expr_ref result(m()); if (re().is_concat(r, r1, r2) || re().is_intersection(r, r1, r2)) { - result = mk_and(m(), is_nullable(r1), is_nullable(r2)); + result = mk_and(m(), is_nullable_rec(r1), is_nullable_rec(r2)); } else if (re().is_union(r, r1, r2)) { - result = mk_or(m(), is_nullable(r1), is_nullable(r2)); + result = mk_or(m(), is_nullable_rec(r1), is_nullable_rec(r2)); } else if (re().is_diff(r, r1, r2)) { - result = mk_not(m(), is_nullable(r2)); - result = mk_and(m(), is_nullable(r1), result); + result = mk_not(m(), is_nullable_rec(r2)); + result = mk_and(m(), is_nullable_rec(r1), result); } else if (re().is_star(r) || re().is_opt(r) || @@ -2184,10 +2193,10 @@ expr_ref seq_rewriter::is_nullable(expr* r) { (re().is_loop(r, r1, lo) && lo > 0) || (re().is_loop(r, r1, lo, hi) && lo > 0) || (re().is_reverse(r, r1))) { - result = is_nullable(r1); + result = is_nullable_rec(r1); } else if (re().is_complement(r, r1)) { - result = mk_not(m(), is_nullable(r1)); + result = mk_not(m(), is_nullable_rec(r1)); } else if (re().is_to_re(r, r1)) { sort* seq_sort = nullptr; @@ -2196,7 +2205,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) { result = m().mk_eq(emptystr, r1); } else if (m().is_ite(r, cond, r1, r2)) { - result = m().mk_ite(cond, is_nullable(r1), is_nullable(r2)); + result = m().mk_ite(cond, is_nullable_rec(r1), is_nullable_rec(r2)); } else { sort* seq_sort = nullptr; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 83a662d56..873f88581 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -311,6 +311,7 @@ public: void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs); expr_ref is_nullable(expr* r); + expr_ref is_nullable_rec(expr* r); bool has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 544628597..17438a054 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -108,6 +108,7 @@ enum seq_op_kind { _OP_STRING_STRIDOF, _OP_REGEXP_EMPTY, _OP_REGEXP_FULL_CHAR, + _OP_RE_IS_NULLABLE, _OP_SEQ_SKOLEM, LAST_SEQ_OP };