Home
last modified time | relevance | path

Searched refs:mk_ite (Results 1 – 25 of 163) sorted by relevance

1234567

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp597 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 Dfpa2bv_converter.cpp596 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 Dbdd.cpp27 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 Dmodel_evaluator.cpp40 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 Dbdd.cpp27 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 Dmodel_evaluator.cpp40 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 Dbool_rewriter.cpp452 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 Dbool_rewriter.h205 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 Dth_rewriter.cpp160 … 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 Dseq_rewriter.cpp977 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 Dbool_rewriter.cpp452 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 Dbool_rewriter.h190 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 Dth_rewriter.cpp158 … 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 Dseq_rewriter.cpp879 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 Dbit_blaster.h51 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 Dbit_blaster_tpl_def.h488 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 Dbit_blaster.h51 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 Dbit_blaster_tpl_def.h408 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 Dmodel2expr.cpp126 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 Dmodel2expr.cpp126 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 Dpreprocessor.c175 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 Dreduce_invertible_tactic.cpp396 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 Daig.h68 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 Daig.h68 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 Dbv2int_rewriter.cpp126 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()

1234567