From 8718c1c99f8946e43ce84e246f0000f909e52c6d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 17 Feb 2016 19:14:02 +0000 Subject: [PATCH 1/4] bv_bounds: simplify negated expressions as well --- src/tactic/bv/bv_bounds_tactic.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 96115bad6..5a37d166a 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -49,6 +49,7 @@ struct interval { SASSERT(sz == b.sz); return l == b.l && h == b.h; } + bool operator!=(const interval& b) const { return !(*this == b); } bool implies(const interval& b) const { if (b.is_full()) @@ -182,6 +183,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { v = lhs; return true; } + } else if (m.is_not(e, lhs)) { + if (is_bound(lhs, v, b)) + return b.negate(b); } return false; } @@ -223,9 +227,7 @@ public: if (m_bound->find(t1, ctx)) { if (!b.intersect(ctx, intr)) { result = m.mk_false(); - } else if (intr == b) { - // no improvement in range; do nothing - } else if (intr.l == intr.h) { + } else if (intr.l == intr.h && intr != b) { result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); } else if (ctx.implies(b)) { result = m.mk_true(); From 67958efed25de9e39e3e2919331cbb289dd023d6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Feb 2016 21:20:39 -0800 Subject: [PATCH 2/4] add fixed length heuristic Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 55 ++++++++++++++++++++++++++++++++++++++++++ src/smt/theory_seq.h | 16 ++++++++++++ 2 files changed, 71 insertions(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e11ca806a..11bf2b678 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -233,6 +233,11 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>solve_nqs\n";); return FC_CONTINUE; } + if (fixed_length()) { + ++m_stats.m_fixed_length; + TRACE("seq", tout << ">>fixed_length\n";); + return FC_CONTINUE; + } if (branch_variable()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); @@ -430,6 +435,7 @@ lbool theory_seq::assume_equality(expr* l, expr* r) { return l_undef; } + bool theory_seq::propagate_length_coherence(expr* e) { expr_ref head(m), tail(m); rational lo, hi; @@ -509,6 +515,54 @@ bool theory_seq::check_length_coherence() { return false; } +bool theory_seq::fixed_length() { + obj_hashtable::iterator it = m_length.begin(), end = m_length.end(); + bool found = false; + for (; it != end; ++it) { + if (fixed_length(*it)) { + found = true; + } + } + return found; +} + +bool theory_seq::fixed_length(expr* e) { + rational lo, hi; + if (!(is_var(e) && lower_bound(e, lo) && upper_bound(e, hi) && lo == hi && lo.is_unsigned() && lo.is_pos())) { + return false; + } + if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) || + is_skolem(m_indexof_left, e) || is_skolem(m_indexof_right, e) || + is_skolem(m_contains_left, e) || is_skolem(m_contains_right, e) || + m_fixed.contains(e)) { + return false; + } + + context& ctx = get_context(); + + m_trail_stack.push(insert_obj_trail(m_fixed, e)); + m_fixed.insert(e); + + + unsigned _lo = lo.get_unsigned(); + expr_ref seq(e, m), head(m), tail(m); + expr_ref_vector elems(m); + + for (unsigned j = 0; j < _lo; ++j) { + mk_decompose(seq, head, tail); + elems.push_back(head); + seq = tail; + } + seq = mk_concat(elems.size(), elems.c_ptr()); + TRACE("seq", tout << "Fixed: " << mk_pp(e, m) << " " << lo << "\n";); + add_axiom(~mk_eq(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true), false), mk_seq_eq(seq, e)); + if (!ctx.at_base_level()) { + m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, e))); + } + return true; +} + + /* lit => s != "" */ @@ -1778,6 +1832,7 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq solve =", m_stats.m_solve_eqs); st.update("seq add axiom", m_stats.m_add_axiom); st.update("seq extensionality", m_stats.m_extensionality); + st.update("seq fixed length", m_stats.m_fixed_length); } void theory_seq::init_model(expr_ref_vector const& es) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index a28458e02..3aedac835 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -208,6 +208,17 @@ namespace smt { } }; + class replay_fixed_length : public apply { + expr_ref m_e; + public: + replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {} + virtual ~replay_fixed_length() {} + virtual void operator()(theory_seq& th) { + th.fixed_length(m_e); + m_e.reset(); + } + }; + class replay_axiom : public apply { expr_ref m_e; public: @@ -251,6 +262,7 @@ namespace smt { unsigned m_solve_eqs; unsigned m_add_axiom; unsigned m_extensionality; + unsigned m_fixed_length; }; ast_manager& m; dependency_manager m_dm; @@ -292,6 +304,8 @@ namespace smt { bool m_new_propagation; // new propagation to core re2automaton m_mk_aut; + obj_hashtable m_fixed; // string variables that are fixed length. + virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); @@ -322,6 +336,8 @@ namespace smt { bool is_solved(); bool check_length_coherence(); bool check_length_coherence(expr* e); + bool fixed_length(); + bool fixed_length(expr* e); bool propagate_length_coherence(expr* e); bool check_extensionality(); From d32b4c71d12dbdbf26887de7e4018e5dcaa1ebf2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 18 Feb 2016 15:53:11 +0000 Subject: [PATCH 3/4] [bv_bounds] introduce a tight bit in intervals to denote they are tight (over and under approx) use this to ensure certain transformations remain sound --- src/tactic/bv/bv_bounds_tactic.cpp | 72 +++++++++++++++++-------- src/tactic/core/ctx_simplify_tactic.cpp | 27 ++++++---- src/tactic/core/ctx_simplify_tactic.h | 2 +- 3 files changed, 69 insertions(+), 32 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 5a37d166a..d9703990c 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -32,14 +32,16 @@ struct interval { // l > h: [0, h] U [l, UMAX_INT] rational l, h; unsigned sz; + bool tight; - explicit interval() : l(0), h(0), sz(0) {} - interval(const rational& l, const rational& h, unsigned sz) : l(l), h(h), sz(sz) { + explicit interval() : l(0), h(0), sz(0), tight(false) {} + interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { SASSERT(invariant()); } bool invariant() const { - return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz); + return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) && + (!is_wrapped() || l != h+rational::one()); } bool is_full() const { return l.is_zero() && h == uMaxInt(sz); } @@ -113,13 +115,18 @@ struct interval { return false; // 0 .. l.. l' ... h ... h' - result = interval(std::max(l, b.l), std::min(h, b.h), sz); + 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(rational::zero(), uMaxInt(sz), true); + return true; + } + if (is_full()) return false; if (l.is_zero()) { @@ -152,40 +159,43 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { if (m_bv.is_bv_ule(e, lhs, rhs)) { if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C - b = interval(n, uMaxInt(sz), sz); + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); v = rhs; return true; } if (m_bv.is_numeral(rhs, n, sz)) { // x ule C - b = interval(rational::zero(), n, sz); + b = interval(rational::zero(), n, sz, true); v = lhs; return true; } } else if (m_bv.is_bv_sle(e, lhs, rhs)) { if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C - b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz); + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true); v = rhs; return true; } if (m_bv.is_numeral(rhs, n, sz)) { // x sle C - b = interval(rational::power_of_two(sz-1), n, sz); + b = interval(rational::power_of_two(sz-1), n, sz, true); v = lhs; return true; } } else if (m.is_eq(e, lhs, rhs)) { if (m_bv.is_numeral(lhs, n, sz)) { - b = interval(n, n, sz); + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); v = rhs; return true; } if (m_bv.is_numeral(rhs, n, sz)) { - b = interval(n, n, sz); + b = interval(n, n, sz, true); v = lhs; return true; } - } else if (m.is_not(e, lhs)) { - if (is_bound(lhs, v, b)) - return b.negate(b); } return false; } @@ -199,7 +209,7 @@ public: virtual ~bv_bounds_simplifier() {} - virtual void assert_expr(expr * t, bool sign) { + virtual bool assert_expr(expr * t, bool sign) { while (m.is_not(t, t)) { sign = !sign; } @@ -207,34 +217,54 @@ public: interval b; expr* t1; if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); if (sign) VERIFY(b.negate(b)); push(); TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value; - VERIFY(r.intersect(b, r)); + return r.intersect(b, r); } + return true; } virtual bool simplify(expr* t, expr_ref& result) { expr* t1; interval b, ctx, intr; result = 0; + bool sign = false; + + while (m.is_not(t, t)) { + sign = !sign; + } + if (!is_bound(t, t1, b)) return false; - if (m_bound->find(t1, ctx)) { - if (!b.intersect(ctx, intr)) { + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { result = m.mk_false(); - } else if (intr.l == intr.h && intr != b) { - result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); - } else if (ctx.implies(b)) { - result = m.mk_true(); + return true; } } + 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 (intr.l == intr.h) { + result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); + } + } else if (b.is_full() && b.tight) { + result = m.mk_true(); + } + 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; } diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 95be200a8..01937eb18 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -34,7 +34,7 @@ class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier { public: ctx_propagate_assertions(ast_manager& m); virtual ~ctx_propagate_assertions() {} - virtual void assert_expr(expr * t, bool sign); + virtual bool assert_expr(expr * t, bool sign); virtual bool simplify(expr* t, expr_ref& result); virtual void push(); virtual void pop(unsigned num_scopes); @@ -45,7 +45,7 @@ public: ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {} -void ctx_propagate_assertions::assert_expr(expr * t, bool sign) { +bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) { expr * p = t; while (m.is_not(t, t)) { @@ -64,6 +64,7 @@ void ctx_propagate_assertions::assert_expr(expr * t, bool sign) { else if (m.is_value(lhs)) assert_eq_val(rhs, to_app(lhs), mk_scope); } + return true; } void ctx_propagate_assertions::assert_eq_val(expr * t, app * val, bool mk_scope) { @@ -307,8 +308,8 @@ struct ctx_simplify_tactic::imp { CASSERT("ctx_simplify_tactic", check_cache()); } - void assert_expr(expr * t, bool sign) { - m_simp->assert_expr(t, sign); + bool assert_expr(expr * t, bool sign) { + return m_simp->assert_expr(t, sign); } bool is_cached(expr * t, expr_ref & r) { @@ -370,6 +371,9 @@ struct ctx_simplify_tactic::imp { simplify(arg, new_arg); if (new_arg != arg) modified = true; + if (i < num_args - 1 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR)) + new_arg = m.mk_false(); + if ((OR && m.is_false(new_arg)) || (!OR && m.is_true(new_arg))) { modified = true; @@ -383,8 +387,6 @@ struct ctx_simplify_tactic::imp { return; } new_args.push_back(new_arg); - if (i < num_args - 1) - assert_expr(new_arg, OR); } pop(scope_level() - old_lvl); @@ -398,6 +400,9 @@ struct ctx_simplify_tactic::imp { simplify(arg, new_arg); if (new_arg != arg) modified = true; + if (i > 0 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR)) + new_arg = m.mk_false(); + if ((OR && m.is_false(new_arg)) || (!OR && m.is_true(new_arg))) { modified = true; @@ -411,8 +416,6 @@ struct ctx_simplify_tactic::imp { return; } new_new_args.push_back(new_arg); - if (i > 0) - assert_expr(new_arg, OR); } pop(scope_level() - old_lvl); @@ -448,10 +451,14 @@ struct ctx_simplify_tactic::imp { else { expr_ref new_t(m); expr_ref new_e(m); - assert_expr(new_c, false); + if (!assert_expr(new_c, false)) { + simplify(e, r); + cache(ite, r); + return; + } simplify(t, new_t); pop(scope_level() - old_lvl); - assert_expr(new_c, true); + VERIFY(assert_expr(new_c, true)); simplify(e, new_e); pop(scope_level() - old_lvl); if (c == new_c && t == new_t && e == new_e) { diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index fccb25d3b..3c95ca554 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -28,7 +28,7 @@ public: goal_num_occurs* m_occs; public: virtual ~simplifier() {} - virtual void assert_expr(expr * t, bool sign) = 0; + virtual bool assert_expr(expr * t, bool sign) = 0; virtual bool simplify(expr* t, expr_ref& result) = 0; virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; From 73da4dda076f026871371290270100cebdd12182 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 18 Feb 2016 17:45:55 +0000 Subject: [PATCH 4/4] add a bv rewrite pattern: (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1)) --- src/ast/rewriter/bv_rewriter.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index fc0e5a807..be9b5f375 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -320,6 +320,21 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref } } + expr* a1, *a2, *a3, *a4, *a5, *a6; + // (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1)) + // (bvsle (+ x (* -1 (srem_i x c1))) c2) + // pre: (and (> c1 0) (> c2 0) (= c2 % c1 0) (<= (+ c1 c2 -1) max_int)) + if (is_signed && is_num2 && m_util.is_bv_add(a, a1, a2) && + m_util.is_bv_mul(a2, a3, a4) && is_numeral(a3, r1, sz) && + m_util.norm(r1, sz, is_signed).is_minus_one() && + m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r1, sz) && + (r1 = m_util.norm(r1, sz, is_signed), r1.is_pos()) && + r2.is_pos() && + (r2 % r1).is_zero() && r1 + r2 - rational::one() < rational::power_of_two(sz-1)) { + result = m_util.mk_sle(a1, m_util.mk_numeral(r1 + r2 - rational::one(), sz)); + return BR_REWRITE2; + } + #if 0 if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) { //