Searched refs:tLEalpha (Results 1 – 7 of 7) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | arith_proof_rules.h | 200 const Theorem& tLEalpha) = 0;
|
| H A D | arith_theorem_producer.cpp | 1583 const Theorem& tLEalpha) in realShadowEq() argument
1586 const Expr& expr2 = tLEalpha.getExpr(); in realShadowEq()
1590 alphaLEt.toString() + tLEalpha.toString()); in realShadowEq()
1595 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1600 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1602 Assumptions a(alphaLEt, tLEalpha); in realShadowEq()
1607 pfs.push_back(tLEalpha.getProof()); in realShadowEq()
1608 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); in realShadowEq()
|
| H A D | arith_theorem_producer3.cpp | 1540 const Theorem& tLEalpha) in realShadowEq() argument
1543 const Expr& expr2 = tLEalpha.getExpr(); in realShadowEq()
1547 alphaLEt.toString() + tLEalpha.toString()); in realShadowEq()
1552 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1557 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1559 Assumptions a(alphaLEt, tLEalpha); in realShadowEq()
1564 pfs.push_back(tLEalpha.getProof()); in realShadowEq()
1565 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); in realShadowEq()
|
| H A D | arith_theorem_producer.h | 246 Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
|
| H A D | arith_theorem_producer_old.h | 245 Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
|
| H A D | arith_theorem_producer3.h | 245 Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
|
| H A D | arith_theorem_producer_old.cpp | 1738 const Theorem& tLEalpha) in realShadowEq() argument
1741 const Expr& expr2 = tLEalpha.getExpr(); in realShadowEq()
1745 alphaLEt.toString() + tLEalpha.toString()); in realShadowEq()
1750 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1755 alphaLEt.toString() + " , " + tLEalpha.toString()); in realShadowEq()
1757 Assumptions a(alphaLEt, tLEalpha); in realShadowEq()
1762 pfs.push_back(tLEalpha.getProof()); in realShadowEq()
1763 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); in realShadowEq()
|