| /dports/math/z3/z3-z3-4.8.13/src/tactic/bv/ |
| H A D | bv_size_reduction_tactic.cpp | 42 generic_model_converter_ref m_fmc; member in __anon29f03ab90111::bv_size_reduction_tactic
65 m_fmc = nullptr; in cleanup()
267 if (!m_fmc && new_const) in run()
268 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); in run()
270 m_fmc->hide(new_const); in run()
333 if (!m_fmc && new_const) in run()
334 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); in run()
336 m_fmc->hide(new_const); in run()
361 if (m_fmc) { in run()
362 mc = concat(m_fmc.get(), mc.get()); in run()
[all …]
|
| H A D | bvarray2uf_rewriter.h | 31 generic_model_converter * m_fmc; variable
59 void set_mcs(generic_model_converter * fmc) { m_fmc = fmc; } in set_mcs()
|
| H A D | bvarray2uf_rewriter.cpp | 39 m_fmc(nullptr), in bvarray2uf_rewriter_cfg()
115 if (m_fmc) { in mk_uf_for_array()
116 m_fmc->hide(bv_f); in mk_uf_for_array()
118 m_fmc->add(e, m_array_util.mk_as_array(bv_f)); in mk_uf_for_array()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/ |
| H A D | bv_size_reduction_tactic.cpp | 42 generic_model_converter_ref m_fmc; member in __anon3cbe4f340111::bv_size_reduction_tactic
65 m_fmc = nullptr; in cleanup()
267 if (!m_fmc && new_const) in run()
268 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); in run()
270 m_fmc->hide(new_const); in run()
333 if (!m_fmc && new_const) in run()
334 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); in run()
336 m_fmc->hide(new_const); in run()
361 if (m_fmc) { in run()
362 mc = concat(m_fmc.get(), mc.get()); in run()
[all …]
|
| H A D | bvarray2uf_rewriter.h | 31 generic_model_converter * m_fmc; variable
59 void set_mcs(generic_model_converter * fmc) { m_fmc = fmc; } in set_mcs()
|
| H A D | bvarray2uf_rewriter.cpp | 39 m_fmc(nullptr), in bvarray2uf_rewriter_cfg()
115 if (m_fmc) { in mk_uf_for_array()
116 m_fmc->hide(bv_f); in mk_uf_for_array()
118 m_fmc->add(e, m_array_util.mk_as_array(bv_f)); in mk_uf_for_array()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | nla2bv_tactic.cpp | 63 generic_model_converter_ref m_fmc; member in nla2bv_tactic::imp
78 m_fmc(nullptr) { in imp()
91 m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); in operator ()()
107 mc = m_fmc.get(); in operator ()()
109 m_fmc->add(m_vars[i].get(), m_defs[i].get()); in operator ()()
112 m_fmc->hide(m_bv2real.get_aux_decl(i)); in operator ()()
239 m_fmc->hide(s_bv); in add_int_var()
277 m_fmc->hide(s); in add_real_var()
278 m_fmc->hide(t); in add_real_var()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
| H A D | nla2bv_tactic.cpp | 63 generic_model_converter_ref m_fmc; member in nla2bv_tactic::imp
78 m_fmc(nullptr) { in imp()
91 m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); in operator ()()
107 mc = m_fmc.get(); in operator ()()
109 m_fmc->add(m_vars[i].get(), m_defs[i].get()); in operator ()()
112 m_fmc->hide(m_bv2real.get_aux_decl(i)); in operator ()()
239 m_fmc->hide(s_bv); in add_int_var()
277 m_fmc->hide(s); in add_real_var()
278 m_fmc->hide(t); in add_real_var()
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | qsat.h | 74 generic_model_converter_ref m_fmc; variable
|
| H A D | qsat.cpp | 49 m_fmc(alloc(generic_model_converter, m, "qsat")) in pred_abs()
54 return m_fmc.get(); in fmc()
297 m_fmc->hide(r); in fresh_bool()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | qsat.h | 74 generic_model_converter_ref m_fmc; variable
|
| H A D | qsat.cpp | 49 m_fmc(alloc(generic_model_converter, m, "qsat")) in pred_abs()
54 return m_fmc.get(); in fmc()
297 m_fmc->hide(r); in fresh_bool()
|