From 009e94d18821ed3723f1db681ca032aae086ca0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Aug 2017 14:00:01 -0700 Subject: [PATCH] update to theory_seq following examples from PJLJ Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.h | 1 + src/ast/pattern/pattern_inference.cpp | 637 +----------------------- src/ast/rewriter/seq_rewriter.cpp | 18 +- src/math/automata/automaton.h | 10 + src/smt/smt_quantifier.cpp | 26 +- src/smt/theory_seq.cpp | 79 ++- src/smt/theory_seq.h | 2 + src/tactic/core/dom_simplify_tactic.cpp | 116 ++++- src/tactic/core/dom_simplify_tactic.h | 31 ++ 9 files changed, 213 insertions(+), 707 deletions(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index 924481dd8..d360356eb 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -79,6 +79,7 @@ public: } } bool empty() const { return m_subst.empty(); } + expr* find(expr * e) { proof* pr; expr* d = 0; if (find(e, d, pr)) return d; else return e; } bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); } bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); } bool contains(expr * s) { return m_subst.contains(s); } diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index dfeb29ffe..6a91dd85e 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -97,641 +97,6 @@ static void dump_app_vector(std::ostream & out, ptr_vector const & v, ast_m } #endif -#if 0 -pattern_inference_old::pattern_inference_old(ast_manager & m, pattern_inference_params & params): - simplifier(m), - m_params(params), - m_bfid(m.get_basic_family_id()), - m_afid(m.mk_family_id("arith")), - m_le(m), - m_nested_arith_only(true), - m_block_loop_patterns(params.m_pi_block_loop_patterns), - m_candidates(m), - m_pattern_weight_lt(m_candidates_info), - m_collect(m, *this), - m_contains_subpattern(*this), - m_database(m) { - if (params.m_pi_arith == AP_NO) - register_forbidden_family(m_afid); - enable_ac_support(false); -} - -void pattern_inference_old::collect::operator()(expr * n, unsigned num_bindings) { - SASSERT(m_info.empty()); - SASSERT(m_todo.empty()); - SASSERT(m_cache.empty()); - m_num_bindings = num_bindings; - m_todo.push_back(entry(n, 0)); - while (!m_todo.empty()) { - entry & e = m_todo.back(); - n = e.m_node; - unsigned delta = e.m_delta; - TRACE("collect", tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";); - TRACE("collect_info", tout << mk_pp(n, m) << "\n";); - if (visit_children(n, delta)) { - m_todo.pop_back(); - save_candidate(n, delta); - } - } - reset(); -} - -inline void pattern_inference_old::collect::visit(expr * n, unsigned delta, bool & visited) { - entry e(n, delta); - if (!m_cache.contains(e)) { - m_todo.push_back(e); - visited = false; - } -} - -bool pattern_inference_old::collect::visit_children(expr * n, unsigned delta) { - bool visited = true; - unsigned i; - switch (n->get_kind()) { - case AST_APP: - i = to_app(n)->get_num_args(); - while (i > 0) { - --i; - visit(to_app(n)->get_arg(i), delta, visited); - } - break; - case AST_QUANTIFIER: - visit(to_quantifier(n)->get_expr(), delta + to_quantifier(n)->get_num_decls(), visited); - break; - default: - break; - } - return visited; -} - -inline void pattern_inference_old::collect::save(expr * n, unsigned delta, info * i) { - m_cache.insert(entry(n, delta), i); - if (i != 0) - m_info.push_back(i); -} - -void pattern_inference_old::collect::save_candidate(expr * n, unsigned delta) { - switch (n->get_kind()) { - case AST_VAR: { - unsigned idx = to_var(n)->get_idx(); - if (idx >= delta) { - idx = idx - delta; - uint_set free_vars; - if (idx < m_num_bindings) - free_vars.insert(idx); - info * i = 0; - if (delta == 0) - i = alloc(info, m, n, free_vars, 1); - else - i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1); - save(n, delta, i); - } - else { - save(n, delta, 0); - } - return; - } - case AST_APP: { - app * c = to_app(n); - func_decl * decl = c->get_decl(); - if (m_owner.is_forbidden(c)) { - save(n, delta, 0); - return; - } - - if (c->get_num_args() == 0) { - save(n, delta, alloc(info, m, n, uint_set(), 1)); - return; - } - - ptr_buffer buffer; - bool changed = false; // false if none of the children is mapped to a node different from itself. - uint_set free_vars; - unsigned size = 1; - unsigned num = c->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * child = c->get_arg(i); - info * child_info = 0; -#ifdef Z3DEBUG - bool found = -#endif - m_cache.find(entry(child, delta), child_info); - SASSERT(found); - if (child_info == 0) { - save(n, delta, 0); - return; - } - buffer.push_back(child_info->m_node.get()); - free_vars |= child_info->m_free_vars; - size += child_info->m_size; - if (child != child_info->m_node.get()) - changed = true; - } - - app * new_node = 0; - if (changed) - new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr()); - else - new_node = to_app(n); - save(n, delta, alloc(info, m, new_node, free_vars, size)); - // Remark: arithmetic patterns are only used if they are nested inside other terms. - // That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern - // if arithmetic is not in the forbidden list. - // - // Remark: The rule above has an exception. The operators (div, idiv, mod) are allowed to be - // used as patterns even when they are not nested in other terms. The motivation is that - // Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms - // stating properties about these operators. - family_id fid = c->get_family_id(); - decl_kind k = c->get_decl_kind(); - if (!free_vars.empty() && - (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) { - TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";); - m_owner.add_candidate(new_node, free_vars, size); - } - return; - } - default: - save(n, delta, 0); - return; - } -} - - -void pattern_inference_old::collect::reset() { - m_cache.reset(); - std::for_each(m_info.begin(), m_info.end(), delete_proc()); - m_info.reset(); - SASSERT(m_todo.empty()); -} - -void pattern_inference_old::add_candidate(app * n, uint_set const & free_vars, unsigned size) { - for (unsigned i = 0; i < m_num_no_patterns; i++) { - if (n == m_no_patterns[i]) - return; - } - - if (!m_candidates_info.contains(n)) { - m_candidates_info.insert(n, info(free_vars, size)); - m_candidates.push_back(n); - } -} - - -/** - \brief Copy the non-looping patterns in m_candidates to result when m_params.m_pi_block_loop_patterns = true. - Otherwise, copy m_candidates to result. -*/ -void pattern_inference_old::filter_looping_patterns(ptr_vector & result) { - unsigned num = m_candidates.size(); - for (unsigned i1 = 0; i1 < num; i1++) { - app * n1 = m_candidates.get(i1); - expr2info::obj_map_entry * e1 = m_candidates_info.find_core(n1); - SASSERT(e1); - uint_set const & s1 = e1->get_data().m_value.m_free_vars; - if (m_block_loop_patterns) { - bool smaller = false; - for (unsigned i2 = 0; i2 < num; i2++) { - if (i1 != i2) { - app * n2 = m_candidates.get(i2); - expr2info::obj_map_entry * e2 = m_candidates_info.find_core(n2); - if (e2) { - uint_set const & s2 = e2->get_data().m_value.m_free_vars; - // Remark: the comparison operator only makes sense if both AST nodes - // contain the same number of variables. - // Example: - // (f X Y) <: (f (g X Z W) Y) - if (s1 == s2 && m_le(m_num_bindings, n1, n2) && !m_le(m_num_bindings, n2, n1)) { - smaller = true; - break; - } - } - } - } - if (!smaller) - result.push_back(n1); - else - m_candidates_info.erase(n1); - } - else { - result.push_back(n1); - } - } -} - - - -inline void pattern_inference_old::contains_subpattern::save(expr * n) { - unsigned id = n->get_id(); - m_already_processed.assure_domain(id); - if (!m_already_processed.contains(id)) { - m_todo.push_back(n); - m_already_processed.insert(id); - } -} - -bool pattern_inference_old::contains_subpattern::operator()(expr * n) { - m_already_processed.reset(); - m_todo.reset(); - expr2info::obj_map_entry * _e = m_owner.m_candidates_info.find_core(n); - SASSERT(_e); - uint_set const & s1 = _e->get_data().m_value.m_free_vars; - save(n); - unsigned num; - while (!m_todo.empty()) { - expr * curr = m_todo.back(); - m_todo.pop_back(); - switch (curr->get_kind()) { - case AST_APP: - if (curr != n) { - expr2info::obj_map_entry * e = m_owner.m_candidates_info.find_core(curr); - if (e) { - uint_set const & s2 = e->get_data().m_value.m_free_vars; - SASSERT(s2.subset_of(s1)); - if (s1 == s2) { - TRACE("pattern_inference", tout << mk_pp(n, m_owner.m) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m) << "\n";); - return true; - } - } - } - num = to_app(curr)->get_num_args(); - for (unsigned i = 0; i < num; i++) - save(to_app(curr)->get_arg(i)); - break; - case AST_VAR: - break; - default: - UNREACHABLE(); - } - } - return false; -} - -/** - Return true if n contains a direct/indirect child that is also a - pattern, and contains the same number of free variables. -*/ -inline bool pattern_inference_old::contains_subpattern(expr * n) { - return m_contains_subpattern(n); -} - -/** - \brief Copy a pattern p in patterns to result, if there is no - direct/indirect child of p in patterns which contains the same set - of variables. - - Remark: Every pattern p in patterns is also a member of - m_pattern_map. -*/ -void pattern_inference_old::filter_bigger_patterns(ptr_vector const & patterns, ptr_vector & result) { - for (app * curr : patterns) { - if (!contains_subpattern(curr)) - result.push_back(curr); - } -} - - -bool pattern_inference_old::pattern_weight_lt::operator()(expr * n1, expr * n2) const { - expr2info::obj_map_entry * e1 = m_candidates_info.find_core(n1); - expr2info::obj_map_entry * e2 = m_candidates_info.find_core(n2); - SASSERT(e1 != 0); - SASSERT(e2 != 0); - info const & i1 = e1->get_data().m_value; - info const & i2 = e2->get_data().m_value; - unsigned num_free_vars1 = i1.m_free_vars.num_elems(); - unsigned num_free_vars2 = i2.m_free_vars.num_elems(); - return num_free_vars1 > num_free_vars2 || (num_free_vars1 == num_free_vars2 && i1.m_size < i2.m_size); -} - -/** - \brief Create unary patterns (single expressions that contain all - bound variables). If a candidate does not contain all bound - variables, then it is copied to remaining_candidate_patterns. The - new patterns are stored in result. -*/ -void pattern_inference_old::candidates2unary_patterns(ptr_vector const & candidate_patterns, - ptr_vector & remaining_candidate_patterns, - app_ref_buffer & result) { - for (app * candidate : candidate_patterns) { - expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate); - info const & i = e->get_data().m_value; - if (i.m_free_vars.num_elems() == m_num_bindings) { - app * new_pattern = m.mk_pattern(candidate); - result.push_back(new_pattern); - } - else { - remaining_candidate_patterns.push_back(candidate); - } - } -} - -// TODO: this code is too inefficient when the number of candidate -// patterns is too big. -// HACK: limit the number of case-splits: -#define MAX_SPLITS 32 - -void pattern_inference_old::candidates2multi_patterns(unsigned max_num_patterns, - ptr_vector const & candidate_patterns, - app_ref_buffer & result) { - SASSERT(!candidate_patterns.empty()); - m_pre_patterns.push_back(alloc(pre_pattern)); - unsigned sz = candidate_patterns.size(); - unsigned num_splits = 0; - for (unsigned j = 0; j < m_pre_patterns.size(); j++) { - pre_pattern * curr = m_pre_patterns[j]; - if (curr->m_free_vars.num_elems() == m_num_bindings) { - app * new_pattern = m.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr()); - result.push_back(new_pattern); - if (result.size() >= max_num_patterns) - return; - } - else if (curr->m_idx < sz) { - app * n = candidate_patterns[curr->m_idx]; - expr2info::obj_map_entry * e = m_candidates_info.find_core(n); - uint_set const & s = e->get_data().m_value.m_free_vars; - if (!s.subset_of(curr->m_free_vars)) { - pre_pattern * new_p = alloc(pre_pattern,*curr); - new_p->m_exprs.push_back(n); - new_p->m_free_vars |= s; - new_p->m_idx++; - m_pre_patterns.push_back(new_p); - - if (num_splits < MAX_SPLITS) { - m_pre_patterns[j] = 0; - curr->m_idx++; - m_pre_patterns.push_back(curr); - num_splits++; - } - } - else { - m_pre_patterns[j] = 0; - curr->m_idx++; - m_pre_patterns.push_back(curr); - } - } - TRACE("pattern_inference", tout << "m_pre_patterns.size(): " << m_pre_patterns.size() << - "\nnum_splits: " << num_splits << "\n";); - } -} - -void pattern_inference_old::reset_pre_patterns() { - std::for_each(m_pre_patterns.begin(), m_pre_patterns.end(), delete_proc()); - m_pre_patterns.reset(); -} - - -bool pattern_inference_old::is_forbidden(app * n) const { - func_decl const * decl = n->get_decl(); - if (is_ground(n)) - return false; - // Remark: skolem constants should not be used in patterns, since they do not - // occur outside of the quantifier. That is, Z3 will never match this kind of - // pattern. - if (m_params.m_pi_avoid_skolems && decl->is_skolem()) { - CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";); - return true; - } - if (is_forbidden(decl)) - return true; - return false; -} - -bool pattern_inference_old::has_preferred_patterns(ptr_vector & candidate_patterns, app_ref_buffer & result) { - if (m_preferred.empty()) - return false; - bool found = false; - for (app * candidate : candidate_patterns) { - if (m_preferred.contains(to_app(candidate)->get_decl())) { - expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate); - info const & i = e->get_data().m_value; - if (i.m_free_vars.num_elems() == m_num_bindings) { - TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m) << "\n";); - app * p = m.mk_pattern(candidate); - result.push_back(p); - found = true; - } - } - } - return found; -} - -void pattern_inference_old::mk_patterns(unsigned num_bindings, - expr * n, - unsigned num_no_patterns, - expr * const * no_patterns, - app_ref_buffer & result) { - m_num_bindings = num_bindings; - m_num_no_patterns = num_no_patterns; - m_no_patterns = no_patterns; - - m_collect(n, num_bindings); - - TRACE("pattern_inference", - tout << mk_pp(n, m); - tout << "\ncandidates:\n"; - unsigned num = m_candidates.size(); - for (unsigned i = 0; i < num; i++) { - tout << mk_pp(m_candidates.get(i), m) << "\n"; - }); - - if (!m_candidates.empty()) { - m_tmp1.reset(); - filter_looping_patterns(m_tmp1); - TRACE("pattern_inference", - tout << "candidates after removing looping-patterns:\n"; - dump_app_vector(tout, m_tmp1, m);); - SASSERT(!m_tmp1.empty()); - if (!has_preferred_patterns(m_tmp1, result)) { - // continue if there are no preferred patterns - m_tmp2.reset(); - filter_bigger_patterns(m_tmp1, m_tmp2); - SASSERT(!m_tmp2.empty()); - TRACE("pattern_inference", - tout << "candidates after removing bigger patterns:\n"; - dump_app_vector(tout, m_tmp2, m);); - m_tmp1.reset(); - candidates2unary_patterns(m_tmp2, m_tmp1, result); - unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns; - if (result.empty()) - num_extra_multi_patterns++; - if (num_extra_multi_patterns > 0 && !m_tmp1.empty()) { - // m_pattern_weight_lt is not a total order - std::stable_sort(m_tmp1.begin(), m_tmp1.end(), m_pattern_weight_lt); - TRACE("pattern_inference", - tout << "candidates after sorting:\n"; - dump_app_vector(tout, m_tmp1, m);); - candidates2multi_patterns(num_extra_multi_patterns, m_tmp1, result); - } - } - } - - reset_pre_patterns(); - m_candidates_info.reset(); - m_candidates.reset(); -} - - -void pattern_inference_old::reduce1_quantifier(quantifier * q) { - TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";); - if (!q->is_forall()) { - simplifier::reduce1_quantifier(q); - return; - } - - int weight = q->get_weight(); - - if (m_params.m_pi_use_database) { - m_database.initialize(g_pattern_database); - app_ref_vector new_patterns(m); - unsigned new_weight; - if (m_database.match_quantifier(q, new_patterns, new_weight)) { -#ifdef Z3DEBUG - for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); } -#endif - quantifier_ref new_q(m); - if (q->get_num_patterns() > 0) { - // just update the weight... - TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";); - new_q = m.update_quantifier_weight(q, new_weight); - } - else { - quantifier_ref tmp(m); - tmp = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr()); - new_q = m.update_quantifier_weight(tmp, new_weight); - TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";); - } - proof * pr = 0; - if (m.fine_grain_proofs()) - pr = m.mk_rewrite(q, new_q); - cache_result(q, new_q, pr); - return; - } - } - - if (q->get_num_patterns() > 0) { - simplifier::reduce1_quantifier(q); - return; - } - - if (m_params.m_pi_nopat_weight >= 0) - weight = m_params.m_pi_nopat_weight; - - SASSERT(q->get_num_patterns() == 0); - expr * new_body; - proof * new_body_pr; - get_cached(q->get_expr(), new_body, new_body_pr); - - ptr_buffer new_no_patterns; - unsigned num_no_patterns = q->get_num_no_patterns(); - for (unsigned i = 0; i < num_no_patterns; i++) { - expr * new_pattern; - proof * new_pattern_pr; - get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr); - new_no_patterns.push_back(new_pattern); - } - - app_ref_buffer new_patterns(m); - - if (m_params.m_pi_arith == AP_CONSERVATIVE) - m_forbidden.push_back(m_afid); - - mk_patterns(q->get_num_decls(), new_body, new_no_patterns.size(), new_no_patterns.c_ptr(), new_patterns); - - if (new_patterns.empty() && !new_no_patterns.empty()) { - if (new_patterns.empty()) { - mk_patterns(q->get_num_decls(), new_body, 0, 0, new_patterns); - if (m_params.m_pi_warnings && !new_patterns.empty()) { - warning_msg("ignoring nopats annotation because Z3 couldn't find any other pattern (quantifier id: %s)", q->get_qid().str().c_str()); - } - } - } - - if (m_params.m_pi_arith == AP_CONSERVATIVE) { - m_forbidden.pop_back(); - if (new_patterns.empty()) { - flet l1(m_block_loop_patterns, false); // allow looping patterns - mk_patterns(q->get_num_decls(), new_body, new_no_patterns.size(), new_no_patterns.c_ptr(), new_patterns); - if (!new_patterns.empty()) { - weight = std::max(weight, static_cast(m_params.m_pi_arith_weight)); - if (m_params.m_pi_warnings) { - warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=).", - q->get_qid().str().c_str(), weight); - } - } - } - } - - if (m_params.m_pi_arith != AP_NO && new_patterns.empty()) { - if (new_patterns.empty()) { - flet l1(m_nested_arith_only, false); // try to find a non-nested arith pattern - flet l2(m_block_loop_patterns, false); // allow looping patterns - mk_patterns(q->get_num_decls(), new_body, new_no_patterns.size(), new_no_patterns.c_ptr(), new_patterns); - if (!new_patterns.empty()) { - weight = std::max(weight, static_cast(m_params.m_pi_non_nested_arith_weight)); - if (m_params.m_pi_warnings) { - warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=).", - q->get_qid().str().c_str(), weight); - } - // verbose_stream() << mk_pp(q, m) << "\n"; - } - } - } - - quantifier_ref new_q(m); - new_q = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body); - if (weight != q->get_weight()) - new_q = m.update_quantifier_weight(new_q, weight); - proof_ref pr(m); - if (m.fine_grain_proofs()) { - if (new_body_pr == 0) - new_body_pr = m.mk_reflexivity(new_body); - pr = m.mk_quant_intro(q, new_q, new_body_pr); - } - - if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) { - pull_quant pull(m); - expr_ref new_expr(m); - proof_ref new_pr(m); - pull(new_q, new_expr, new_pr); - quantifier * new_new_q = to_quantifier(new_expr); - if (new_new_q != new_q) { - mk_patterns(new_new_q->get_num_decls(), new_new_q->get_expr(), 0, 0, new_patterns); - if (!new_patterns.empty()) { - if (m_params.m_pi_warnings) { - warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str()); - } - new_q = m.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr()); - if (m.fine_grain_proofs()) { - pr = m.mk_transitivity(pr, new_pr); - pr = m.mk_transitivity(pr, m.mk_quant_intro(new_new_q, new_q, m.mk_reflexivity(new_q->get_expr()))); - } - TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";); - } - } - } - - if (new_patterns.empty()) { - if (m_params.m_pi_warnings) { - warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", q->get_qid().str().c_str()); - } - TRACE("pi_failed", tout << mk_pp(q, m) << "\n";); - } - - if (new_patterns.empty() && new_body == q->get_expr()) { - cache_result(q, q, 0); - return; - } - - IF_IVERBOSE(10, - verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n"; - for (unsigned i = 0; i < new_patterns.size(); i++) - verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n"; - verbose_stream() << ")\n"; ); - - cache_result(q, new_q, pr); -} - -#endif #include "ast/pattern/database.h" @@ -881,7 +246,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) { // stating properties about these operators. family_id fid = c->get_family_id(); decl_kind k = c->get_decl_kind(); - if (!free_vars.empty() && + if (!free_vars.empty() && (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) { TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";); m_owner.add_candidate(new_node, free_vars, size); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 70eddcea1..997d5671e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -26,6 +26,7 @@ Notes: #include "math/automata/automaton.h" #include "ast/well_sorted.h" #include "ast/rewriter/var_subst.h" +#include "ast/rewriter/bool_rewriter.h" #include "math/automata/symbolic_automata_def.h" @@ -102,7 +103,6 @@ public: return sym_expr::mk_pred(fml, x->get_sort()); } } - sort* s = x->get_sort(); if (m.is_bool(s)) s = y->get_sort(); var_ref v(m.mk_var(0, s), m); @@ -112,7 +112,10 @@ public: return y; } if (m.is_true(fml2)) return x; - expr_ref fml(m.mk_and(fml1, fml2), m); + if (fml1 == fml2) return x; + bool_rewriter br(m); + expr_ref fml(m); + br.mk_and(fml1, fml2, fml); return sym_expr::mk_pred(fml, x->get_sort()); } virtual T mk_or(T x, T y) { @@ -120,12 +123,15 @@ public: x->get_char() == y->get_char()) { return x; } + if (x == y) return x; var_ref v(m.mk_var(0, x->get_sort()), m); expr_ref fml1 = x->accept(v); expr_ref fml2 = y->accept(v); if (m.is_false(fml1)) return y; if (m.is_false(fml2)) return x; - expr_ref fml(m.mk_or(fml1, fml2), m); + bool_rewriter br(m); + expr_ref fml(m); + br.mk_or(fml1, fml2, fml); return sym_expr::mk_pred(fml, x->get_sort()); } @@ -197,10 +203,10 @@ void re2automaton::set_solver(expr_solver* solver) { eautomaton* re2automaton::operator()(expr* e) { eautomaton* r = re2aut(e); - if (r) { - display_expr1 disp(m); + if (r) { r->compress(); - TRACE("seq", r->display(tout, disp);); + bool_rewriter br(m); + TRACE("seq", display_expr1 disp(m); r->display(tout, disp);); } return r; } diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 2f55d5cc2..12aa120b3 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -300,6 +300,16 @@ public: } } + bool is_sink_state(unsigned s) const { + if (is_final_state(s)) return false; + moves mvs; + get_moves_from(s, mvs); + for (move const& m : mvs) { + if (s != m.dst()) return false; + } + return true; + } + void add_init_to_final_states() { add_to_final_states(init()); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 22004ee78..1d58e2bb3 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -208,10 +208,8 @@ namespace smt { IF_VERBOSE(10, verbose_stream() << "quick checking quantifiers (unsat)...\n";); quick_checker mc(m_context); bool result = true; - ptr_vector::const_iterator it = m_quantifiers.begin(); - ptr_vector::const_iterator end = m_quantifiers.end(); - for (; it != end; ++it) - if (check_quantifier(*it) && mc.instantiate_unsat(*it)) + for (quantifier* q : m_quantifiers) + if (check_quantifier(q) && mc.instantiate_unsat(q)) result = false; if (m_params.m_qi_quick_checker == MC_UNSAT || !result) { m_qi_queue.instantiate(); @@ -220,9 +218,8 @@ namespace smt { // MC_NO_SAT is too expensive (it creates too many irrelevant instances). // we should use MBQI=true instead. IF_VERBOSE(10, verbose_stream() << "quick checking quantifiers (not sat)...\n";); - it = m_quantifiers.begin(); - for (; it != end; ++it) - if (check_quantifier(*it) && mc.instantiate_not_sat(*it)) + for (quantifier* q : m_quantifiers) + if (check_quantifier(q) && mc.instantiate_not_sat(q)) result = false; m_qi_queue.instantiate(); return result; @@ -493,10 +490,11 @@ namespace smt { virtual void assign_eh(quantifier * q) { m_active = true; + ast_manager& m = m_context->get_manager(); if (!m_fparams->m_ematching) { return; } - if (false && m_context->get_manager().is_rec_fun_def(q) && mbqi_enabled(q)) { + if (false && m.is_rec_fun_def(q) && mbqi_enabled(q)) { return; } bool has_unary_pattern = false; @@ -513,16 +511,20 @@ namespace smt { num_eager_multi_patterns++; for (unsigned i = 0, j = 0; i < num_patterns; i++) { app * mp = to_app(q->get_pattern(i)); - SASSERT(m_context->get_manager().is_pattern(mp)); + SASSERT(m.is_pattern(mp)); bool unary = (mp->get_num_args() == 1); - if (!unary && j >= num_eager_multi_patterns) { - TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n" + if (m.is_rec_fun_def(q) && i > 0) { + // add only the first pattern + TRACE("quantifier", tout << "skip recursive function body " << mk_ismt2_pp(mp, m) << "\n";); + } + else if (!unary && j >= num_eager_multi_patterns) { + TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n" << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";); m_lazy_mam->add_pattern(q, mp); } else { - TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";); + TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m) << "\n";); m_mam->add_pattern(q, mp); } if (!unary) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 461e9e8ee..44ce804e7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -151,9 +151,8 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { } void theory_seq::solution_map::display(std::ostream& out) const { - eqdep_map_t::iterator it = m_map.begin(), end = m_map.end(); - for (; it != end; ++it) { - out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n"; + for (auto const& kv : m_map) { + out << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value.first, m) << "\n"; } } @@ -187,9 +186,8 @@ void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) { } void theory_seq::exclusion_table::display(std::ostream& out) const { - table_t::iterator it = m_table.begin(), end = m_table.end(); - for (; it != end; ++it) { - out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n"; + for (auto const& kv : m_table) { + out << mk_pp(kv.first, m) << " != " << mk_pp(kv.second, m) << "\n"; } } @@ -214,6 +212,7 @@ theory_seq::theory_seq(ast_manager& m): m_trail_stack(*this), m_ls(m), m_rs(m), m_lhs(m), m_rhs(m), + m_res(m), m_atoms_qhead(0), m_new_solution(false), m_new_propagation(false), @@ -937,18 +936,14 @@ bool theory_seq::check_length_coherence0(expr* e) { bool theory_seq::check_length_coherence() { - obj_hashtable::iterator it = m_length.begin(), end = m_length.end(); #if 1 - for (; it != end; ++it) { - expr* e = *it; + for (expr* e : m_length) { if (check_length_coherence0(e)) { return true; } } - it = m_length.begin(); #endif - for (; it != end; ++it) { - expr* e = *it; + for (expr* e : m_length) { if (check_length_coherence(e)) { return true; } @@ -957,10 +952,9 @@ bool theory_seq::check_length_coherence() { } 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)) { + for (expr* e : m_length) { + if (fixed_length(e)) { found = true; } } @@ -2502,12 +2496,11 @@ void theory_seq::display(std::ostream & out) const { } if (!m_re2aut.empty()) { out << "Regex\n"; - obj_map::iterator it = m_re2aut.begin(), end = m_re2aut.end(); - for (; it != end; ++it) { - out << mk_pp(it->m_key, m) << "\n"; + for (auto const& kv : m_re2aut) { + out << mk_pp(kv.m_key, m) << "\n"; display_expr disp(m); - if (it->m_value) { - it->m_value->display(out, disp); + if (kv.m_value) { + kv.m_value->display(out, disp); } } } @@ -2521,9 +2514,7 @@ void theory_seq::display(std::ostream & out) const { } if (!m_length.empty()) { - obj_hashtable::iterator it = m_length.begin(), end = m_length.end(); - for (; it != end; ++it) { - expr* e = *it; + for (expr* e : m_length) { rational lo(-1), hi(-1); lower_bound(e, lo); upper_bound(e, hi); @@ -2636,6 +2627,12 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq int.to.str", m_stats.m_int_string); } +void theory_seq::init_search_eh() { + m_re2aut.reset(); + m_res.reset(); + m_automata.reset(); +} + void theory_seq::init_model(expr_ref_vector const& es) { expr_ref new_s(m); for (expr* e : es) { @@ -3397,7 +3394,6 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { literal lit = ctx.get_literal(n); if (!is_true) { e3 = m_util.re.mk_complement(e2); - is_true = true; lit.neg(); } eautomaton* a = get_automaton(e3); @@ -3416,26 +3412,17 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); literal_vector lits; - if (is_true) { - lits.push_back(~lit); - } + lits.push_back(~lit); + for (unsigned i = 0; i < states.size(); ++i) { - if (is_true) { - lits.push_back(mk_accept(e1, zero, e3, states[i])); - } - else { - literal nlit = ~lit; - propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i])); - } + lits.push_back(mk_accept(e1, zero, e3, states[i])); } - if (is_true) { - if (lits.size() == 2) { - propagate_lit(0, 1, &lit, lits[1]); - } - else { - TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";); - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - } + if (lits.size() == 2) { + propagate_lit(0, 1, &lit, lits[1]); + } + else { + TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";); + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } } @@ -4180,10 +4167,8 @@ eautomaton* theory_seq::get_automaton(expr* re) { TRACE("seq", result->display(tout, disp);); } m_automata.push_back(result); - m_trail_stack.push(push_back_vector >(m_automata)); - m_re2aut.insert(re, result); - m_trail_stack.push(insert_obj_map(m_re2aut, re)); + m_res.push_back(re); return result; } @@ -4264,6 +4249,10 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { if (m_util.str.is_length(idx)) return; SASSERT(m_autil.is_numeral(idx)); SASSERT(get_context().get_assignment(lit) == l_true); + if (aut->is_sink_state(src)) { + propagate_lit(0, 1, &lit, false_literal); + return; + } bool is_final = aut->is_final_state(src); if (is_final == is_acc) { propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx))); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b5a53e8e4..1f97697c2 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -328,6 +328,7 @@ namespace smt { // maintain automata with regular expressions. scoped_ptr_vector m_automata; obj_map m_re2aut; + expr_ref_vector m_res; // queue of asserted atoms ptr_vector m_atoms; @@ -361,6 +362,7 @@ namespace smt { virtual void collect_statistics(::statistics & st) const; virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & mg); + virtual void init_search_eh(); void init_model(expr_ref_vector const& es); // final check diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 21686fe64..595f8f7c6 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -115,8 +115,6 @@ void expr_dominators::extract_tree() { } } - - void expr_dominators::compile(expr * e) { reset(); m_root = e; @@ -130,7 +128,6 @@ void expr_dominators::compile(unsigned sz, expr * const* es) { compile(e); } - void expr_dominators::reset() { m_expr2post.reset(); m_post2expr.reset(); @@ -142,11 +139,8 @@ void expr_dominators::reset() { -// goes to header file: - - - -// implementation: +// ----------------------- +// dom_simplify_tactic tactic * dom_simplify_tactic::translate(ast_manager & m) { return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params); @@ -340,3 +334,109 @@ void dom_simplify_tactic::simplify_goal(goal& g) { } +// ---------------------- +// expr_substitution_simplifier + +bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) { + expr* tt; + if (!sign) { + update_substitution(t, 0); + } + else if (m.is_not(t, tt)) { + update_substitution(tt, 0); + } + else { + expr_ref nt(m.mk_not(t), m); + update_substitution(nt, 0); + } + return true; +} + + +bool expr_substitution_simplifier::is_gt(expr* lhs, expr* rhs) { + if (lhs == rhs) { + return false; + } + if (m.is_value(rhs)) { + return true; + } + SASSERT(is_ground(lhs) && is_ground(rhs)); + if (depth(lhs) > depth(rhs)) { + return true; + } + if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) { + app* l = to_app(lhs); + app* r = to_app(rhs); + if (l->get_decl()->get_id() != r->get_decl()->get_id()) { + return l->get_decl()->get_id() > r->get_decl()->get_id(); + } + if (l->get_num_args() != r->get_num_args()) { + return l->get_num_args() > r->get_num_args(); + } + for (unsigned i = 0; i < l->get_num_args(); ++i) { + if (l->get_arg(i) != r->get_arg(i)) { + return is_gt(l->get_arg(i), r->get_arg(i)); + } + } + UNREACHABLE(); + } + + return false; +} + +void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) { + expr* lhs, *rhs, *n1; + if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { + compute_depth(lhs); + compute_depth(rhs); + if (is_gt(lhs, rhs)) { + TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); + m_scoped_substitution.insert(lhs, rhs, pr); + return; + } + if (is_gt(rhs, lhs)) { + TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); + m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr)); + return; + } + TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); + } + if (m.is_not(n, n1)) { + m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); + } + else { + m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr)); + } +} + +void expr_substitution_simplifier::compute_depth(expr* e) { + ptr_vector todo; + todo.push_back(e); + while (!todo.empty()) { + e = todo.back(); + unsigned d = 0; + if (m_expr2depth.contains(e)) { + todo.pop_back(); + continue; + } + if (is_app(e)) { + app* a = to_app(e); + bool visited = true; + for (expr* arg : *a) { + unsigned d1 = 0; + if (m_expr2depth.find(arg, d1)) { + d = std::max(d, d1); + } + else { + visited = false; + todo.push_back(arg); + } + } + if (!visited) { + continue; + } + } + todo.pop_back(); + m_expr2depth.insert(e, d + 1); + } +} diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 9325f95f5..2fa79dd1d 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -21,6 +21,7 @@ Notes: #define DOM_SIMPLIFY_TACTIC_H_ #include "ast/ast.h" +#include "ast/expr_substitution.h" #include "tactic/tactic.h" @@ -129,4 +130,34 @@ public: virtual void cleanup(); }; +class expr_substitution_simplifier : public dom_simplify_tactic::simplifier { + ast_manager& m; + expr_substitution m_subst; + scoped_expr_substitution m_scoped_substitution; + obj_map m_expr2depth; + + // move from asserted_formulas to here.. + void compute_depth(expr* e); + bool is_gt(expr* lhs, expr* rhs); + unsigned depth(expr* e) { return m_expr2depth[e]; } + +public: + expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {} + virtual ~expr_substitution_simplifier() {} + virtual bool assert_expr(expr * t, bool sign); + + void update_substitution(expr* n, proof* pr); + + virtual void operator()(expr_ref& r) { r = m_scoped_substitution.find(r); } + + virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); } + + virtual simplifier * translate(ast_manager & m) { + SASSERT(m_subst.empty()); + return alloc(expr_substitution_simplifier, m); + } + + +}; + #endif