mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

add pre-filter for F* use case

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-10 17:56:48 -07:00
parent 8efa3c8ade
commit 994dab8eb6
1 changed files with 37 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/ast/rewriter/th_rewriter.cpp
View file

@ -37,6 +37,7 @@ Notes:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "ast/for_each_expr.h"
namespace { namespace {
struct th_rewriter_cfg : public default_rewriter_cfg { struct th_rewriter_cfg : public default_rewriter_cfg {
@ -60,6 +61,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_substitution * m_subst = nullptr; expr_substitution * m_subst = nullptr;
unsigned long long m_max_memory; // in bytes unsigned long long m_max_memory; // in bytes
bool m_new_subst = false; bool m_new_subst = false;
expr_fast_mark1 m_visited;
expr_mark m_marks;
bool m_new_mark = false;
unsigned m_max_steps = UINT_MAX; unsigned m_max_steps = UINT_MAX;
bool m_pull_cheap_ite = true; bool m_pull_cheap_ite = true;
bool m_flat = true; bool m_flat = true;
@ -692,11 +696,43 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return result; return result;
} }
/**
* Apply substitution on pattern expressions.
* It happens only very rarely that this operation has an effect.
* To avoid expensive calls to expr_safe_replace we check with a pre-filter
* whether the substitution possibly could apply.
*/
void apply_subst(ptr_buffer<expr>& patterns) { void apply_subst(ptr_buffer<expr>& patterns) {
if (!m_subst) if (!m_subst)
return; return;
if (patterns.empty()) if (patterns.empty())
return; return;
if (m_subst->sub().empty())
return;
if (m_new_mark) {
m_marks.reset();
for (auto const& [k, v] : m_subst->sub())
m_marks.mark(k);
m_new_mark = false;
}
struct has_mark {
expr_mark& m_marks;
bool found = false;
has_mark(expr_mark& m) : m_marks(m) {}
void operator()(quantifier* q) {
found = true;
}
void operator()(expr* e) {
found |= m_marks.is_marked(e);
}
};
has_mark has_mark(m_marks);
for (expr* p : patterns)
quick_for_each_expr(has_mark, m_visited, p);
m_visited.reset();
if (!has_mark.found)
return;
if (m_new_subst) { if (m_new_subst) {
m_rep.reset(); m_rep.reset();
for (auto const& kv : m_subst->sub()) for (auto const& kv : m_subst->sub())
@ -822,6 +858,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
reset(); reset();
m_subst = s; m_subst = s;
m_new_subst = true; m_new_subst = true;
m_new_mark = true;
} }
void reset() { void reset() {