From 823830181b08afa05df7bc64487fe56b8cd72bb4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Feb 2021 16:37:23 -0800 Subject: [PATCH] butterfly effect with relevancy marking bail out of infinite instantiation loop --- src/ast/rewriter/seq_skolem.cpp | 40 ++++++++++++++++----------------- src/ast/rewriter/seq_skolem.h | 6 ++--- src/smt/seq_axioms.h | 2 +- src/smt/seq_eq_solver.cpp | 17 +++++++++++--- src/smt/seq_regex.cpp | 2 +- src/smt/seq_regex.h | 2 +- src/smt/theory_lra.cpp | 7 +++--- src/smt/theory_seq.h | 2 +- 8 files changed, 45 insertions(+), 33 deletions(-) diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index 33f192ceb..8fae87643 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -3,7 +3,7 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - seq_skolem.cpp + skolem.cpp Author: @@ -14,10 +14,10 @@ Author: #include "ast/rewriter/seq_skolem.h" #include "ast/ast_pp.h" -using namespace smt; +using namespace seq; -seq_skolem::seq_skolem(ast_manager& m, th_rewriter& rw): +skolem::skolem(ast_manager& m, th_rewriter& rw): m(m), m_rewrite(rw), seq(m), @@ -40,7 +40,7 @@ seq_skolem::seq_skolem(ast_manager& m, th_rewriter& rw): m_is_non_empty = "re.is_non_empty"; } -expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range, bool rw) { +expr_ref skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range, bool rw) { expr* es[4] = { e1, e2, e3, e4 }; unsigned len = e4?4:(e3?3:(e2?2:(e1?1:0))); if (!range) { @@ -52,19 +52,19 @@ expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, return result; } -expr_ref seq_skolem::mk_max_unfolding_depth(unsigned depth) { +expr_ref skolem::mk_max_unfolding_depth(unsigned depth) { parameter ps[2] = { parameter(m_max_unfolding), parameter(depth) }; func_decl* f = m.mk_func_decl(seq.get_family_id(), _OP_SEQ_SKOLEM, 2, ps, 0, (sort*const*) nullptr, m.mk_bool_sort()); return expr_ref(m.mk_const(f), m); } -expr_ref seq_skolem::mk_length_limit(expr* e, unsigned d) { +expr_ref skolem::mk_length_limit(expr* e, unsigned d) { parameter ps[3] = { parameter(m_length_limit), parameter(d), parameter(e) }; func_decl* f = m.mk_func_decl(seq.get_family_id(), _OP_SEQ_SKOLEM, 3, ps, 0, (sort*const*) nullptr, m.mk_bool_sort()); return expr_ref(m.mk_const(f), m); } -bool seq_skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const { +bool skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const { if (!is_length_limit(p)) return false; lim = to_app(p)->get_parameter(1).get_int(); @@ -73,11 +73,11 @@ bool seq_skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const { } -bool seq_skolem::is_skolem(symbol const& s, expr const* e) const { +bool skolem::is_skolem(symbol const& s, expr const* e) const { return seq.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s; } -void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) { +void skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) { expr* e1 = nullptr, *e2 = nullptr; zstring s; rational r; @@ -124,7 +124,7 @@ decompose_main: } } -bool seq_skolem::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const { +bool skolem::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const { if (is_step(e)) { s = to_app(e)->get_arg(0); idx = to_app(e)->get_arg(1); @@ -139,34 +139,34 @@ bool seq_skolem::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, exp } } -bool seq_skolem::is_tail_u(expr* e, expr*& s, unsigned& idx) const { +bool skolem::is_tail_u(expr* e, expr*& s, unsigned& idx) const { expr* i = nullptr; rational r; return is_tail(e, s, i) && a.is_numeral(i, r) && r.is_unsigned() && (idx = r.get_unsigned(), true); } -bool seq_skolem::is_tail(expr* e, expr*& s) const { +bool skolem::is_tail(expr* e, expr*& s) const { expr* i = nullptr; return is_tail(e, s, i); } -bool seq_skolem::is_tail(expr* e, expr*& s, expr*& idx) const { +bool skolem::is_tail(expr* e, expr*& s, expr*& idx) const { return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true); } -bool seq_skolem::is_eq(expr* e, expr*& a, expr*& b) const { +bool skolem::is_eq(expr* e, expr*& a, expr*& b) const { return is_skolem(m_eq, e) && (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true); } -bool seq_skolem::is_pre(expr* e, expr*& s, expr*& i) { +bool skolem::is_pre(expr* e, expr*& s, expr*& i) { return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true); } -bool seq_skolem::is_post(expr* e, expr*& s, expr*& start) { +bool skolem::is_post(expr* e, expr*& s, expr*& start) { return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), start = to_app(e)->get_arg(1), true); } -expr_ref seq_skolem::mk_unit_inv(expr* n) { +expr_ref skolem::mk_unit_inv(expr* n) { expr* u = nullptr; VERIFY(seq.str.is_unit(n, u)); sort* s = u->get_sort(); @@ -174,7 +174,7 @@ expr_ref seq_skolem::mk_unit_inv(expr* n) { } -expr_ref seq_skolem::mk_last(expr* s) { +expr_ref skolem::mk_last(expr* s) { zstring str; if (seq.str.is_string(s, str) && str.length() > 0) { return expr_ref(seq.str.mk_char(str, str.length()-1), m); @@ -184,7 +184,7 @@ expr_ref seq_skolem::mk_last(expr* s) { return mk(m_seq_last, s, char_sort); } -expr_ref seq_skolem::mk_first(expr* s) { +expr_ref skolem::mk_first(expr* s) { zstring str; if (seq.str.is_string(s, str) && str.length() > 0) { return expr_ref(seq.str.mk_string(str.extract(0, str.length()-1)), m); @@ -192,7 +192,7 @@ expr_ref seq_skolem::mk_first(expr* s) { return mk(m_seq_first, s); } -expr_ref seq_skolem::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) { +expr_ref skolem::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) { expr_ref_vector args(m); args.push_back(s).push_back(idx).push_back(re); args.push_back(a.mk_int(i)); diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 4e59d2c15..bf04d4a48 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -22,9 +22,9 @@ Author: #include "ast/arith_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" -namespace smt { +namespace seq { - class seq_skolem { + class skolem { ast_manager& m; th_rewriter& m_rewrite; // NB: would be nicer not to have this dependency seq_util seq; @@ -43,7 +43,7 @@ namespace smt { public: - seq_skolem(ast_manager& m, th_rewriter& r); + skolem(ast_manager& m, th_rewriter& r); expr_ref mk(symbol const& s, sort* range) { return mk(s, nullptr, nullptr, nullptr, nullptr, range); } expr_ref mk(symbol const& s, expr* e, sort* range) { return mk(s, e, nullptr, nullptr, nullptr, range); } diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 2299695ea..7785b3aa7 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -33,7 +33,7 @@ namespace smt { ast_manager& m; arith_util a; seq_util seq; - seq_skolem m_sk; + seq::skolem m_sk; bool m_digits_initialized; literal mk_eq_empty(expr* e, bool phase = true) { return mk_eq_empty2(e, phase); } diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 05ca8df7f..23bbc7350 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -1321,23 +1321,34 @@ bool theory_seq::propagate_length_coherence(expr* e) { expr_ref lo_e(m_autil.mk_numeral(lo, true), m); expr_ref len_e_ge_lo(m_autil.mk_ge(mk_len(e), lo_e), m); literal low = mk_literal(len_e_ge_lo); - add_axiom(~low, mk_seq_eq(e, tail)); + literal eq = mk_seq_eq(e, tail); + bool added = false; + if (ctx.get_assignment(eq) != l_true) { + add_axiom(~low, eq); + added = true; + } expr_ref len_e = mk_len(e); if (upper_bound(len_e, hi)) { // len(e) <= hi => len(tail) <= hi - lo expr_ref high1(m_autil.mk_le(len_e, m_autil.mk_numeral(hi, true)), m); if (hi == lo) { add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp)); + added = true; } else { expr_ref high2(m_autil.mk_le(mk_len(seq), m_autil.mk_numeral(hi-lo, true)), m); - add_axiom(~mk_literal(high1), mk_literal(high2)); + literal h2 = mk_literal(high2); + if (ctx.get_assignment(h2) != l_true) { + add_axiom(~mk_literal(high1), h2); + added = true; + } } } else { assume_equality(seq, emp); + added = true; } - return true; + return added; } diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b22c61039..0613e584d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -32,7 +32,7 @@ namespace smt { class seq_util::rex& seq_regex::re() { return th.m_util.re; } class seq_util::str& seq_regex::str() { return th.m_util.str; } seq_rewriter& seq_regex::seq_rw() { return th.m_seq_rewrite; } - seq_skolem& seq_regex::sk() { return th.m_sk; } + seq::skolem& seq_regex::sk() { return th.m_sk; } arith_util& seq_regex::a() { return th.m_autil; } void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); } diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 983032979..8a2cf68f1 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -137,7 +137,7 @@ namespace smt { class seq_util::rex& re(); class seq_util::str& str(); seq_rewriter& seq_rw(); - seq_skolem& sk(); + seq::skolem& sk(); arith_util& a(); bool is_string_equality(literal lit); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b42b9a699..bf1ec9cb2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -546,13 +546,14 @@ class theory_lra::imp { enode * mk_enode(app * n) { TRACE("arith", tout << expr_ref(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";); + if (reflect(n)) + for (expr* arg : *n) + if (!ctx().e_internalized(arg)) + th.ensure_enode(arg); if (ctx().e_internalized(n)) { return get_enode(n); } else { - if (reflect(n)) - for (expr* arg : *n) - th.ensure_enode(arg); return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n)); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 1a14279ce..922ed59c0 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -355,7 +355,7 @@ namespace smt { seq_rewriter m_seq_rewrite; seq_util m_util; arith_util m_autil; - seq_skolem m_sk; + seq::skolem m_sk; seq_axioms m_ax; seq_regex m_regex; arith_value m_arith_value;