Searched refs:alphaLEt (Results 1 – 10 of 10) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | arith_proof_rules.h | 199 virtual Theorem realShadowEq(const Theorem& alphaLEt,
|
| H A D | arith_theorem_producer.cpp | 1582 Theorem ArithTheoremProducer::realShadowEq(const Theorem& alphaLEt, in realShadowEq() argument
1585 const Expr& expr1 = alphaLEt.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()
1606 pfs.push_back(alphaLEt.getProof()); in realShadowEq()
1608 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); in realShadowEq()
|
| H A D | arith_theorem_producer3.cpp | 1539 Theorem ArithTheoremProducer3::realShadowEq(const Theorem& alphaLEt, in realShadowEq() argument
1542 const Expr& expr1 = alphaLEt.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()
1563 pfs.push_back(alphaLEt.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 | 1737 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt, in realShadowEq() argument
1740 const Expr& expr1 = alphaLEt.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()
1761 pfs.push_back(alphaLEt.getProof()); in realShadowEq()
1763 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); in realShadowEq()
|
| H A D | theory_arith3.cpp | 1948 const Expr& alphaLEt = thm1.getExpr(); in processFiniteInterval() local
1949 const Expr& alpha = alphaLEt[0]; in processFiniteInterval()
1950 const Expr& t = alphaLEt[1]; in processFiniteInterval()
|
| H A D | theory_arith_new.cpp | 1199 const Expr& alphaLEt = thm1.getExpr(); in processFiniteInterval() local
1200 const Expr& alpha = alphaLEt[0]; in processFiniteInterval()
1201 const Expr& t = alphaLEt[1]; in processFiniteInterval()
|
| H A D | theory_arith_old.cpp | 2404 const Expr& alphaLEt = thm1.getExpr(); in processFiniteInterval() local
2405 const Expr& alpha = alphaLEt[0]; in processFiniteInterval()
2406 const Expr& t = alphaLEt[1]; in processFiniteInterval()
|