| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | bv_internalize.cpp | 107 sat::literal lit = expr2literal(e); in internalize()
490 add_def(def, expr2literal(n)); in internalize_le()
495 literal r = expr2literal(n); in internalize_carry()
496 literal l1 = expr2literal(n->get_arg(0)); in internalize_carry()
497 literal l2 = expr2literal(n->get_arg(1)); in internalize_carry()
498 literal l3 = expr2literal(n->get_arg(2)); in internalize_carry()
509 literal r = expr2literal(n); in internalize_xor3()
510 literal l1 = expr2literal(n->get_arg(0)); in internalize_xor3()
511 literal l2 = expr2literal(n->get_arg(1)); in internalize_xor3()
596 add_def(def, expr2literal(n)); in internalize_novfl()
[all …]
|
| H A D | bv_delay_internalize.cpp | 290 sat::literal no_overflow = expr2literal(n); in check_umul_no_overflow()
304 lits.push_back(expr2literal(n)); in check_umul_no_overflow()
333 sat::literal lit = expr2literal(n->get_expr()); in check_bool_eval()
|
| 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()
|
| H A D | euf_relevancy.cpp | 130 sat::literal lit = expr2literal(c); in init_relevancy()
|
| H A D | sat_th.cpp | 76 sat::literal th_euf_solver::expr2literal(expr* e) const { in expr2literal() function in euf::th_euf_solver
77 return ctx.expr2literal(e); in expr2literal()
|
| H A D | euf_internalize.cpp | 335 sat::literal lit1 = expr2literal(e); in axiomatize_basic()
340 sat::literal lit2 = expr2literal(e2); in axiomatize_basic()
|
| H A D | array_internalize.cpp | 29 auto lit = expr2literal(e); in internalize()
|
| H A D | sat_th.h | 131 sat::literal expr2literal(expr* e) const;
|
| H A D | recfun_solver.cpp | 242 auto lit = expr2literal(e); in internalize()
|
| H A D | bv_solver.cpp | 186 else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) { in display()
248 sat::literal antecedent = ~expr2literal(ne.eq()); in new_diseq_eh()
|
| H A D | fpa_solver.cpp | 104 sat::literal lit = expr2literal(e); in internalize()
|
| H A D | arith_axioms.cpp | 66 literal is_int = ctx.expr2literal(n); in mk_is_int_axiom()
|
| H A D | euf_solver.h | 252 sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); } in expr2literal() function
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | bv_internalize.cpp | 107 sat::literal lit = expr2literal(e); in internalize()
470 add_def(def, expr2literal(n)); in internalize_le()
475 literal r = expr2literal(n); in internalize_carry()
476 literal l1 = expr2literal(n->get_arg(0)); in internalize_carry()
477 literal l2 = expr2literal(n->get_arg(1)); in internalize_carry()
478 literal l3 = expr2literal(n->get_arg(2)); in internalize_carry()
489 literal r = expr2literal(n); in internalize_xor3()
490 literal l1 = expr2literal(n->get_arg(0)); in internalize_xor3()
491 literal l2 = expr2literal(n->get_arg(1)); in internalize_xor3()
576 add_def(def, expr2literal(n)); in internalize_novfl()
[all …]
|
| H A D | bv_delay_internalize.cpp | 288 sat::literal no_overflow = expr2literal(n); in check_umul_no_overflow()
302 lits.push_back(expr2literal(n)); in check_umul_no_overflow()
331 sat::literal lit = expr2literal(n->get_expr()); in check_bool_eval()
|
| H A D | euf_relevancy.cpp | 87 sat::literal lit = expr2literal(c); in init_relevancy()
|
| 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()
|
| H A D | sat_th.cpp | 76 sat::literal th_euf_solver::expr2literal(expr* e) const { in expr2literal() function in euf::th_euf_solver
77 return ctx.expr2literal(e); in expr2literal()
|
| H A D | euf_internalize.cpp | 305 sat::literal lit1 = expr2literal(e); in axiomatize_basic()
310 sat::literal lit2 = expr2literal(e2); in axiomatize_basic()
|
| H A D | array_internalize.cpp | 29 auto lit = expr2literal(e); in internalize()
|
| H A D | sat_th.h | 131 sat::literal expr2literal(expr* e) const;
|
| H A D | bv_solver.cpp | 179 else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) { in display()
241 sat::literal antecedent = ~expr2literal(ne.eq()); in new_diseq_eh()
|
| H A D | fpa_solver.cpp | 94 return expr2literal(e); in internalize()
|
| H A D | euf_solver.h | 237 sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); } in expr2literal() function
|
| H A D | arith_axioms.cpp | 66 literal is_int = ctx.expr2literal(n); in mk_is_int_axiom()
|