From 68e4ed3c9c039716a53849b2e85fb4818f43b71e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Sep 2019 09:59:58 -0700 Subject: [PATCH] fix #2531 Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.cpp | 46 +++++++++++++++++++++++++++++++++++++++ src/ast/for_each_expr.h | 20 +++++++++++++++++ src/qe/nlqsat.cpp | 9 +++++--- src/qe/qsat.cpp | 10 ++++----- src/smt/theory_seq.cpp | 11 +++++++--- 5 files changed, 85 insertions(+), 11 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 311133e05..dd8a546f9 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -63,3 +63,49 @@ bool has_skolem_functions(expr * n) { } return false; } + +subterms::subterms(expr_ref_vector const& es): m_es(es) {} +subterms::subterms(expr_ref& e) : m_es(e.m()) { m_es.push_back(e); } +subterms::iterator subterms::begin() { return iterator(*this, true); } +subterms::iterator subterms::end() { return iterator(*this, false); } +subterms::iterator::iterator(subterms& f, bool start): m_es(f.m_es) { + if (!start) m_es.reset(); +} +expr* subterms::iterator::operator*() { + return m_es.back(); +} +subterms::iterator subterms::iterator::operator++(int) { + iterator tmp = *this; + ++*this; + return tmp; +} +subterms::iterator& subterms::iterator::operator++() { + expr* e = m_es.back(); + m_visited.mark(e, true); + if (is_app(e)) { + for (expr* arg : *to_app(e)) { + m_es.push_back(arg); + } + } + while (m_visited.is_marked(m_es.back())) { + m_es.pop_back(); + } + return *this; +} + +bool subterms::iterator::operator==(iterator const& other) const { + // ignore state of visited + if (other.m_es.size() != m_es.size()) { + return false; + } + for (unsigned i = m_es.size(); i-- > 0; ) { + if (m_es.get(i) != other.m_es.get(i)) + return false; + } + return true; +} + +bool subterms::iterator::operator!=(iterator const& other) const { + return !(*this == other); +} + diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 6e203ccee..647bbd169 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -167,5 +167,25 @@ unsigned get_num_exprs(expr * n, expr_fast_mark1 & visited); bool has_skolem_functions(expr * n); +class subterms { + expr_ref_vector m_es; +public: + class iterator { + expr_ref_vector m_es; + expr_mark m_visited; + public: + iterator(subterms& f, bool start); + expr* operator*(); + iterator operator++(int); + iterator& operator++(); + bool operator==(iterator const& other) const; + bool operator!=(iterator const& other) const; + }; + subterms(expr_ref_vector const& es); + subterms(expr_ref& e); + iterator begin(); + iterator end(); +}; + #endif /* FOR_EACH_EXPR_H_ */ diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 81e1c9ce8..434690ef0 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -666,7 +666,7 @@ namespace qe { // expr -> nlsat::solver - void hoist(expr_ref& fml) { + bool hoist(expr_ref& fml) { expr_ref_vector paxioms(m); ackermanize_div(fml, paxioms); quantifier_hoister hoist(m); @@ -674,7 +674,6 @@ namespace qe { app_ref_vector vars(m); bool is_forall = false; pred_abs abs(m); - expr_ref fml_a(m.mk_and(fml, mk_and(paxioms)), m); abs.get_free_vars(fml_a, vars); insert_set(m_free_vars, vars); @@ -752,6 +751,7 @@ namespace qe { } } TRACE("qe", tout << fml << "\n";); + return true; } @@ -836,7 +836,10 @@ namespace qe { } reset(); TRACE("qe", tout << fml << "\n";); - hoist(fml); + if (!hoist(fml)) { + result.push_back(in.get()); + return; + } TRACE("qe", tout << "ex: " << fml << "\n";); lbool is_sat = check_sat(); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index d1816d807..fcac507fe 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -511,14 +511,14 @@ namespace qe { bool pred_abs::validate_defs(model& model) const { bool valid = true; - obj_map::iterator it = m_pred2lit.begin(), end = m_pred2lit.end(); - for (; it != end; ++it) { + for (auto& kv : m_pred2lit) { expr_ref val_a(m), val_b(m); - expr* a = it->m_key; - expr* b = it->m_value; + expr* a = kv.m_key; + expr* b = kv.m_value; val_a = model(a); val_b = model(b); - if (val_a != val_b) { + if ((m.is_true(val_a) && m.is_false(val_b)) || + (m.is_false(val_a) && m.is_true(val_b))) { TRACE("qe", tout << mk_pp(a, m) << " := " << val_a << "\n"; tout << mk_pp(b, m) << " := " << val_b << "\n"; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 20e6cb140..5db1b0f5f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -339,6 +339,7 @@ final_check_status theory_seq::final_check_eh() { m_rep.reset_cache(); m_reset_cache = false; } + m_new_propagation = false; TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); TRACE("seq_verbose", get_context().display(tout);); @@ -3320,7 +3321,7 @@ bool theory_seq::solve_nc(unsigned idx) { expr_ref c = canonize(n.contains(), deps); expr* a = nullptr, *b = nullptr; - CTRACE("seq", c != n.contains(), tout << n.contains() << " => " << c << "\n";); + CTRACE("seq", c != n.contains(), tout << n.contains() << " =>\n" << c << "\n";); if (m.is_true(c)) { @@ -3334,6 +3335,9 @@ bool theory_seq::solve_nc(unsigned idx) { } if (ctx.get_assignment(len_gt) == l_true) { + VERIFY(m_util.str.is_contains(n.contains(), a, b)); + enforce_length(a); + enforce_length(b); TRACE("seq", tout << len_gt << " is true\n";); return true; } @@ -3605,6 +3609,7 @@ bool theory_seq::internalize_term(app* term) { } void theory_seq::add_length(expr* e, expr* l) { + TRACE("seq", tout << get_context().get_scope_level() << " " << mk_pp(e, m) << "\n";); SASSERT(!m_length.contains(l)); m_length.push_back(l); m_has_length.insert(e); @@ -4278,9 +4283,9 @@ bool theory_seq::can_propagate() { expr_ref theory_seq::canonize(expr* e, dependency*& eqs) { expr_ref result = expand(e, eqs); - TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";); + TRACE("seq", tout << mk_pp(e, m) << " expands to\n" << result << "\n";); m_rewrite(result); - TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";); + TRACE("seq", tout << mk_pp(e, m) << " rewrites to\n" << result << "\n";); return result; }