CVC3
|
This is the complete list of members for CVC3::ArithProofRules, including all inherited members.
addInequalities(const Theorem &thm1, const Theorem &thm2)=0 | CVC3::ArithProofRules | pure virtual |
addInequalities(const std::vector< Theorem > &thms)=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 |
compactNonLinearTerm(const Expr &nonLinear)=0 | CVC3::ArithProofRules | pure virtual |
constPredicate(const Expr &e)=0 | CVC3::ArithProofRules | pure virtual |
cycleConflict(const std::vector< Theorem > &inequalitites)=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 |
divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z)=0 | CVC3::ArithProofRules | pure virtual |
dummyTheorem(const Expr &e)=0 | CVC3::ArithProofRules | pure virtual |
elimPower(const Expr &expr)=0 | CVC3::ArithProofRules | pure virtual |
elimPowerConst(const Expr &expr, const Rational &root)=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 |
evenPowerEqNegConst(const Expr &expr)=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 |
expandGrayShadowRewrite(const Expr &theShadow)=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 |
implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)=0 | CVC3::ArithProofRules | pure virtual |
implyEqualities(const std::vector< Theorem > &inequalities)=0 | CVC3::ArithProofRules | pure virtual |
implyNegatedInequality(const Expr &expr1, const Expr &expr2)=0 | CVC3::ArithProofRules | pure virtual |
implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0 | CVC3::ArithProofRules | pure virtual |
implyWeakerInequality(const Expr &expr1, const Expr &expr2)=0 | CVC3::ArithProofRules | pure virtual |
implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0 | CVC3::ArithProofRules | pure virtual |
integerSplit(const Expr &intVar, const Rational &intPoint)=0 | CVC3::ArithProofRules | pure virtual |
intEqIrrational(const Expr &expr, const Theorem &isInt)=0 | CVC3::ArithProofRules | pure virtual |
intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)=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 |
IsIntegerElim(const Theorem &isIntx)=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 |
lessThanToLERewrite(const Expr &ineq, 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 |
multEqZero(const Expr &expr)=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 |
nonLinearIneqSignSplit(const Theorem &ineqThm)=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 |
powEqZero(const Expr &expr)=0 | CVC3::ArithProofRules | pure virtual |
powerOfOne(const Expr &e)=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 |
rewriteLeavesConst(const Expr &e) | CVC3::ArithProofRules | virtual |
rightMinusLeft(const Expr &e)=0 | CVC3::ArithProofRules | pure virtual |
simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)=0 | CVC3::ArithProofRules | pure virtual |
splitGrayShadow(const Theorem &g)=0 | CVC3::ArithProofRules | pure virtual |
splitGrayShadowSmall(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 | inlinevirtual |