From 059bad909ad4b5f0b70378970475149822cccaa6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 31 Aug 2017 07:33:55 -0700
Subject: [PATCH] prune dead states from automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/simplifier/base_simplifier.h | 1 +
src/ast/simplifier/simplifier.cpp | 9 +++-
src/math/automata/automaton.h | 72 +++++++++++++++++++++-------
src/smt/asserted_formulas.cpp | 3 +-
src/smt/smt_quantifier.cpp | 7 ++-
5 files changed, 70 insertions(+), 22 deletions(-)
diff --git a/src/ast/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h
index 73a04d605..87c372636 100644
--- a/src/ast/simplifier/base_simplifier.h
+++ b/src/ast/simplifier/base_simplifier.h
@@ -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(); }
diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp
index c02753440..e7f842203 100644
--- a/src/ast/simplifier/simplifier.cpp
+++ b/src/ast/simplifier/simplifier.cpp
@@ -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);
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 12aa120b3..07d6d31ec 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -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);
}
}
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index dabae9fbd..d9630c979 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -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);
}
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 84ed7c8cd..0492aff23 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -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";);