mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #4873

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-12 16:03:48 -08:00
parent f71204c222
commit 7fe8298479
2 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/ast/macros/quasi_macros.cpp
View file

@ -158,8 +158,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
if (is_forall(e)) {
quantifier * q = to_quantifier(e);
expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
if ((m.is_eq(qe, lhs, rhs))) {
if (m.is_eq(qe, lhs, rhs)) {
if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs);
@ -293,24 +292,22 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
for (unsigned i = 0 ; i < n ; i++)
tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; );
for (unsigned i = 0; i < n; i++)
tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; );
bool res = false;
m_occurrences.reset();
// Find out how many non-ground appearances for each uninterpreted function there are
for ( unsigned i = 0 ; i < n ; i++ )
for (unsigned i = 0 ; i < n ; i++)
find_occurrences(exprs[i].get_fml());
TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
for (occurrences_map::iterator it = m_occurrences.begin();
it != m_occurrences.end();
it++)
tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
for (auto kv : m_occurrences)
tout << kv.m_key->get_name() << ": " << kv.m_value << std::endl; );
// Find all macros
for ( unsigned i = 0 ; i < n ; i++ ) {
for (unsigned i = 0 ; i < n ; i++) {
app_ref a(m);
expr_ref t(m);
quantifier_ref macro(m);
@ -370,6 +367,7 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<j
}
bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
TRACE("quasi_macros", m_macro_manager.display(tout););
if (find_macros(n, fmls)) {
apply_macros(n, fmls, new_fmls);
return true;

2
src/smt/asserted_formulas.h
View file

@ -88,7 +88,7 @@ class asserted_formulas {
public:
find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
void operator()() override { af.find_macros_core(); }
bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
bool should_apply() const override { return (af.m_smt_params.m_quasi_macros || af.m_smt_params.m_macro_finder) && af.has_quantifiers(); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};