mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

update to theory_seq following examples from PJLJ

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-30 14:00:01 -07:00
parent 4452ff9884
commit 009e94d188
9 changed files with 213 additions and 707 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/expr_substitution.h
View file

@ -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); }

637
src/ast/pattern/pattern_inference.cpp
View file

@ -97,641 +97,6 @@ static void dump_app_vector(std::ostream & out, ptr_vector<app> 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<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_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_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<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_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<app> const & patterns, ptr_vector<app> & 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<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_old::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_old::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_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<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_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<expr> 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<bool> 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<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, new_no_patterns.size(), new_no_patterns.c_ptr(), 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);
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);

18
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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;
}

10
src/math/automata/automaton.h
View file

@ -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());
}

26
src/smt/smt_quantifier.cpp
View file

@ -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<quantifier>::const_iterator it = m_quantifiers.begin();
ptr_vector<quantifier>::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)

79
src/smt/theory_seq.cpp
View file

@ -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<expr>::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<expr>::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<expr, eautomaton*>::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<expr>::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<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
m_re2aut.insert(re, result);
m_trail_stack.push(insert_obj_map<theory_seq, expr, eautomaton*>(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)));

2
src/smt/theory_seq.h
View file

@ -328,6 +328,7 @@ namespace smt {
// maintain automata with regular expressions.
scoped_ptr_vector<eautomaton> m_automata;
obj_map<expr, eautomaton*> m_re2aut;
expr_ref_vector m_res;
// queue of asserted atoms
ptr_vector<expr> 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

116
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -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<expr> 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);
}
}

31
src/tactic/core/dom_simplify_tactic.h
View file

@ -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<expr, unsigned> 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