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

reorder fields

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-15 12:29:13 -07:00
parent bebf2d6a52
commit fe4c48e14c
1 changed files with 14 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -52,21 +52,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
arith_util m_a_util; arith_util m_a_util;
bv_util m_bv_util; bv_util m_bv_util;
expr_safe_replace m_rep; expr_safe_replace m_rep;
bool m_new_subst { false };
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
unsigned long long m_max_memory; // in bytes // substitution support
unsigned m_max_steps;
bool m_pull_cheap_ite;
bool m_flat;
bool m_cache_all;
bool m_push_ite_arith;
bool m_push_ite_bv;
bool m_ignore_patterns_on_ground_qbody;
bool m_rewrite_patterns;
// substitution support
expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
expr_substitution * m_subst; expr_substitution * m_subst = nullptr;
unsigned long long m_max_memory; // in bytes
bool m_new_subst = false;
unsigned m_max_steps = UINT_MAX;
bool m_pull_cheap_ite = true;
bool m_flat = true;
bool m_cache_all = false;
bool m_push_ite_arith = true;
bool m_push_ite_bv = true;
bool m_ignore_patterns_on_ground_qbody = true;
bool m_rewrite_patterns = true;
ast_manager & m() const { return m_b_rw.m(); } ast_manager & m() const { return m_b_rw.m(); }
@ -805,8 +805,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_bv_util(m), m_bv_util(m),
m_rep(m), m_rep(m),
m_pinned(m), m_pinned(m),
m_used_dependencies(m), m_used_dependencies(m) {
m_subst(nullptr) {
updt_local_params(p); updt_local_params(p);
} }