From a073b37ce30b0e2f81161de37d87b7de6f2cc6a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Feb 2016 18:10:16 -0800 Subject: [PATCH 1/4] fix bugs in seq solver: add relevancy and axiom Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 11bf2b678..a576685cc 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2678,6 +2678,7 @@ literal theory_seq::mk_seq_eq(expr* a, expr* b) { } literal theory_seq::mk_eq_empty(expr* _e) { + context& ctx = get_context(); expr_ref e(_e, m); SASSERT(m_util.is_seq(e)); expr_ref emp(m); @@ -2697,9 +2698,9 @@ literal theory_seq::mk_eq_empty(expr* _e) { } emp = m_util.str.mk_empty(m.get_sort(e)); - literal lit = mk_eq(e, emp, false); - get_context().force_phase(lit); + ctx.force_phase(lit); + ctx.mark_as_relevant(lit); return lit; } @@ -3385,16 +3386,15 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) { } expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m); - TRACE("seq", tout << mk_pp(e, m) << "\n";); - literal e2_is_emp = mk_eq_empty(e2); switch (ctx.get_assignment(e2_is_emp)) { case l_true: - TRACE("seq", tout << mk_pp(e2, m) << " = empty\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e2, m) << " = empty\n"; + ctx.display_literals_verbose(tout, 1, &e2_is_emp); tout << "\n"; ); return false; // done case l_undef: // ctx.force_phase(e2_is_emp); - TRACE("seq", tout << mk_pp(e2, m) << " ~ empty\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e2, m) << " ~ empty\n";); return true; // retry default: break; @@ -3407,10 +3407,11 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) { literal e1_is_emp = mk_eq_empty(e1); switch (ctx.get_assignment(e1_is_emp)) { case l_true: - TRACE("seq", tout << mk_pp(e1, m) << " = empty\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " != empty\n";); + add_axiom(ctx.get_literal(e), ~e1_is_emp); return false; // done case l_undef: - TRACE("seq", tout << mk_pp(e1, m) << " ~ empty\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " ~ empty\n";); return true; // retry default: break; @@ -3426,11 +3427,11 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) { case l_true: break; case l_false: - TRACE("seq", tout << head1 << " = " << head2 << "\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << head1 << " != " << head2 << "\n";); return false; case l_undef: ctx.force_phase(~lit); - TRACE("seq", tout << head1 << " ~ " << head2 << "\n";); + TRACE("seq", tout << mk_pp(e, m) << ": " << head1 << " ~ " << head2 << "\n";); return true; } change = true; @@ -3439,7 +3440,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) { lits.push_back(~e2_is_emp); lits.push_back(lit); propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2))); - TRACE("seq", tout << "saturate: " << tail1 << " = " << tail2 << "\n";); + TRACE("seq", tout << mk_pp(e, m) << " saturate: " << tail1 << " = " << tail2 << "\n";); return false; } From 121b3b60f3dba70d6a5189233df764f422d9e1d7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 19 Feb 2016 09:42:42 +0000 Subject: [PATCH 2/4] bv_bounds/ctx_simplify: improve handling of (ite x a b) where (not x) is proved to be false --- src/tactic/bv/bv_bounds_tactic.cpp | 5 +++++ src/tactic/core/ctx_simplify_tactic.cpp | 6 +++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index d9703990c..052345df1 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -36,6 +36,11 @@ struct interval { 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) { + // canonicalize full set + if (is_wrapped() && l == h + rational::one()) { + this->l = rational::zero(); + this->h = uMaxInt(sz); + } SASSERT(invariant()); } diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 01937eb18..f0e0b0059 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -458,7 +458,11 @@ struct ctx_simplify_tactic::imp { } simplify(t, new_t); pop(scope_level() - old_lvl); - VERIFY(assert_expr(new_c, true)); + if (!assert_expr(new_c, true)) { + r = new_t; + cache(ite, r); + return; + } simplify(e, new_e); pop(scope_level() - old_lvl); if (c == new_c && t == new_t && e == new_e) { From c618838ed9e4940c1de642a1b09e2eeb97effc1e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 19 Feb 2016 11:06:22 +0000 Subject: [PATCH 3/4] bv_bounds: fix crash in push() when realloc happened --- src/tactic/bv/bv_bounds_tactic.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 052345df1..317c17f12 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -152,10 +152,12 @@ std::ostream& operator<<(std::ostream& o, const interval& I) { class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { - ast_manager& m; - bv_util m_bv; - vector > m_scopes; - obj_map *m_bound; + typedef obj_map map; + + ast_manager& m; + bv_util m_bv; + vector m_scopes; + map *m_bound; bool is_bound(expr *e, expr*& v, interval& b) { rational n; @@ -208,7 +210,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { public: bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) { - m_scopes.push_back(obj_map()); + m_scopes.push_back(map()); m_bound = &m_scopes.back(); } @@ -275,8 +277,11 @@ public: virtual void push() { TRACE("bv", tout << "push\n";); - m_scopes.push_back(*m_bound); + unsigned sz = m_scopes.size(); + m_scopes.resize(sz + 1); m_bound = &m_scopes.back(); + m_bound->~map(); + new (m_bound) map(m_scopes[sz - 1]); } virtual void pop(unsigned num_scopes) { From 7d3af70a6320c30d43e8785b71b79a3cd664bdb4 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 19 Feb 2016 11:08:01 +0000 Subject: [PATCH 4/4] ctx-simplify: fix mem leak of simplifier --- src/tactic/core/ctx_simplify_tactic.cpp | 11 +++++++---- src/tactic/core/ctx_simplify_tactic.h | 5 +---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index f0e0b0059..3bcadb03d 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -180,6 +180,7 @@ struct ctx_simplify_tactic::imp { pop(scope_level()); SASSERT(scope_level() == 0); restore_cache(0); + dealloc(m_simp); DEBUG_CODE({ for (unsigned i = 0; i < m_cache.size(); i++) { CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, @@ -572,13 +573,15 @@ struct ctx_simplify_tactic::imp { ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p): m_imp(alloc(imp, m, simp, p)), - m_params(p), - m_simp(simp) { + m_params(p) { +} + +tactic * ctx_simplify_tactic::translate(ast_manager & m) { + return alloc(ctx_simplify_tactic, m, m_imp->m_simp->translate(m), m_params); } ctx_simplify_tactic::~ctx_simplify_tactic() { dealloc(m_imp); - dealloc(m_simp); } void ctx_simplify_tactic::updt_params(params_ref const & p) { @@ -606,7 +609,7 @@ void ctx_simplify_tactic::operator()(goal_ref const & in, void ctx_simplify_tactic::cleanup() { ast_manager & m = m_imp->m; - imp * d = alloc(imp, m, m_simp->translate(m), m_params); + imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params); std::swap(d, m_imp); dealloc(d); } diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 3c95ca554..5689a64b7 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -42,13 +42,10 @@ protected: struct imp; imp * m_imp; params_ref m_params; - simplifier* m_simp; public: ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p = params_ref()); - virtual tactic * translate(ast_manager & m) { - return alloc(ctx_simplify_tactic, m, m_simp->translate(m), m_params); - } + virtual tactic * translate(ast_manager & m); virtual ~ctx_simplify_tactic();