Searched refs:s_bv (Results 1 – 6 of 6) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | nla2bv_tactic.cpp | 212 expr_ref s_bv(m_manager); in add_int_var() local
239 m_fmc->hide(s_bv); in add_int_var()
240 s_bv = m_bv.mk_bv2int(s_bv); in add_int_var()
248 s_bv = m_arith.mk_add(s_bv, m_arith.mk_numeral(*low, true)); in add_int_var()
256 s_bv = m_arith.mk_sub(m_arith.mk_numeral(*up, true), s_bv); in add_int_var()
259 … s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(rational::power_of_two(num_bits-1), true)); in add_int_var()
262 m_trail.push_back(s_bv); in add_int_var()
263 m_subst.insert(n, s_bv); in add_int_var()
265 m_defs.push_back(s_bv); in add_int_var()
280 m_trail.push_back(s_bv); in add_real_var()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
| H A D | nla2bv_tactic.cpp | 212 expr_ref s_bv(m_manager); in add_int_var() local
239 m_fmc->hide(s_bv); in add_int_var()
240 s_bv = m_bv.mk_bv2int(s_bv); in add_int_var()
248 s_bv = m_arith.mk_add(s_bv, m_arith.mk_numeral(*low, true)); in add_int_var()
256 s_bv = m_arith.mk_sub(m_arith.mk_numeral(*up, true), s_bv); in add_int_var()
259 … s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(rational::power_of_two(num_bits-1), true)); in add_int_var()
262 m_trail.push_back(s_bv); in add_int_var()
263 m_subst.insert(n, s_bv); in add_int_var()
265 m_defs.push_back(s_bv); in add_int_var()
280 m_trail.push_back(s_bv); in add_real_var()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/bv/ |
| H A D | bvarray2uf_rewriter.cpp | 43 symbol s_bv("bv"); in bvarray2uf_rewriter_cfg() local
44 if (!m_manager.has_plugin(s_bv)) in bvarray2uf_rewriter_cfg()
45 m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); in bvarray2uf_rewriter_cfg()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/ |
| H A D | bvarray2uf_rewriter.cpp | 43 symbol s_bv("bv"); in bvarray2uf_rewriter_cfg() local
44 if (!m_manager.has_plugin(s_bv)) in bvarray2uf_rewriter_cfg()
45 m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); in bvarray2uf_rewriter_cfg()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/fpa/ |
| H A D | fpa2bv_rewriter.cpp | 34 symbol s_bv("bv"); in fpa2bv_rewriter_cfg() local
35 if (!m_manager.has_plugin(s_bv)) in fpa2bv_rewriter_cfg()
36 m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); in fpa2bv_rewriter_cfg()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
| H A D | fpa2bv_rewriter.cpp | 34 symbol s_bv("bv"); in fpa2bv_rewriter_cfg() local
35 if (!m_manager.has_plugin(s_bv)) in fpa2bv_rewriter_cfg()
36 m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); in fpa2bv_rewriter_cfg()
|