mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

#5532 add blocking condition for recursion.

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-07 12:28:18 +02:00
parent 93415740b6
commit 8c406c161e
2 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/rewriter.h
View file

@ -21,6 +21,7 @@ Notes:
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/rewriter_types.h"
#include "ast/act_cache.h" #include "ast/act_cache.h"
#include "util/obj_hashtable.h"
/** /**
\brief Common infrastructure for AST rewriters. \brief Common infrastructure for AST rewriters.
@ -60,6 +61,7 @@ protected:
proof_ref_vector m_result_pr_stack; proof_ref_vector m_result_pr_stack;
// -------------------------- // --------------------------
obj_hashtable<expr> m_blocked;
expr * m_root; expr * m_root;
unsigned m_num_qvars; unsigned m_num_qvars;
struct scope { struct scope {
@ -112,6 +114,8 @@ protected:
void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); } void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); }
void elim_reflex_prs(unsigned spos); void elim_reflex_prs(unsigned spos);
void block(expr* t) { m_blocked.insert(t); }
bool is_blocked(expr* t) const { return m_blocked.contains(t); }
public: public:
rewriter_core(ast_manager & m, bool proof_gen); rewriter_core(ast_manager & m, bool proof_gen);
virtual ~rewriter_core(); virtual ~rewriter_core();

17
src/ast/rewriter/rewriter_def.h
View file

@ -195,14 +195,15 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
if (process_const<ProofGen>(to_app(t))) if (process_const<ProofGen>(to_app(t)))
return true; return true;
TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";); TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";);
#if 1 if (!is_blocked(t)) {
#else rewriter_tpl rw(m(), false, m_cfg);
// disabled pending fix for loop/stack overflow in case of recursive expansion (possible) for (auto* s : m_blocked)
rewriter_tpl rw(m(), false, m_cfg); rw.block(s);
expr_ref result(m()); rw.block(t);
rw(m_r, result, m_pr); expr_ref result(m());
m_r = result; rw(m_r, result, m_pr);
#endif m_r = result;
}
set_new_child_flag(t, m_r); set_new_child_flag(t, m_r);
result_stack().push_back(m_r); result_stack().push_back(m_r);
return true; return true;