Searched refs:isIntegerDerive (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 | 72 return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e)); in isIntegerThm()
76 Theorem TheoryArith3::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() function in TheoryArith3
86 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
2440 Theorem res(isIntegerDerive(e, typePred(e[0]))); in rewrite()
|
| H A D | theory_arith_new.cpp | 72 return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e)); in isIntegerThm()
76 Theorem TheoryArithNew::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() function in TheoryArithNew
86 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
|
| H A D | theory_arith_old.cpp | 77 return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e)); in isIntegerThm()
81 Theorem TheoryArithOld::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { in isIntegerDerive() function in TheoryArithOld
91 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); in isIntegerDerive()
3251 Theorem res(isIntegerDerive(e, typePred(e[0]))); in rewrite()
|