| /dports/math/z3/z3-z3-4.8.13/src/ast/normal_forms/ |
| H A D | elim_term_ite.cpp | 28 proof_ref new_def_pr(m); in reduce_app() local
31 if (!m_defined_names.mk_name(r, new_def, new_def_pr, new_r, result_pr)) { in reduce_app()
37 m_new_defs.push_back(justified_expr(m, new_def, new_def_pr)); in reduce_app()
|
| H A D | defined_names.cpp | 68 bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
247 bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n… in mk_name() argument
279 new_def_pr = m.mk_def_intro(new_def); in mk_name()
280 pr = m.mk_apply_def(e, n, new_def_pr); in mk_name()
333 bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proo… in mk_name() argument
334 return m_impl->mk_name(e, new_def, new_def_pr, n, pr); in mk_name()
337 bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, … in mk_pos_name() argument
338 return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr); in mk_pos_name()
|
| H A D | defined_names.h | 65 bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
77 …bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr…
|
| H A D | name_exprs.cpp | 47 proof_ref new_def_pr(m); in gen_name_for_expr() local
49 if (m_defined_names.mk_name(n, new_def, new_def_pr, m_r, m_pr)) { in gen_name_for_expr()
52 m_def_proofs->push_back(new_def_pr); in gen_name_for_expr()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/normal_forms/ |
| H A D | elim_term_ite.cpp | 28 proof_ref new_def_pr(m); in reduce_app() local
31 if (!m_defined_names.mk_name(r, new_def, new_def_pr, new_r, result_pr)) { in reduce_app()
37 m_new_defs.push_back(justified_expr(m, new_def, new_def_pr)); in reduce_app()
|
| H A D | defined_names.cpp | 68 bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
245 bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n… in mk_name() argument
277 new_def_pr = m.mk_def_intro(new_def); in mk_name()
278 pr = m.mk_apply_def(e, n, new_def_pr); in mk_name()
331 bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proo… in mk_name() argument
332 return m_impl->mk_name(e, new_def, new_def_pr, n, pr); in mk_name()
335 bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, … in mk_pos_name() argument
336 return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr); in mk_pos_name()
|
| H A D | defined_names.h | 65 bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
77 …bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr…
|
| H A D | name_exprs.cpp | 47 proof_ref new_def_pr(m); in gen_name_for_expr() local
49 if (m_defined_names.mk_name(n, new_def, new_def_pr, m_r, m_pr)) { in gen_name_for_expr()
52 m_def_proofs->push_back(new_def_pr); in gen_name_for_expr()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/ |
| H A D | elim_term_ite_tactic.cpp | 49 proof_ref new_def_pr(m); in reduce_app() local
51 if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) { in reduce_app()
52 m_goal->assert_expr(new_def, new_def_pr, nullptr); in reduce_app()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
| H A D | elim_term_ite_tactic.cpp | 49 proof_ref new_def_pr(m); in reduce_app() local
51 if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) { in reduce_app()
52 m_goal->assert_expr(new_def, new_def_pr, nullptr); in reduce_app()
|