Home
last modified time | relevance | path

Searched refs:rw_cfg (Results 1 – 25 of 32) sorted by relevance

12

/dports/math/z3/z3-z3-4.8.13/src/tactic/core/
H A Ddistribute_forall_tactic.cpp24 struct rw_cfg : public default_rewriter_cfg { struct in distribute_forall_tactic
27 rw_cfg(ast_manager & _m):m(_m) {} in rw_cfg() argument
87 struct rw : public rewriter_tpl<rw_cfg> {
88 rw_cfg m_cfg;
91 rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg), in rw()
H A Delim_term_ite_tactic.cpp27 struct rw_cfg : public default_rewriter_cfg { struct in elim_term_ite_tactic
64 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() function
77 struct rw : public rewriter_tpl<rw_cfg> {
78 rw_cfg m_cfg;
81 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dblast_term_ite_tactic.cpp35 struct rw_cfg : public default_rewriter_cfg { struct in blast_term_ite_tactic
43 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() argument
108 struct rw : public rewriter_tpl<rw_cfg> {
109 rw_cfg m_cfg;
112 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Delim_uncnstr_tactic.cpp38 struct rw_cfg : public default_rewriter_cfg { struct in __anon2f1f399f0111::elim_uncnstr_tactic
52 rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, mc * _m, in rw_cfg() function
749 class rw : public rewriter_tpl<rw_cfg> {
750 rw_cfg m_cfg;
754 rewriter_tpl<rw_cfg>(m, produce_proofs, m_cfg), in rw()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/
H A Ddistribute_forall_tactic.cpp24 struct rw_cfg : public default_rewriter_cfg { struct in distribute_forall_tactic
27 rw_cfg(ast_manager & _m):m(_m) {} in rw_cfg() argument
87 struct rw : public rewriter_tpl<rw_cfg> {
88 rw_cfg m_cfg;
91 rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg), in rw()
H A Delim_term_ite_tactic.cpp27 struct rw_cfg : public default_rewriter_cfg { struct in elim_term_ite_tactic
64 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() function
77 struct rw : public rewriter_tpl<rw_cfg> {
78 rw_cfg m_cfg;
81 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dblast_term_ite_tactic.cpp35 struct rw_cfg : public default_rewriter_cfg { struct in blast_term_ite_tactic
43 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() function
108 struct rw : public rewriter_tpl<rw_cfg> {
109 rw_cfg m_cfg;
112 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/z3/z3-z3-4.8.13/src/ast/normal_forms/
H A Dpull_quant.cpp27 struct rw_cfg : public default_rewriter_cfg { struct
31 rw_cfg(ast_manager & m): in rw_cfg() function
302 struct rw : public rewriter_tpl<rw_cfg> {
303 rw_cfg m_cfg;
305 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
343 struct rw_cfg : public default_rewriter_cfg { struct
348 rw_cfg(ast_manager & m):m_pull(m), m_r(m), m_pr(m) {} in rw_cfg() function
360 struct rw : public rewriter_tpl<rw_cfg> {
361 rw_cfg m_cfg;
363 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/normal_forms/
H A Dpull_quant.cpp26 struct rw_cfg : public default_rewriter_cfg { struct
30 rw_cfg(ast_manager & m): in rw_cfg() argument
300 struct rw : public rewriter_tpl<rw_cfg> {
301 rw_cfg m_cfg;
303 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
341 struct rw_cfg : public default_rewriter_cfg { struct
346 rw_cfg(ast_manager & m):m_pull(m), m_r(m), m_pr(m) {} in rw_cfg() argument
358 struct rw : public rewriter_tpl<rw_cfg> {
359 rw_cfg m_cfg;
361 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/z3/z3-z3-4.8.13/src/tactic/bv/
H A Dmax_bv_sharing_tactic.cpp30 struct rw_cfg : public default_rewriter_cfg { struct in max_bv_sharing_tactic
44 rw_cfg(ast_manager & m, params_ref const & p): in rw_cfg() function
218 struct rw : public rewriter_tpl<rw_cfg> {
219 rw_cfg m_cfg;
222 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Delim_small_bv_tactic.cpp33 struct rw_cfg : public default_rewriter_cfg { struct in __anonc279b6710111::elim_small_bv_tactic
46 rw_cfg(ast_manager & _m, params_ref const & p) : in rw_cfg() function
217 struct rw : public rewriter_tpl<rw_cfg> {
218 rw_cfg m_cfg;
221 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dbv1_blaster_tactic.cpp35 struct rw_cfg : public default_rewriter_cfg { struct in bv1_blaster_tactic
56 rw_cfg(ast_manager & m, params_ref const & p): in rw_cfg() function
321 struct rw : public rewriter_tpl<rw_cfg> {
322 rw_cfg m_cfg;
325 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/
H A Dmax_bv_sharing_tactic.cpp30 struct rw_cfg : public default_rewriter_cfg { struct in max_bv_sharing_tactic
44 rw_cfg(ast_manager & m, params_ref const & p): in rw_cfg() function
218 struct rw : public rewriter_tpl<rw_cfg> {
219 rw_cfg m_cfg;
222 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Delim_small_bv_tactic.cpp33 struct rw_cfg : public default_rewriter_cfg { struct in __anond1b2c56c0111::elim_small_bv_tactic
46 rw_cfg(ast_manager & _m, params_ref const & p) : in rw_cfg() argument
217 struct rw : public rewriter_tpl<rw_cfg> {
218 rw_cfg m_cfg;
221 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dbv1_blaster_tactic.cpp35 struct rw_cfg : public default_rewriter_cfg { struct in bv1_blaster_tactic
56 rw_cfg(ast_manager & m, params_ref const & p): in rw_cfg() function
321 struct rw : public rewriter_tpl<rw_cfg> {
322 rw_cfg m_cfg;
325 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Ddegree_shift_tactic.cpp49 struct rw_cfg : public default_rewriter_cfg { struct
51 rw_cfg(imp & _o):o(_o) {} in rw_cfg() function
79 class rw : public rewriter_tpl<rw_cfg> {
80 rw_cfg m_cfg;
83 rewriter_tpl<rw_cfg>(o.m, o.m_produce_proofs, m_cfg), in rw()
H A Dfactor_tactic.cpp25 struct rw_cfg : public default_rewriter_cfg { struct in factor_tactic
34 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() argument
236 struct rw : public rewriter_tpl<rw_cfg> {
237 rw_cfg m_cfg;
240 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dpurify_arith_tactic.cpp191 struct rw_cfg : public default_rewriter_cfg { struct
205 rw_cfg(purify_arith_proc & o): in rw_cfg() function
229 rw_cfg& o; in init_cannot_purify()
230 proc(rw_cfg& o):o(o) {} in init_cannot_purify()
746 struct rw : public rewriter_tpl<rw_cfg> {
747 rw_cfg m_cfg;
749 rewriter_tpl<rw_cfg>(o.m(), o.m_produce_proofs, m_cfg), in rw()
754 struct rw_rec : public rewriter_tpl<rw_cfg> {
755 rw_cfg& m_cfg;
756 rw_rec(rw_cfg& cfg): in rw_rec()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Ddegree_shift_tactic.cpp49 struct rw_cfg : public default_rewriter_cfg { struct
51 rw_cfg(imp & _o):o(_o) {} in rw_cfg() function
79 class rw : public rewriter_tpl<rw_cfg> {
80 rw_cfg m_cfg;
83 rewriter_tpl<rw_cfg>(o.m, o.m_produce_proofs, m_cfg), in rw()
H A Dfactor_tactic.cpp25 struct rw_cfg : public default_rewriter_cfg { struct in factor_tactic
34 rw_cfg(ast_manager & _m, params_ref const & p): in rw_cfg() function
236 struct rw : public rewriter_tpl<rw_cfg> {
237 rw_cfg m_cfg;
240 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
H A Dpurify_arith_tactic.cpp191 struct rw_cfg : public default_rewriter_cfg { struct
205 rw_cfg(purify_arith_proc & o): in rw_cfg() argument
229 rw_cfg& o; in init_cannot_purify()
230 proc(rw_cfg& o):o(o) {} in init_cannot_purify()
746 struct rw : public rewriter_tpl<rw_cfg> {
747 rw_cfg m_cfg;
749 rewriter_tpl<rw_cfg>(o.m(), o.m_produce_proofs, m_cfg), in rw()
754 struct rw_rec : public rewriter_tpl<rw_cfg> {
755 rw_cfg& m_cfg;
756 rw_rec(rw_cfg& cfg): in rw_rec()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/
H A Denum2bv_rewriter.cpp41 struct rw_cfg : public default_rewriter_cfg { struct
47 rw_cfg(imp& i, ast_manager & m) : in rw_cfg() function
220 struct rw : public rewriter_tpl<rw_cfg> {
221 rw_cfg m_cfg;
224 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/
H A Denum2bv_rewriter.cpp41 struct rw_cfg : public default_rewriter_cfg { struct
49 rw_cfg(imp& i, ast_manager & m) : in rw_cfg() function
253 struct rw : public rewriter_tpl<rw_cfg> {
254 rw_cfg m_cfg;
257 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg), in rw()
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/
H A Dspacer_arith_generalizers.cpp73 limit_denominator_rewriter_cfg rw_cfg(m, limit); in limit_denominators() local
74 rewriter_tpl<limit_denominator_rewriter_cfg> rw(m, false, rw_cfg); in limit_denominators()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/
H A Dspacer_arith_generalizers.cpp73 limit_denominator_rewriter_cfg rw_cfg(m, limit); in limit_denominators() local
74 rewriter_tpl<limit_denominator_rewriter_cfg> rw(m, false, rw_cfg); in limit_denominators()

12