Searched refs:isIntConstrThm (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 | 432 virtual Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) = 0;
436 …virtual Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) = 0;
|
| H A D | arith_theorem_producer.h | 316 Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
320 Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr);
|
| H A D | arith_theorem_producer_old.h | 316 Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
320 Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr);
|
| H A D | arith_theorem_producer3.h | 315 Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
319 Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr);
|
| H A D | arith_theorem_producer_old.cpp | 3253 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& con… in rafineStrictInteger() argument
3263 Expr intSum = isIntConstrThm.getExpr()[0]; in rafineStrictInteger()
3316 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); in rafineStrictInteger()
3321 pf = newPf("rafineStrictInteger", constr,newConstr, isIntConstrThm.getProof()); in rafineStrictInteger()
3332 Theorem ArithTheoremProducerOld::intEqualityRationalConstant(const Theorem& isIntConstrThm, const E… in intEqualityRationalConstant() argument
3347 Expr intSum = isIntConstrThm.getExpr()[0]; in intEqualityRationalConstant()
3358 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); in intEqualityRationalConstant()
3363 pf = newPf("intEqualityRationalConstant", constr, isIntConstrThm.getProof()); in intEqualityRationalConstant()
|
| H A D | arith_theorem_producer.cpp | 3068 Theorem ArithTheoremProducer::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr… in rafineStrictInteger() argument
3075 …CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn'… in rafineStrictInteger()
3111 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); in rafineStrictInteger()
3115 if (withProof()) pf = newPf("rafineStrictInteger", constr, newConstr,isIntConstrThm.getProof()); in rafineStrictInteger()
3133 Theorem ArithTheoremProducer::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr… in intEqualityRationalConstant() argument
|
| H A D | arith_theorem_producer3.cpp | 2970 Theorem ArithTheoremProducer3::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& const… in rafineStrictInteger() argument
2977 …CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn'… in rafineStrictInteger()
3013 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); in rafineStrictInteger()
3017 if (withProof()) pf = newPf("rafineStrictInteger", constr, isIntConstrThm.getProof()); in rafineStrictInteger()
3083 Theorem ArithTheoremProducer3::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Exp… in intEqualityRationalConstant() argument
|