mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

prune dead states from automata

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-31 07:33:55 -07:00
parent e8198bbbe3
commit 059bad909a
5 changed files with 70 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/simplifier/base_simplifier.h
View file

@ -37,6 +37,7 @@ protected:
tout << mk_pp(n, m) << "\n";
tout << mk_pp(r, m) << "\n";
tout << mk_pp(p, m) << "\n";);
TRACE("cache", tout << mk_pp(n, m) << " -> " << mk_pp(r, m) << "\n";);
SASSERT(is_rewrite_proof(n, r, p));
}
void reset_cache() { m_cache.reset(); }

9
src/ast/simplifier/simplifier.cpp
View file

@ -591,8 +591,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
if (m_ac_cache.find(to_app(arg), new_arg)) {
SASSERT(new_arg != 0);
new_args.push_back(new_arg);
if (arg != new_arg)
if (arg != new_arg) {
TRACE("ac", tout << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
has_new_arg = true;
}
if (m.fine_grain_proofs()) {
proof * pr = 0;
m_ac_pr_cache.find(to_app(arg), pr);
@ -610,8 +612,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
proof * pr;
get_cached(arg, new_arg, pr);
new_args.push_back(new_arg);
if (arg != new_arg)
if (arg != new_arg) {
TRACE("ac", tout << "cached: " << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
has_new_arg = true;
}
if (m.fine_grain_proofs() && pr != 0)
new_arg_prs.push_back(pr);
}
@ -627,6 +631,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
else {
app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
m_ac_cache.insert(curr, new_curr);
TRACE("ac", tout << mk_pp(curr, m) << " -> " << mk_pp(new_curr, m) << "\n";);
if (m.fine_grain_proofs()) {
proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
m_ac_pr_cache.insert(curr, p);

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

@ -25,6 +25,7 @@ Revision History:
#include "util/util.h"
#include "util/vector.h"
#include "util/uint_set.h"
#include "util/trace.h"
template<class T>
class default_value_manager {
@ -383,12 +384,12 @@ public:
else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
moves const& mvs = m_delta[dst];
moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) {
mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t()));
for (move const& mv : mvs) {
mvs1.push_back(move(m, src, mv.dst(), mv.t()));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(dst, mvs1[k].dst(), mvs1[k].t());
add(mvs1[k]);
for (move const& mv : mvs1) {
remove(dst, mv.dst(), mv.t());
add(mv);
}
}
//
@ -401,13 +402,13 @@ public:
unsigned_vector src0s;
moves const& mvs = m_delta_inv[dst];
moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) {
SASSERT(mvs[k].is_epsilon());
mvs1.push_back(move(m, mvs[k].src(), dst1, t));
for (move const& mv1 : mvs) {
SASSERT(mv1.is_epsilon());
mvs1.push_back(move(m, mv1.src(), dst1, t));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(mvs1[k].src(), dst, 0);
add(mvs1[k]);
for (move const& mv1 : mvs1) {
remove(mv1.src(), dst, 0);
add(mv1);
}
remove(dst, dst1, t);
--j;
@ -419,12 +420,12 @@ public:
else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
moves const& mvs = m_delta_inv[src];
moves mvs1;
for (unsigned k = 0; k < mvs.size(); ++k) {
mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
for (move const& mv : mvs) {
mvs1.push_back(move(m, mv.src(), dst, mv.t()));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(mvs1[k].src(), src, mvs1[k].t());
add(mvs1[k]);
for (move const& mv : mvs1) {
remove(mv.src(), src, mv.t());
add(mv);
}
}
else {
@ -447,6 +448,7 @@ public:
break;
}
}
sinkify_dead_states();
}
bool is_sequence(unsigned& length) const {
@ -564,6 +566,40 @@ public:
}
private:
void sinkify_dead_states() {
uint_set dead_states;
for (unsigned i = 0; i < m_delta.size(); ++i) {
if (!m_final_states.contains(i)) {
dead_states.insert(i);
}
}
bool change = true;
unsigned_vector to_remove;
while (change) {
change = false;
to_remove.reset();
for (unsigned s : dead_states) {
moves const& mvs = m_delta[s];
for (move const& mv : mvs) {
if (!dead_states.contains(mv.dst())) {
to_remove.push_back(s);
break;
}
}
}
change = !to_remove.empty();
for (unsigned s : to_remove) {
dead_states.remove(s);
}
to_remove.reset();
}
TRACE("seq", tout << "remove: " << dead_states << "\n";);
for (unsigned s : dead_states) {
CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";);
m_delta[s].reset();
}
}
void remove_dead_states() {
unsigned_vector remap;
for (unsigned i = 0; i < m_delta.size(); ++i) {
@ -669,8 +705,8 @@ private:
}
static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
final.push_back(a.m_final_states[i]+offset);
for (unsigned s : a.m_final_states) {
final.push_back(s+offset);
}
}

3
src/smt/asserted_formulas.cpp
View file

@ -645,7 +645,7 @@ void asserted_formulas::propagate_values() {
new_prs2.push_back(pr);
}
}
TRACE("propagate_values", tout << "found: " << found << "\n";);
TRACE("propagate_values", tout << "found: " << found << "\n" << new_exprs2 << "\n";);
// If C is not empty, then reduce R using the updated simplifier cache with entries
// x -> n for each constraint 'x = n' in C.
if (found) {
@ -656,6 +656,7 @@ void asserted_formulas::propagate_values() {
expr_ref new_n(m);
proof_ref new_pr(m);
m_simplifier(n, new_n, new_pr);
TRACE("propagate_values", tout << mk_pp(n, m) << " -> " << new_n << "\n";);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs1, new_prs1);
}

7
src/smt/smt_quantifier.cpp
View file

@ -492,6 +492,7 @@ namespace smt {
virtual void assign_eh(quantifier * q) {
m_active = true;
ast_manager& m = m_context->get_manager();
if (!m_fparams->m_ematching) {
return;
}
@ -514,7 +515,11 @@ namespace smt {
app * mp = to_app(q->get_pattern(i));
SASSERT(m_context->get_manager().is_pattern(mp));
bool unary = (mp->get_num_args() == 1);
if (!unary && j >= num_eager_multi_patterns) {
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_context->get_manager()) << "\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";);