/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_arith_value.cpp | 84 if (b.is_bv(e) && m_thb) return m_thb->get_upper(n, up); in get_up() 96 if (b.is_bv(e) && m_thb) return m_thb->get_lower(n, up); in get_lo() 108 if (m_thb && b.is_bv(e)) return m_thb->get_value(n, _val); in get_value() 136 if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) { in get_lo() 145 if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) { in get_up()
|
H A D | theory_bv.h | 149 bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); } in is_bv() function 150 bool is_bv(enode const* n) const { return is_bv(n->get_expr()); } in is_bv() function 151 bool is_bv(theory_var v) const { return is_bv(get_enode(v)); } in is_bv() function
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_arith_value.cpp | 84 if (b.is_bv(e) && m_thb) return m_thb->get_upper(n, up); in get_up() 96 if (b.is_bv(e) && m_thb) return m_thb->get_lower(n, up); in get_lo() 108 if (m_thb && b.is_bv(e)) return m_thb->get_value(n, _val); in get_value() 136 if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) { in get_lo() 145 if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) { in get_up()
|
H A D | theory_bv.h | 150 bool is_bv(app const* n) const { return m_util.is_bv_sort(get_manager().get_sort(n)); } in is_bv() function 151 bool is_bv(enode const* n) const { return is_bv(n->get_owner()); } in is_bv() function 152 bool is_bv(theory_var v) const { return is_bv(get_enode(v)); } in is_bv() function
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
H A D | bv_invariant.cpp | 39 if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) { in check_missing_propagation() 65 if (!is_root(v) || !is_bv(v)) in check_zero_one_bits()
|
H A D | bv_delay_internalize.cpp | 28 SASSERT(bv.is_bv(e)); in check_delay_internalized() 316 SASSERT(bv.is_bv(a)); in check_bv_eval() 355 if (!bv.is_bv(e)) in get_internalize_mode()
|
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
H A D | bv_invariant.cpp | 39 if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) { in check_missing_propagation() 65 if (!is_root(v) || !is_bv(v)) in check_zero_one_bits()
|
H A D | bv_delay_internalize.cpp | 28 SASSERT(bv.is_bv(e)); in check_delay_internalized() 318 SASSERT(bv.is_bv(a)); in check_bv_eval() 357 if (!bv.is_bv(e)) in get_internalize_mode()
|
H A D | bv_solver.cpp | 75 is_bv(v2) && in fixed_var_eh() 178 if (is_bv(v)) { in display() 199 if (is_bv(eq.v1())) { in new_eq_eh() 207 if (!is_bv(v1)) in new_diseq_eh() 715 SASSERT(bv.is_bv(n->get_expr())); in add_value()
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/ |
H A D | probe.cpp | 284 if (!m.is_bool(n) && !u.is_bv(n)) in operator ()() 340 if (!m.is_bool(n) && !m_bv_util.is_bv(n) && !m_array_util.is_array(n)) in operator ()() 378 if (!m.is_bool(n) && !m_bv_util.is_bv(n)) in operator ()()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/ |
H A D | probe.cpp | 284 if (!m.is_bool(n) && !u.is_bv(n)) in operator ()() 340 if (!m.is_bool(n) && !m_bv_util.is_bv(n) && !m_array_util.is_array(n)) in operator ()() 378 if (!m.is_bool(n) && !m_bv_util.is_bv(n)) in operator ()()
|
/dports/math/z3/z3-z3-4.8.13/src/api/c++/ |
H A D | z3++.h | 784 bool is_bv() const { return get_sort().is_bv(); } in is_bv() function 1567 if (a.is_bv()) { in mod() 1661 else if (a.is_bv() && b.is_bv()) { 1691 else if (a.is_bv() && b.is_bv()) { 1714 else if (a.is_bv() && b.is_bv()) { 1734 else if (a.is_bv() && b.is_bv()) { 1776 else if (a.is_bv() && b.is_bv()) { 1798 else if (a.is_bv() && b.is_bv()) { 1823 else if (a.is_bv() && b.is_bv()) { 1845 else if (a.is_bv() && b.is_bv()) { [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/ast/ |
H A D | fpa_decl_plugin.h | 274 SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); in mk_fp() 275 SASSERT(m_bv_util.is_bv(exp)); in mk_fp() 276 SASSERT(m_bv_util.is_bv(sig)); in mk_fp() 348 SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); in mk_bv2rm()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
H A D | fpa_decl_plugin.h | 269 SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); 270 SASSERT(m_bv_util.is_bv(exp)); 271 SASSERT(m_bv_util.is_bv(sig)); 343 SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
|
/dports/math/vampire/vampire-4.5.1/z3/api/ |
H A D | z3++.h | 698 bool is_bv() const { return get_sort().is_bv(); } in is_bv() function 1341 else if (a.is_bv() && b.is_bv()) { 1371 else if (a.is_bv() && b.is_bv()) { 1394 else if (a.is_bv() && b.is_bv()) { 1411 else if (a.is_bv() && b.is_bv()) { 1432 else if (a.is_bv()) { 1453 else if (a.is_bv() && b.is_bv()) { 1475 else if (a.is_bv() && b.is_bv()) { 1500 else if (a.is_bv() && b.is_bv()) { 1522 else if (a.is_bv() && b.is_bv()) { [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/api/ |
H A D | api_fpa.cpp | 37 static bool is_bv(Z3_context c, Z3_ast a) { in is_bv() function 38 return mk_c(c)->bvutil().is_bv(to_expr(a)); in is_bv() 265 if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { in Z3_mk_fpa_fp() 738 if (!is_bv(c, bv) || !is_fp_sort(c, s)) { in Z3_mk_fpa_to_fp_bv() 744 if (!ctx->bvutil().is_bv(to_expr(bv)) || in Z3_mk_fpa_to_fp_bv() 798 !ctx->bvutil().is_bv(to_expr(t)) || in Z3_mk_fpa_to_fp_signed() 816 !ctx->bvutil().is_bv(to_expr(t)) || in Z3_mk_fpa_to_fp_unsigned()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
H A D | api_fpa.cpp | 37 static bool is_bv(Z3_context c, Z3_ast a) { in is_bv() function 38 return mk_c(c)->bvutil().is_bv(to_expr(a)); in is_bv() 265 if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { in Z3_mk_fpa_fp() 738 if (!is_bv(c, bv) || !is_fp_sort(c, s)) { in Z3_mk_fpa_to_fp_bv() 744 if (!ctx->bvutil().is_bv(to_expr(bv)) || in Z3_mk_fpa_to_fp_bv() 798 !ctx->bvutil().is_bv(to_expr(t)) || in Z3_mk_fpa_to_fp_signed() 816 !ctx->bvutil().is_bv(to_expr(t)) || in Z3_mk_fpa_to_fp_unsigned()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/opt/ |
H A D | opt_context.cpp | 116 if (!m_bv.is_bv(t) && !m_arith.is_int_real(t)) { in add() 224 else if (m_bv.is_bv(result)) { in get_objective() 594 if (m_bv.is_bv(t)) { in mk_ge() 706 struct context::is_bv { struct in opt::context 711 is_bv(ast_manager& m): m(m), pb(m), bv(m) {} in is_bv() function 719 (!is_uninterp_const(n) || (!m.is_bool(n) && !bv.is_bv(n)))) { in operator ()() 727 is_bv proc(m); in probe_bv() 744 catch (const is_bv::found &) { in probe_bv() 987 if ((is_max || is_min) && m_bv.is_bv(term)) { in is_maxsat()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/macros/ |
H A D | macro_util.cpp | 41 bool macro_util::is_bv(expr * n) const { in is_bv() function in macro_util 42 return m_bv.is_bv(n); in is_bv() 70 if (m_bv_rw.is_bv(n)) { in is_zero_safe() 88 if (is_bv(t1)) { in mk_sub() 97 if (is_bv(t1)) { in mk_add()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/macros/ |
H A D | macro_util.cpp | 41 bool macro_util::is_bv(expr * n) const { in is_bv() function in macro_util 42 return m_bv.is_bv(n); in is_bv() 70 if (m_bv_rw.is_bv(n)) { in is_zero_safe() 88 if (is_bv(t1)) { in mk_sub() 97 if (is_bv(t1)) { in mk_add()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/c++/ |
H A D | z3++.h | 777 bool is_bv() const { return get_sort().is_bv(); } in is_bv() function 1400 if (a.is_bv()) { in mod() 1494 else if (a.is_bv() && b.is_bv()) { 1524 else if (a.is_bv() && b.is_bv()) { 1547 else if (a.is_bv() && b.is_bv()) { 1567 else if (a.is_bv() && b.is_bv()) { 1588 else if (a.is_bv()) { 1609 else if (a.is_bv() && b.is_bv()) { 1631 else if (a.is_bv() && b.is_bv()) { 1656 else if (a.is_bv() && b.is_bv()) { [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
H A D | bv2int_rewriter.cpp | 325 SASSERT(m_bv.is_bv(s)); in mk_bv_add() 326 SASSERT(m_bv.is_bv(t)); in mk_bv_add() 376 SASSERT(m_bv.is_bv(s)); in mk_bv_mul() 377 SASSERT(m_bv.is_bv(t)); in mk_bv_mul()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
H A D | bv2int_rewriter.cpp | 325 SASSERT(m_bv.is_bv(s)); in mk_bv_add() 326 SASSERT(m_bv.is_bv(t)); in mk_bv_add() 376 SASSERT(m_bv.is_bv(s)); in mk_bv_mul() 377 SASSERT(m_bv.is_bv(t)); in mk_bv_mul()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
H A D | bv_bounds.h | 96 return is_app(e) && m_bv_util.is_bv(e) in to_bound()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
H A D | bv_bounds.h | 96 return is_app(e) && m_bv_util.is_bv(e) in to_bound()
|