diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 70434435b..bff1e7dae 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -298,104 +298,6 @@ struct macro_manager::macro_expander_rw : public rewriter_tpl<macro_manager::mac
{}
};
-macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm):
- simplifier(m),
- m_macro_manager(mm) {
- // REMARK: theory simplifier should not be used by macro_expander...
- // is_arith_macro rewrites a quantifer such as:
- // forall (x Int) (= (+ x (+ (f x) 1)) 2)
- // into
- // forall (x Int) (= (f x) (+ 1 (* -1 x)))
- // The goal is to make simple macro detection detect the arith macro.
- // The arith simplifier will undo this transformation.
- // borrow_plugins(s);
- enable_ac_support(false);
-}
-
-macro_manager::macro_expander::~macro_expander() {
- // release_plugins();
-}
-
-void macro_manager::macro_expander::reduce1_quantifier(quantifier * q) {
- simplifier::reduce1_quantifier(q);
- // If a macro was expanded in a pattern, we must erase it since it may not be a valid pattern anymore.
- // The MAM assumes valid patterns, and it crashes if invalid patterns are provided.
- // For example, it will crash if the pattern does not contain all variables.
- //
- // Alternative solution: use pattern_validation to check if the pattern is still valid.
- // I'm not sure if this is a good solution, since the pattern may be meaningless after the macro expansion.
- // So, I'm just erasing them.
- expr * new_q_expr = 0;
- proof * new_q_pr = 0;
- get_cached(q, new_q_expr, new_q_pr);
- if (!is_quantifier(new_q_expr))
- return;
- quantifier * new_q = to_quantifier(new_q_expr);
- bool erase_patterns = false;
- if (q->get_num_patterns() != new_q->get_num_patterns() ||
- q->get_num_no_patterns() != new_q->get_num_no_patterns()) {
- erase_patterns = true;
- }
- else {
- for (unsigned i = 0; !erase_patterns && i < q->get_num_patterns(); i++) {
- if (q->get_pattern(i) != new_q->get_pattern(i))
- erase_patterns = true;
- }
- for (unsigned i = 0; !erase_patterns && i < q->get_num_no_patterns(); i++) {
- if (q->get_no_pattern(i) != new_q->get_no_pattern(i))
- erase_patterns = true;
- }
- }
- if (erase_patterns) {
- ast_manager & m = get_manager();
- expr * new_new_q = m.update_quantifier(new_q, 0, 0, 0, 0, new_q->get_expr());
- // we can use the same proof since new_new_q and new_q are identical modulo patterns/annotations
- cache_result(q, new_new_q, new_q_pr);
- }
-}
-
-bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref & p) {
- if (!is_app(_n))
- return false;
- app * n = to_app(_n);
- quantifier * q = 0;
- func_decl * d = n->get_decl();
- TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
- if (m_macro_manager.m_decl2macro.find(d, q)) {
- TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
- app * head = 0;
- expr * def = 0;
- m_macro_manager.get_head_def(q, d, head, def);
- unsigned num = n->get_num_args();
- SASSERT(head && def);
- ptr_buffer<expr> subst_args;
- subst_args.resize(num, 0);
- for (unsigned i = 0; i < num; i++) {
- var * v = to_var(head->get_arg(i));
- SASSERT(v->get_idx() < num);
- unsigned nidx = num - v->get_idx() - 1;
- SASSERT(subst_args[nidx] == 0);
- subst_args[nidx] = n->get_arg(i);
- }
- var_subst s(m);
- s(def, num, subst_args.c_ptr(), r);
- if (m.proofs_enabled()) {
- expr_ref instance(m);
- s(q->get_expr(), num, subst_args.c_ptr(), instance);
- proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
- proof * q_pr = 0;
- m_macro_manager.m_decl2macro_pr.find(d, q_pr);
- SASSERT(q_pr != 0);
- proof * prs[2] = { qi_pr, q_pr };
- p = m.mk_unit_resolution(2, prs);
- }
- else {
- p = 0;
- }
- return true;
- }
- return false;
-}
void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) {
if (has_macros()) {
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 98e242cd8..71864a699 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -60,17 +60,6 @@ class macro_manager {
struct macro_expander_cfg;
struct macro_expander_rw;
- class macro_expander : public simplifier {
- protected:
- macro_manager & m_macro_manager;
- virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
- virtual void reduce1_quantifier(quantifier * q);
- public:
- macro_expander(ast_manager & m, macro_manager & mm);
- ~macro_expander();
- };
- friend class macro_expander;
-
public:
macro_manager(ast_manager & m);
~macro_manager();
diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index d97c2f094..94a90d829 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -16,15 +16,17 @@ Author:
Revision History:
--*/
+
+#include "util/warning.h"
#include "ast/pattern/pattern_inference.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
-#include "util/warning.h"
#include "ast/arith_decl_plugin.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/well_sorted.h"
#include "ast/for_each_expr.h"
+#include "ast/rewriter/rewriter_def.h"
void smaller_pattern::save(expr * p1, expr * p2) {
expr_pair e(p1, p2);
@@ -87,7 +89,7 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) {
return process(p1, p2);
}
-pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params):
+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()),
@@ -105,7 +107,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params &
enable_ac_support(false);
}
-void pattern_inference::collect::operator()(expr * n, unsigned num_bindings) {
+void pattern_inference_old::collect::operator()(expr * n, unsigned num_bindings) {
SASSERT(m_info.empty());
SASSERT(m_todo.empty());
SASSERT(m_cache.empty());
@@ -125,7 +127,7 @@ void pattern_inference::collect::operator()(expr * n, unsigned num_bindings) {
reset();
}
-inline void pattern_inference::collect::visit(expr * n, unsigned delta, bool & visited) {
+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);
@@ -133,7 +135,7 @@ inline void pattern_inference::collect::visit(expr * n, unsigned delta, bool & v
}
}
-bool pattern_inference::collect::visit_children(expr * n, unsigned delta) {
+bool pattern_inference_old::collect::visit_children(expr * n, unsigned delta) {
bool visited = true;
unsigned i;
switch (n->get_kind()) {
@@ -153,13 +155,13 @@ bool pattern_inference::collect::visit_children(expr * n, unsigned delta) {
return visited;
}
-inline void pattern_inference::collect::save(expr * n, unsigned delta, info * i) {
+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::collect::save_candidate(expr * n, unsigned delta) {
+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();
@@ -247,14 +249,14 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
}
-void pattern_inference::collect::reset() {
+void pattern_inference_old::collect::reset() {
m_cache.reset();
std::for_each(m_info.begin(), m_info.end(), delete_proc<info>());
m_info.reset();
SASSERT(m_todo.empty());
}
-void pattern_inference::add_candidate(app * n, uint_set const & free_vars, unsigned size) {
+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;
@@ -271,7 +273,7 @@ void pattern_inference::add_candidate(app * n, uint_set const & free_vars, unsig
\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::filter_looping_patterns(ptr_vector<app> & result) {
+void pattern_inference_old::filter_looping_patterns(ptr_vector<app> & result) {
unsigned num = m_candidates.size();
for (unsigned i1 = 0; i1 < num; i1++) {
app * n1 = m_candidates.get(i1);
@@ -310,7 +312,7 @@ void pattern_inference::filter_looping_patterns(ptr_vector<app> & result) {
-inline void pattern_inference::contains_subpattern::save(expr * n) {
+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)) {
@@ -319,7 +321,7 @@ inline void pattern_inference::contains_subpattern::save(expr * n) {
}
}
-bool pattern_inference::contains_subpattern::operator()(expr * n) {
+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);
@@ -360,7 +362,7 @@ bool pattern_inference::contains_subpattern::operator()(expr * n) {
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::contains_subpattern(expr * n) {
+inline bool pattern_inference_old::contains_subpattern(expr * n) {
return m_contains_subpattern(n);
}
@@ -372,18 +374,15 @@ inline bool pattern_inference::contains_subpattern(expr * n) {
Remark: Every pattern p in patterns is also a member of
m_pattern_map.
*/
-void pattern_inference::filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result) {
- ptr_vector<app>::const_iterator it = patterns.begin();
- ptr_vector<app>::const_iterator end = patterns.end();
- for (; it != end; ++it) {
- app * curr = *it;
+void pattern_inference_old::filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result) {
+ for (app * curr : patterns) {
if (!contains_subpattern(curr))
result.push_back(curr);
}
}
-bool pattern_inference::pattern_weight_lt::operator()(expr * n1, expr * n2) const {
+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);
@@ -401,13 +400,10 @@ bool pattern_inference::pattern_weight_lt::operator()(expr * n1, expr * n2) cons
variables, then it is copied to remaining_candidate_patterns. The
new patterns are stored in result.
*/
-void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
+void pattern_inference_old::candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
ptr_vector<app> & remaining_candidate_patterns,
app_ref_buffer & result) {
- ptr_vector<app>::const_iterator it = candidate_patterns.begin();
- ptr_vector<app>::const_iterator end = candidate_patterns.end();
- for (; it != end; ++it) {
- app * candidate = *it;
+ 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) {
@@ -425,7 +421,7 @@ void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candid
// HACK: limit the number of case-splits:
#define MAX_SPLITS 32
-void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
+void pattern_inference_old::candidates2multi_patterns(unsigned max_num_patterns,
ptr_vector<app> const & candidate_patterns,
app_ref_buffer & result) {
SASSERT(!candidate_patterns.empty());
@@ -469,21 +465,19 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
}
}
-void pattern_inference::reset_pre_patterns() {
+void pattern_inference_old::reset_pre_patterns() {
std::for_each(m_pre_patterns.begin(), m_pre_patterns.end(), delete_proc<pre_pattern>());
m_pre_patterns.reset();
}
#ifdef _TRACE
static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
- ptr_vector<app>::const_iterator it = v.begin();
- ptr_vector<app>::const_iterator end = v.end();
- for (; it != end; ++it)
- out << mk_pp(*it, m) << "\n";
+ for (app * e : v)
+ out << mk_pp(e, m) << "\n";
}
#endif
-bool pattern_inference::is_forbidden(app * n) const {
+bool pattern_inference_old::is_forbidden(app * n) const {
func_decl const * decl = n->get_decl();
if (is_ground(n))
return false;
@@ -499,14 +493,11 @@ bool pattern_inference::is_forbidden(app * n) const {
return false;
}
-bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patterns, app_ref_buffer & result) {
+bool pattern_inference_old::has_preferred_patterns(ptr_vector<app> & candidate_patterns, app_ref_buffer & result) {
if (m_preferred.empty())
return false;
bool found = false;
- ptr_vector<app>::const_iterator it = candidate_patterns.begin();
- ptr_vector<app>::const_iterator end = candidate_patterns.end();
- for (; it != end; ++it) {
- app * candidate = *it;
+ 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;
@@ -521,7 +512,7 @@ bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patte
return found;
}
-void pattern_inference::mk_patterns(unsigned num_bindings,
+void pattern_inference_old::mk_patterns(unsigned num_bindings,
expr * n,
unsigned num_no_patterns,
expr * const * no_patterns,
@@ -578,7 +569,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
#include "ast/pattern/database.h"
-void pattern_inference::reduce1_quantifier(quantifier * q) {
+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);
@@ -739,13 +730,626 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
}
-#if 0
-// unused
-static void dump_expr_vector(std::ostream & out, ptr_vector<expr> const & v, ast_manager & m) {
- ptr_vector<expr>::const_iterator it = v.begin();
- ptr_vector<expr>::const_iterator end = v.end();
- for (; it != end; ++it)
- out << mk_pp(*it, m) << "\n";
-}
-#endif
+pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_params & params):
+ m(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);
+}
+
+void pattern_inference_cfg::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_cfg::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_cfg::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_cfg::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_cfg::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<expr> 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_cfg::collect::reset() {
+ m_cache.reset();
+ std::for_each(m_info.begin(), m_info.end(), delete_proc<info>());
+ m_info.reset();
+ SASSERT(m_todo.empty());
+}
+
+void pattern_inference_cfg::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_cfg::filter_looping_patterns(ptr_vector<app> & 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_cfg::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_cfg::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_cfg::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_cfg::filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result) {
+ for (app * curr : patterns) {
+ if (!contains_subpattern(curr))
+ result.push_back(curr);
+ }
+}
+
+
+bool pattern_inference_cfg::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_cfg::candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
+ ptr_vector<app> & 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_cfg::candidates2multi_patterns(unsigned max_num_patterns,
+ ptr_vector<app> 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_cfg::reset_pre_patterns() {
+ std::for_each(m_pre_patterns.begin(), m_pre_patterns.end(), delete_proc<pre_pattern>());
+ m_pre_patterns.reset();
+}
+
+
+bool pattern_inference_cfg::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_cfg::has_preferred_patterns(ptr_vector<app> & 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_cfg::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();
+}
+
+
+bool pattern_inference_cfg::reduce_quantifier(
+ quantifier * q,
+ expr * new_body,
+ expr * const *, // new_patterns
+ expr * const * new_no_patterns,
+ expr_ref & result,
+ proof_ref & result_pr) {
+
+ TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
+ if (!q->is_forall()) {
+ return false;
+ }
+
+ int weight = q->get_weight();
+
+ if (m_params.m_pi_use_database) {
+ app_ref_vector new_patterns(m);
+ m_database.initialize(g_pattern_database);
+ unsigned new_weight;
+ if (m_database.match_quantifier(q, new_patterns, new_weight)) {
+ DEBUG_CODE(for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); });
+ 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";);
+ result = 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());
+ result = 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";);
+ }
+ if (m.fine_grain_proofs())
+ result_pr = m.mk_rewrite(q, new_q);
+ return true;
+ }
+ }
+
+ if (q->get_num_patterns() > 0) {
+ return false;
+ }
+
+ if (m_params.m_pi_nopat_weight >= 0)
+ weight = m_params.m_pi_nopat_weight;
+
+ SASSERT(q->get_num_patterns() == 0);
+
+ if (m_params.m_pi_arith == AP_CONSERVATIVE)
+ m_forbidden.push_back(m_afid);
+
+ app_ref_buffer new_patterns(m);
+ unsigned num_no_patterns = q->get_num_no_patterns();
+ mk_patterns(q->get_num_decls(), new_body, num_no_patterns, new_no_patterns, new_patterns);
+
+ if (new_patterns.empty() && num_no_patterns > 0) {
+ 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<bool> l1(m_block_loop_patterns, false); // allow looping patterns
+ mk_patterns(q->get_num_decls(), new_body, num_no_patterns, new_no_patterns, new_patterns);
+ if (!new_patterns.empty()) {
+ weight = std::max(weight, static_cast<int>(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=<val>).",
+ q->get_qid().str().c_str(), weight);
+ }
+ }
+ }
+ }
+
+ if (m_params.m_pi_arith != AP_NO && new_patterns.empty()) {
+ if (new_patterns.empty()) {
+ flet<bool> l1(m_nested_arith_only, false); // try to find a non-nested arith pattern
+ flet<bool> l2(m_block_loop_patterns, false); // allow looping patterns
+ mk_patterns(q->get_num_decls(), new_body, num_no_patterns, new_no_patterns, new_patterns);
+ if (!new_patterns.empty()) {
+ weight = std::max(weight, static_cast<int>(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=<val>).",
+ q->get_qid().str().c_str(), weight);
+ }
+ // verbose_stream() << mk_pp(q, m) << "\n";
+ }
+ }
+ }
+
+ quantifier_ref new_q(m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body), m);
+ if (weight != q->get_weight())
+ new_q = m.update_quantifier_weight(new_q, weight);
+ if (m.fine_grain_proofs()) {
+ proof* new_body_pr = m.mk_reflexivity(new_body);
+ result_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 * result2 = to_quantifier(new_expr);
+ if (result2 != new_q) {
+ mk_patterns(result2->get_num_decls(), result2->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(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr());
+ if (m.fine_grain_proofs()) {
+ result_pr = m.mk_transitivity(new_pr, m.mk_quant_intro(result2, 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()) {
+ return false;
+ }
+
+ result = new_q;
+
+ 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"; );
+
+ return true;
+}
+
+pattern_inference_rw::pattern_inference_rw(ast_manager& m, pattern_inference_params & params):
+ rewriter_tpl<pattern_inference_cfg>(m, m.proofs_enabled(), m_cfg),
+ m_cfg(m, params)
+{}
diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index a138d1033..7b0ec9cfe 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -21,6 +21,7 @@ Revision History:
#include "ast/ast.h"
#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/rewriter.h"
#include "ast/pattern/pattern_inference_params.h"
#include "util/vector.h"
#include "util/uint_set.h"
@@ -60,7 +61,7 @@ public:
bool operator()(unsigned num_bindings, expr * p1, expr * p2);
};
-class pattern_inference : public simplifier {
+class pattern_inference_old : public simplifier {
pattern_inference_params & m_params;
family_id m_bfid;
family_id m_afid;
@@ -88,7 +89,7 @@ class pattern_inference : public simplifier {
typedef obj_map<expr, info> expr2info;
- expr2info m_candidates_info; // candidate -> set of free vars + size
+ expr2info m_candidates_info; // candidate -> set of free vars + size
app_ref_vector m_candidates;
ptr_vector<app> m_tmp1;
@@ -136,7 +137,7 @@ class pattern_inference : public simplifier {
};
ast_manager & m;
- pattern_inference & m_owner;
+ pattern_inference_old & m_owner;
family_id m_afid;
unsigned m_num_bindings;
typedef map<entry, info *, obj_hash<entry>, default_eq<entry> > cache;
@@ -150,7 +151,7 @@ class pattern_inference : public simplifier {
void save_candidate(expr * n, unsigned delta);
void reset();
public:
- collect(ast_manager & m, pattern_inference & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
+ collect(ast_manager & m, pattern_inference_old & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
void operator()(expr * n, unsigned num_bindings);
};
@@ -165,12 +166,12 @@ class pattern_inference : public simplifier {
void filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result);
class contains_subpattern {
- pattern_inference & m_owner;
+ pattern_inference_old & m_owner;
nat_set m_already_processed;
ptr_vector<expr> m_todo;
void save(expr * n);
public:
- contains_subpattern(pattern_inference & owner):
+ contains_subpattern(pattern_inference_old & owner):
m_owner(owner) {}
bool operator()(expr * n);
};
@@ -217,7 +218,7 @@ class pattern_inference : public simplifier {
virtual void reduce1_quantifier(quantifier * q);
public:
- pattern_inference(ast_manager & m, pattern_inference_params & params);
+ pattern_inference_old(ast_manager & m, pattern_inference_params & params);
void register_forbidden_family(family_id fid) {
SASSERT(fid != m_bfid);
@@ -244,5 +245,201 @@ public:
bool is_forbidden(app * n) const;
};
+class pattern_inference_cfg : public default_rewriter_cfg {
+ ast_manager& m;
+ pattern_inference_params & m_params;
+ family_id m_bfid;
+ family_id m_afid;
+ svector<family_id> m_forbidden;
+ obj_hashtable<func_decl> m_preferred;
+ smaller_pattern m_le;
+ unsigned m_num_bindings;
+ unsigned m_num_no_patterns;
+ expr * const * m_no_patterns;
+ bool m_nested_arith_only;
+ bool m_block_loop_patterns;
+
+ struct info {
+ uint_set m_free_vars;
+ unsigned m_size;
+ info(uint_set const & vars, unsigned size):
+ m_free_vars(vars),
+ m_size(size) {
+ }
+ info():
+ m_free_vars(),
+ m_size(0) {
+ }
+ };
+
+ typedef obj_map<expr, info> expr2info;
+
+ expr2info m_candidates_info; // candidate -> set of free vars + size
+ app_ref_vector m_candidates;
+
+ ptr_vector<app> m_tmp1;
+ ptr_vector<app> m_tmp2;
+ ptr_vector<app> m_todo;
+
+ // Compare candidates patterns based on their usefulness
+ // p1 < p2 if
+ // - p1 has more free variables than p2
+ // - p1 and p2 has the same number of free variables,
+ // and p1 is smaller than p2.
+ struct pattern_weight_lt {
+ expr2info & m_candidates_info;
+ pattern_weight_lt(expr2info & i):
+ m_candidates_info(i) {
+ }
+ bool operator()(expr * n1, expr * n2) const;
+ };
+
+ pattern_weight_lt m_pattern_weight_lt;
+
+ //
+ // Functor for collecting candidates.
+ //
+ class collect {
+ struct entry {
+ expr * m_node;
+ unsigned m_delta;
+ entry():m_node(0), m_delta(0) {}
+ entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
+ unsigned hash() const {
+ return hash_u_u(m_node->get_id(), m_delta);
+ }
+ bool operator==(entry const & e) const {
+ return m_node == e.m_node && m_delta == e.m_delta;
+ }
+ };
+
+ struct info {
+ expr_ref m_node;
+ uint_set m_free_vars;
+ unsigned m_size;
+ info(ast_manager & m, expr * n, uint_set const & vars, unsigned sz):
+ m_node(n, m), m_free_vars(vars), m_size(sz) {}
+ };
+
+ ast_manager & m;
+ pattern_inference_cfg & m_owner;
+ family_id m_afid;
+ unsigned m_num_bindings;
+ typedef map<entry, info *, obj_hash<entry>, default_eq<entry> > cache;
+ cache m_cache;
+ ptr_vector<info> m_info;
+ svector<entry> m_todo;
+
+ void visit(expr * n, unsigned delta, bool & visited);
+ bool visit_children(expr * n, unsigned delta);
+ void save(expr * n, unsigned delta, info * i);
+ void save_candidate(expr * n, unsigned delta);
+ void reset();
+ public:
+ collect(ast_manager & m, pattern_inference_cfg & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
+ void operator()(expr * n, unsigned num_bindings);
+ };
+
+ collect m_collect;
+
+ void add_candidate(app * n, uint_set const & s, unsigned size);
+
+ void filter_looping_patterns(ptr_vector<app> & result);
+
+ bool has_preferred_patterns(ptr_vector<app> & candidate_patterns, app_ref_buffer & result);
+
+ void filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result);
+
+ class contains_subpattern {
+ pattern_inference_cfg & m_owner;
+ nat_set m_already_processed;
+ ptr_vector<expr> m_todo;
+ void save(expr * n);
+ public:
+ contains_subpattern(pattern_inference_cfg & owner):
+ m_owner(owner) {}
+ bool operator()(expr * n);
+ };
+
+ contains_subpattern m_contains_subpattern;
+
+ bool contains_subpattern(expr * n);
+
+ struct pre_pattern {
+ ptr_vector<app> m_exprs; // elements of the pattern.
+ uint_set m_free_vars; // set of free variables in m_exprs
+ unsigned m_idx; // idx of the next candidate to process.
+ pre_pattern():
+ m_idx(0) {
+ }
+ };
+
+ ptr_vector<pre_pattern> m_pre_patterns;
+ expr_pattern_match m_database;
+
+ void candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
+ ptr_vector<app> & remaining_candidate_patterns,
+ app_ref_buffer & result);
+
+ void candidates2multi_patterns(unsigned max_num_patterns,
+ ptr_vector<app> const & candidate_patterns,
+ app_ref_buffer & result);
+
+ void reset_pre_patterns();
+
+ /**
+ \brief All minimal unary patterns (i.e., expressions that
+ contain all bound variables) are copied to result. If there
+ are unary patterns, then at most num_extra_multi_patterns multi
+ patterns are created. If there are no unary pattern, then at
+ most 1 + num_extra_multi_patterns multi_patterns are created.
+ */
+ void mk_patterns(unsigned num_bindings, // IN number of bindings.
+ expr * n, // IN node where the patterns are going to be extracted.
+ unsigned num_no_patterns, // IN num. patterns that should not be used.
+ expr * const * no_patterns, // IN patterns that should not be used.
+ app_ref_buffer & result); // OUT result
+
+public:
+ pattern_inference_cfg(ast_manager & m, pattern_inference_params & params);
+
+ void register_forbidden_family(family_id fid) {
+ SASSERT(fid != m_bfid);
+ m_forbidden.push_back(fid);
+ }
+
+ /**
+ \brief Register f as a preferred function symbol. The inference algorithm
+ gives preference to patterns rooted by this kind of function symbol.
+ */
+ void register_preferred(func_decl * f) {
+ m_preferred.insert(f);
+ }
+
+ bool reduce_quantifier(quantifier * old_q,
+ expr * new_body,
+ expr * const * new_patterns,
+ expr * const * new_no_patterns,
+ expr_ref & result,
+ proof_ref & result_pr);
+
+ void register_preferred(unsigned num, func_decl * const * fs) { for (unsigned i = 0; i < num; i++) register_preferred(fs[i]); }
+
+ bool is_forbidden(func_decl const * decl) const {
+ family_id fid = decl->get_family_id();
+ if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
+ return true;
+ return std::find(m_forbidden.begin(), m_forbidden.end(), fid) != m_forbidden.end();
+ }
+
+ bool is_forbidden(app * n) const;
+};
+
+class pattern_inference_rw : public rewriter_tpl<pattern_inference_cfg> {
+ pattern_inference_cfg m_cfg;
+public:
+ pattern_inference_rw(ast_manager& m, pattern_inference_params & params);
+};
+
#endif /* PATTERN_INFERENCE_H_ */
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 7eb2284c0..cfb998a32 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -70,7 +70,7 @@ namespace datalog {
if (q->get_num_patterns() == 0) {
proof_ref new_pr(m);
pattern_inference_params params;
- pattern_inference infer(m, params);
+ pattern_inference_old infer(m, params);
infer(q, qe, new_pr);
q = to_quantifier(qe);
}
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 7eb189ebf..26265a6f8 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -21,6 +21,7 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
+#include "ast/rewriter/rewriter_def.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/array_simplifier_plugin.h"
#include "ast/simplifier/datatype_simplifier_plugin.h"
@@ -517,7 +518,7 @@ void asserted_formulas::reduce_and_solve() {
void asserted_formulas::infer_patterns() {
IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
TRACE("before_pattern_inference", display(tout););
- pattern_inference infer(m, m_params);
+ pattern_inference_rw infer(m, m_params);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 725c9fc51..0a75ff700 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -207,8 +207,10 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, fun
by their interpretations.
*/
void proto_model::cleanup() {
+ TRACE("model_bug", model_v2_pp(tout, *this););
func_decl_set found_aux_fs;
for (auto const& kv : m_finterp) {
+ TRACE("model_bug", tout << kv.m_key->get_name() << "\n";);
func_interp * fi = kv.m_value;
cleanup_func_interp(fi, found_aux_fs);
}
@@ -365,7 +367,7 @@ void proto_model::complete_partial_funcs() {
}
model * proto_model::mk_model() {
- TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this););
+ TRACE("proto_model", model_v2_pp(tout << "mk_model\n", *this););
model * m = alloc(model, m_manager);
for (auto const& kv : m_interp) {
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 953afd4b7..5848fac62 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -19,7 +19,6 @@ Revision History:
#include "util/ref_util.h"
#include "ast/for_each_expr.h"
-#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt2_pp.h"
#include "smt/smt_context.h"