Searched refs:PR_IFF_TRUE (Results 1 – 8 of 8) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/api/ |
| H A D | api_ast.cpp | 1003 case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE; in Z3_get_decl_kind()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/proofs/ |
| H A D | proof_checker.cpp | 628 case PR_IFF_TRUE: { in check1_basic()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/proofs/ |
| H A D | proof_checker.cpp | 628 case PR_IFF_TRUE: { in check1_basic()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
| H A D | api_ast.cpp | 995 case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE; in Z3_get_decl_kind()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | ast.cpp | 840 case PR_IFF_TRUE: return mk_proof_decl("iff-true", k, 1, m_iff_true_decl); in mk_proof_decl()
2775 return mk_app(basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true())); in mk_iff_true()
|
| H A D | ast.h | 1107 …PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_A… enumerator
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | ast.cpp | 905 case PR_IFF_TRUE: return mk_proof_decl("iff-true", k, 1, m_iff_true_decl); in mk_proof_decl()
2853 return mk_app(m_basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true())); in mk_iff_true()
|
| H A D | ast.h | 1104 …PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_A… enumerator
|