/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 597 mk_ite(inf_xor, nan, x, v2); in mk_add() 603 mk_ite(v3_and, nan, y, v3); in mk_add() 614 mk_ite(v4_and, x, v4, v4); in mk_add() 676 mk_ite(c6, v6, v7, result); in mk_add() 858 mk_ite(c6, v6, v7, result); in mk_mul() 1012 mk_ite(c7, v7, v8, result); in mk_div() 1240 mk_ite(c6, v6, v7, result); in mk_rem() 1779 mk_ite(c7, v7, v8, result); in mk_fma() 1933 mk_ite(c4, v4, v5, result); in mk_sqrt() 2189 mk_ite(c5, v5, v6, result); in mk_round_to_integral() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 596 mk_ite(inf_xor, nan, x, v2); 602 mk_ite(v3_and, nan, y, v3); 613 mk_ite(v4_and, x, v4, v4); 675 mk_ite(c6, v6, v7, result); 857 mk_ite(c6, v6, v7, result); 1011 mk_ite(c7, v7, v8, result); 1239 mk_ite(c6, v6, v7, result); 1768 mk_ite(c7, v7, v8, result); 1922 mk_ite(c4, v4, v5, result); 2178 mk_ite(c5, v5, v6, result); [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
H A D | bdd.cpp | 27 SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1)); in test2() 28 SASSERT(m.mk_ite(v0,v1,v1) == v1); in test2() 29 SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1)); in test2() 30 SASSERT(m.mk_ite(v1,v0,v0) == v0); in test2() 31 SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); in test2() 32 SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); in test2()
|
H A D | model_evaluator.cpp | 40 hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p))); in tst_model_evaluator() 50 …fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk… in tst_model_evaluator() 51 …gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2… in tst_model_evaluator()
|
/dports/math/z3/z3-z3-4.8.13/src/test/ |
H A D | bdd.cpp | 27 SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1)); in test2() 28 SASSERT(m.mk_ite(v0,v1,v1) == v1); in test2() 29 SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1)); in test2() 30 SASSERT(m.mk_ite(v1,v0,v0) == v0); in test2() 31 SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); in test2() 32 SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); in test2()
|
H A D | model_evaluator.cpp | 40 hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p))); in tst_model_evaluator() 50 …fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk… in tst_model_evaluator() 51 …gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2… in tst_model_evaluator()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
H A D | bool_rewriter.cpp | 452 result = m().mk_ite(c, t, e); in mk_nested_ite() 649 result = m().mk_ite(cond, result, mk_eq(e, val)); in try_ite_value() 654 result = m().mk_ite(cond, mk_eq(t, val), result); in try_ite_value() 831 result = m().mk_ite(m().mk_or(c, to_app(e)->get_arg(0)), t, to_app(e)->get_arg(2)); in mk_ite_core() 933 result = m().mk_ite(new_c, to_app(t)->get_arg(2), e); in mk_ite_core() 940 result = m().mk_ite(new_c, to_app(t)->get_arg(1), e); in mk_ite_core() 957 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); in mk_ite_core() 974 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); in mk_ite_core() 985 result = m().mk_ite(new_c, t, to_app(e)->get_arg(2)); in mk_ite_core() 994 result = m().mk_ite(new_c, t, to_app(e)->get_arg(1)); in mk_ite_core() [all …]
|
H A D | bool_rewriter.h | 205 void mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { in mk_ite() function 207 result = m().mk_ite(c, t, e); in mk_ite() 209 expr_ref mk_ite(expr * c, expr * t, expr * e) { in mk_ite() function 211 mk_ite(c, t, e, r); in mk_ite()
|
H A D | th_rewriter.cpp | 160 … result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); in apply_tamagotchi() 164 … result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); in apply_tamagotchi() 269 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 276 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 282 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 326 result = m().mk_ite(to_app(args[0])->get_arg(0), in pull_ite() 572 result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e)); in push_ite() 574 result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common); in push_ite()
|
H A D | seq_rewriter.cpp | 977 result = m().mk_ite(c, arg1, arg2); in lift_ites_throttled() 2393 result = m().mk_ite( in mk_str_sbv2s() 2508 result = m().mk_ite(str().mk_is_empty(head), in mk_str_stoi() 2515 result = m().mk_ite(str().mk_is_empty(result), in mk_str_stoi() 2694 return expr_ref(m().mk_ite(cond, r, re_empty), m()); in re_and() 3530 auto mk_ite = [&](expr* c, expr* a, expr* b) { in mk_der_op_rec() local 3531 return (a == b) ? a : m().mk_ite(c, a, b); in mk_der_op_rec() 3592 result = mk_ite(ca, r1, r2); in mk_der_op_rec() 3621 result = mk_ite(ca, r1, r2); in mk_der_op_rec() 3627 result = mk_ite(cb, r1, r2); in mk_der_op_rec() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
H A D | bool_rewriter.cpp | 452 result = m().mk_ite(c, t, e); in mk_nested_ite() 649 result = m().mk_ite(cond, result, mk_eq(e, val)); in try_ite_value() 654 result = m().mk_ite(cond, mk_eq(t, val), result); in try_ite_value() 822 result = m().mk_ite(m().mk_or(c, to_app(e)->get_arg(0)), t, to_app(e)->get_arg(2)); in mk_ite_core() 906 result = m().mk_ite(new_c, to_app(t)->get_arg(2), e); in mk_ite_core() 913 result = m().mk_ite(new_c, to_app(t)->get_arg(1), e); in mk_ite_core() 929 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); in mk_ite_core() 946 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); in mk_ite_core() 957 result = m().mk_ite(new_c, t, to_app(e)->get_arg(2)); in mk_ite_core() 966 result = m().mk_ite(new_c, t, to_app(e)->get_arg(1)); in mk_ite_core() [all …]
|
H A D | bool_rewriter.h | 190 void mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { in mk_ite() function 192 result = m().mk_ite(c, t, e); in mk_ite() 194 expr_ref mk_ite(expr * c, expr * t, expr * e) { in mk_ite() function 196 mk_ite(c, t, e, r); in mk_ite()
|
H A D | th_rewriter.cpp | 158 … result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); in apply_tamagotchi() 162 … result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); in apply_tamagotchi() 250 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 257 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 263 result = m().mk_ite(ite->get_arg(0), in pull_ite_core() 307 result = m().mk_ite(to_app(args[0])->get_arg(0), in pull_ite() 553 result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e)); in push_ite() 555 result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common); in push_ite()
|
H A D | seq_rewriter.cpp | 879 result = m().mk_ite(c, arg1, arg2); in lift_ites_throttled() 1523 m().mk_ite(m().mk_eq(c, zero()), in mk_seq_index() 1533 result = m().mk_ite(str().mk_prefix(b, a), zero(), in mk_seq_index() 2081 result = m().mk_ite(str().mk_is_empty(head), in mk_str_stoi() 2254 return expr_ref(m().mk_ite(cond, r, re_empty), m()); in re_and() 2706 auto mk_ite = [&](expr* c, expr* a, expr* b) { in mk_der_op_rec() local 2707 return (a == b) ? a : m().mk_ite(c, a, b); in mk_der_op_rec() 2768 result = mk_ite(ca, r1, r2); in mk_der_op_rec() 2796 result = mk_ite(ca, r1, r2); in mk_der_op_rec() 2802 result = mk_ite(cb, r1, r2); in mk_der_op_rec() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/bit_blaster/ |
H A D | bit_blaster.h | 51 void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); } in mk_ite() function
|
H A D | bit_blaster_tpl_def.h | 488 mk_ite(q, t.get(j-1), p.get(j-1), ie); in mk_udiv_urem() 497 mk_ite(q, t.get(j), p.get(j), ie); in mk_udiv_urem() 535 mk_ite(c, t_bits[i], e_bits[i], t); in mk_multiplexer() 954 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_shl() 968 mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); in mk_shl() 998 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_lshr() 1011 mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); in mk_lshr() 1041 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_ashr() 1054 mk_ite(is_large, a_bits[sz-1], out_bits[j].get(), new_out); in mk_ashr() 1090 mk_ite(eqs.get(j), a_bits[src], out, new_out); in mk_ext_rotate_left_right() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/bit_blaster/ |
H A D | bit_blaster.h | 51 void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); } in mk_ite() function
|
H A D | bit_blaster_tpl_def.h | 408 mk_ite(q, t.get(j-1), p.get(j-1), ie); in mk_udiv_urem() 417 mk_ite(q, t.get(j), p.get(j), ie); in mk_udiv_urem() 455 mk_ite(c, t_bits[i], e_bits[i], t); in mk_multiplexer() 874 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_shl() 888 mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); in mk_shl() 918 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_lshr() 931 mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); in mk_lshr() 961 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); in mk_ashr() 974 mk_ite(is_large, a_bits[sz-1], out_bits[j].get(), new_out); in mk_ashr() 1010 mk_ite(eqs.get(j), a_bits[src], out, new_out); in mk_ext_rotate_left_right() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/model/ |
H A D | model2expr.cpp | 126 tmp = m.mk_ite(cond, m.mk_eq(func, fi->get_entry(j)->get_result()), tmp); in model2expr() 135 tmp = m.mk_ite(cond, fi->get_entry(j)->get_result(), tmp); in model2expr()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
H A D | model2expr.cpp | 126 tmp = m.mk_ite(cond, m.mk_eq(func, fi->get_entry(j)->get_result()), tmp); in model2expr() 135 tmp = m.mk_ite(cond, fi->get_entry(j)->get_result(), tmp); in model2expr()
|
/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | preprocessor.c | 175 return mk_ite(tm, children[0], children[1], children[2], type); in mk_composite() 616 term_t b1 = mk_ite(tm, msb_t, t1, t2, tau); in preprocessor_apply() 617 term_t b2 = mk_ite(tm, msb_t, t3, t4, tau); in preprocessor_apply() 619 current_pre = mk_ite(tm, msb_s, b1, b2, tau); in preprocessor_apply() 665 term_t b1 = mk_ite(tm, msb_t, t1, t2, tau); in preprocessor_apply() 666 term_t b2 = mk_ite(tm, msb_t, t3, t4, tau); in preprocessor_apply() 668 current_pre = mk_ite(tm, msb_s, b1, b2, tau); in preprocessor_apply()
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
H A D | reduce_invertible_tactic.cpp | 396 new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v); in is_invertible() 426 (*mc)->add(v, m.mk_ite(new_v, other, mk_diagonal(other))); in is_invertible() 451 (*mc)->add(v, m.mk_ite(delta, e2, succ_e2)); in is_invertible() 467 (*mc)->add(v, m.mk_ite(delta, e1, pred_e1)); in is_invertible()
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/aig/ |
H A D | aig.h | 68 aig_ref mk_ite(aig_ref const & r1, aig_ref const & r2, aig_ref const & r3);
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/aig/ |
H A D | aig.h | 68 aig_ref mk_ite(aig_ref const & r1, aig_ref const & r2, aig_ref const & r3);
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
H A D | bv2int_rewriter.cpp | 126 case OP_ITE: SASSERT(num_args == 3); return mk_ite(args[0], args[1], args[2], result); in mk_app_core() 188 br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) { in mk_ite() function in bv2int_rewriter 192 result = m_bv.mk_bv2int(m().mk_ite(c, s1, t1)); in mk_ite() 198 result = mk_sbv2int(m().mk_ite(c, s1, t1)); in mk_ite() 617 return m().mk_ite(c, t, e); in mk_sbv2int()
|