| addInequalities(const Theorem &thm1, const Theorem &thm2)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonComboLikeTerms(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonDivide(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonDivideConst(const Expr &c, const Expr &d)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonDivideMult(const Expr &cx, const Expr &d)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonDividePlus(const Expr &e, const Expr &d)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonDivideVar(const Expr &e, const Expr &d)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonFlattenSum(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonInvert(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMult(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultConstConst(const Expr &c1, const Expr &c2)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultConstSum(const Expr &c1, const Expr &sum)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultMtermMterm(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultOne(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultTerm1Term2(const Expr &t1, const Expr &t2)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultTermConst(const Expr &c, const Expr &t)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonMultZero(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonPlus(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonPowConst(const Expr &pow)=0 | CVC3::ArithProofRules | [pure virtual] |
| canonUMinusToDivide(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)=0 | CVC3::ArithProofRules | [pure virtual] |
| constPredicate(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0 | CVC3::ArithProofRules | [pure virtual] |
| darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0 | CVC3::ArithProofRules | [pure virtual] |
| diseqToIneq(const Theorem &diseq)=0 | CVC3::ArithProofRules | [pure virtual] |
| dummyTheorem(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0 | CVC3::ArithProofRules | [pure virtual] |
| eqToIneq(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| equalLeaves1(const Theorem &thm)=0 | CVC3::ArithProofRules | [pure virtual] |
| equalLeaves2(const Theorem &thm)=0 | CVC3::ArithProofRules | [pure virtual] |
| equalLeaves3(const Theorem &thm)=0 | CVC3::ArithProofRules | [pure virtual] |
| equalLeaves4(const Theorem &thm)=0 | CVC3::ArithProofRules | [pure virtual] |
| expandDarkShadow(const Theorem &darkShadow)=0 | CVC3::ArithProofRules | [pure virtual] |
| expandGrayShadow(const Theorem &g)=0 | CVC3::ArithProofRules | [pure virtual] |
| expandGrayShadow0(const Theorem &g)=0 | CVC3::ArithProofRules | [pure virtual] |
| expandGrayShadowConst(const Theorem &g)=0 | CVC3::ArithProofRules | [pure virtual] |
| finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0 | CVC3::ArithProofRules | [pure virtual] |
| flipInequality(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| grayShadowConst(const Theorem &g)=0 | CVC3::ArithProofRules | [pure virtual] |
| implyNegatedInequality(const Expr &expr1, const Expr &expr2)=0 | CVC3::ArithProofRules | [pure virtual] |
| implyWeakerInequality(const Expr &expr1, const Expr &expr2)=0 | CVC3::ArithProofRules | [pure virtual] |
| integerSplit(const Expr &intVar, const Rational &intPoint)=0 | CVC3::ArithProofRules | [pure virtual] |
| intVarEqnConst(const Expr &eqn, const Theorem &isIntx)=0 | CVC3::ArithProofRules | [pure virtual] |
| isIntConst(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| leftMinusRight(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0 | CVC3::ArithProofRules | [pure virtual] |
| minusToPlus(const Expr &x, const Expr &y)=0 | CVC3::ArithProofRules | [pure virtual] |
| moveSumConstantRight(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| multEqn(const Expr &x, const Expr &y, const Expr &z)=0 | CVC3::ArithProofRules | [pure virtual] |
| multIneqn(const Expr &e, const Expr &z)=0 | CVC3::ArithProofRules | [pure virtual] |
| negatedInequality(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| oneElimination(const Expr &x)=0 | CVC3::ArithProofRules | [pure virtual] |
| plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind)=0 | CVC3::ArithProofRules | [pure virtual] |
| rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)=0 | CVC3::ArithProofRules | [pure virtual] |
| realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)=0 | CVC3::ArithProofRules | [pure virtual] |
| realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)=0 | CVC3::ArithProofRules | [pure virtual] |
| rightMinusLeft(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| splitGrayShadow(const Theorem &g)=0 | CVC3::ArithProofRules | [pure virtual] |
| trustedRewrite(const Expr &expr1, const Expr &expr2)=0 | CVC3::ArithProofRules | [pure virtual] |
| uMinusToMult(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| varToMult(const Expr &e)=0 | CVC3::ArithProofRules | [pure virtual] |
| ~ArithProofRules() | CVC3::ArithProofRules | [inline, virtual] |
