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()
|