Searched refs:isIntE (Results 1 – 6 of 6) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_arith3.h | 141 Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
|
| H A D | theory_arith_new.h | 143 Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
|
| H A D | theory_arith_old.h | 165 Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith3.cpp | 76 Theorem TheoryArith3::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() argument
79 if(e == isIntE) return thm; in isIntegerDerive()
86 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
|
| H A D | theory_arith_new.cpp | 76 Theorem TheoryArithNew::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() argument
79 if(e == isIntE) return thm; in isIntegerDerive()
86 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
|
| H A D | theory_arith_old.cpp | 81 Theorem TheoryArithOld::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() argument
84 if(e == isIntE) return thm; in isIntegerDerive()
91 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
|