Home
last modified time | relevance | path

Searched refs:is_bv (Results 1 – 25 of 96) sorted by relevance

1234

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_arith_value.cpp84 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 Dtheory_bv.h149 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 Dsmt_arith_value.cpp84 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 Dtheory_bv.h150 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 Dbv_invariant.cpp39 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 Dbv_delay_internalize.cpp28 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 Dbv_invariant.cpp39 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 Dbv_delay_internalize.cpp28 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 Dbv_solver.cpp75 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 Dprobe.cpp284 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 Dprobe.cpp284 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 Dz3++.h784 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 Dfpa_decl_plugin.h274 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 Dfpa_decl_plugin.h269 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 Dz3++.h698 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 Dapi_fpa.cpp37 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 Dapi_fpa.cpp37 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 Dopt_context.cpp116 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 Dmacro_util.cpp41 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 Dmacro_util.cpp41 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 Dz3++.h777 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 Dbv2int_rewriter.cpp325 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 Dbv2int_rewriter.cpp325 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 Dbv_bounds.h96 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 Dbv_bounds.h96 return is_app(e) && m_bv_util.is_bv(e) in to_bound()

1234