CVC3
|
This is the complete list of members for CVC3::ArithTheoremProducer, including all inherited members.
addInequalities(const Theorem &thm1, const Theorem &thm2) | CVC3::ArithTheoremProducer | virtual |
addInequalities(const std::vector< Theorem > &thms) | CVC3::ArithTheoremProducer | virtual |
ArithTheoremProducer(TheoremManager *tm, TheoryArithNew *theoryArith) | CVC3::ArithTheoremProducer | inline |
canonCombineLikeTerms(const std::vector< Expr > &sumExprs) | CVC3::ArithTheoremProducer | virtual |
canonComboLikeTerms(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonDivide(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonDivideConst(const Expr &c, const Expr &d) | CVC3::ArithTheoremProducer | virtual |
canonDivideMult(const Expr &cx, const Expr &d) | CVC3::ArithTheoremProducer | virtual |
canonDividePlus(const Expr &e, const Expr &d) | CVC3::ArithTheoremProducer | virtual |
canonDivideVar(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonFlattenSum(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonInvert(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonInvertConst(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonInvertLeaf(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonInvertMult(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonInvertPow(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonMult(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonMultConstConst(const Expr &c1, const Expr &c2) | CVC3::ArithTheoremProducer | virtual |
canonMultConstMult(const Expr &c, const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonMultConstPlus(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultConstSum(const Expr &c1, const Expr &sum) | CVC3::ArithTheoremProducer | virtual |
canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t) | CVC3::ArithTheoremProducer | virtual |
canonMultLeafLeaf(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultLeafOrPowMult(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultLeafOrPowOrMultPlus(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultMtermMterm(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonMultOne(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonMultPlusPlus(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultPowLeaf(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultPowPow(const Expr &e1, const Expr &e2) | CVC3::ArithTheoremProducer | virtual |
canonMultTerm1Term2(const Expr &t1, const Expr &t2) | CVC3::ArithTheoremProducer | virtual |
canonMultTermConst(const Expr &c, const Expr &t) | CVC3::ArithTheoremProducer | virtual |
canonMultZero(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonPlus(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
canonPowConst(const Expr &pow) | CVC3::ArithTheoremProducer | virtual |
canonUMinusToDivide(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
clashingBounds(const Theorem &lowerBound, const Theorem &upperBound) | CVC3::ArithTheoremProducer | virtual |
compactNonLinearTerm(const Expr &nonLinear) | CVC3::ArithTheoremProducer | virtual |
constPredicate(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
constRHSGrayShadow(const Rational &c, const Rational &b, const Rational &a) | CVC3::ArithTheoremProducer | |
create_t(const Expr &eqn) | CVC3::ArithTheoremProducer | private |
create_t2(const Expr &lhs, const Expr &rhs, const Expr &t) | CVC3::ArithTheoremProducer | private |
create_t3(const Expr &lhs, const Expr &rhs, const Expr &t) | CVC3::ArithTheoremProducer | private |
cycleConflict(const std::vector< Theorem > &inequalitites) | CVC3::ArithTheoremProducer | virtual |
d_checkProofs | CVC3::TheoremProducer | protected |
d_em | CVC3::TheoremProducer | protected |
d_hole | CVC3::TheoremProducer | protected |
d_pfOp | CVC3::TheoremProducer | protected |
d_theoryArith | CVC3::ArithTheoremProducer | private |
d_tm | CVC3::TheoremProducer | protected |
darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) | CVC3::ArithTheoremProducer | virtual |
darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) | CVC3::ArithTheoremProducer | virtual |
darkShadow(const Expr &lhs, const Expr &rhs) | CVC3::ArithTheoremProducer | inline |
diseqToIneq(const Theorem &diseq) | CVC3::ArithTheoremProducer | virtual |
divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z) | CVC3::ArithTheoremProducer | virtual |
dummyTheorem(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
elimPower(const Expr &expr) | CVC3::ArithTheoremProducer | virtual |
elimPowerConst(const Expr &expr, const Rational &root) | CVC3::ArithTheoremProducer | virtual |
eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars) | CVC3::ArithTheoremProducer | virtual |
eqToIneq(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
equalLeaves1(const Theorem &e) | CVC3::ArithTheoremProducer | virtual |
equalLeaves2(const Theorem &e) | CVC3::ArithTheoremProducer | virtual |
equalLeaves3(const Theorem &e) | CVC3::ArithTheoremProducer | virtual |
equalLeaves4(const Theorem &e) | CVC3::ArithTheoremProducer | virtual |
evenPowerEqNegConst(const Expr &expr) | CVC3::ArithTheoremProducer | virtual |
expandDarkShadow(const Theorem &darkShadow) | CVC3::ArithTheoremProducer | virtual |
expandGrayShadow(const Theorem &grayShadow) | CVC3::ArithTheoremProducer | virtual |
expandGrayShadow0(const Theorem &grayShadow) | CVC3::ArithTheoremProducer | virtual |
expandGrayShadowConst(const Theorem &grayShadow) | CVC3::ArithTheoremProducer | virtual |
expandGrayShadowRewrite(const Expr &theShadow) | CVC3::ArithTheoremProducer | virtual |
f(const Rational &i, const Rational &m) | CVC3::ArithTheoremProducer | private |
finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt) | CVC3::ArithTheoremProducer | virtual |
flipInequality(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2) | CVC3::ArithTheoremProducer | inline |
grayShadowConst(const Theorem &g) | CVC3::ArithTheoremProducer | virtual |
greaterthan(const Expr &, const Expr &) | CVC3::ArithTheoremProducer | static |
implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2) | CVC3::ArithTheoremProducer | virtual |
implyEqualities(const std::vector< Theorem > &inequalities) | CVC3::ArithTheoremProducer | virtual |
implyNegatedInequality(const Expr &expr1, const Expr &expr2) | CVC3::ArithTheoremProducer | virtual |
implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied) | CVC3::ArithTheoremProducer | virtual |
implyWeakerInequality(const Expr &expr1, const Expr &expr2) | CVC3::ArithTheoremProducer | virtual |
implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied) | CVC3::ArithTheoremProducer | virtual |
integerSplit(const Expr &intVar, const Rational &intPoint) | CVC3::ArithTheoremProducer | virtual |
intEqIrrational(const Expr &expr, const Theorem &isInt) | CVC3::ArithTheoremProducer | virtual |
intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr) | CVC3::ArithTheoremProducer | virtual |
intType() | CVC3::ArithTheoremProducer | inline |
intVarEqnConst(const Expr &eqn, const Theorem &isIntx) | CVC3::ArithTheoremProducer | virtual |
isIntConst(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
IsIntegerElim(const Theorem &isIntx) | CVC3::ArithTheoremProducer | virtual |
leftMinusRight(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight) | CVC3::ArithTheoremProducer | virtual |
lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight) | CVC3::ArithTheoremProducer | virtual |
minusToPlus(const Expr &x, const Expr &y) | CVC3::ArithTheoremProducer | virtual |
modEq(const Rational &i, const Rational &m) | CVC3::ArithTheoremProducer | private |
monomialModM(const Expr &e, const Rational &m, const Rational &divisor) | CVC3::ArithTheoremProducer | private |
monomialMulF(const Expr &e, const Rational &m, const Rational &divisor) | CVC3::ArithTheoremProducer | private |
moveSumConstantRight(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
multEqn(const Expr &x, const Expr &y, const Expr &z) | CVC3::ArithTheoremProducer | virtual |
multEqZero(const Expr &expr) | CVC3::ArithTheoremProducer | virtual |
multIneqn(const Expr &e, const Expr &z) | CVC3::ArithTheoremProducer | virtual |
negatedInequality(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVC3::TheoremProducer | inlineprotected |
newLabel(const Expr &e) | CVC3::TheoremProducer | |
newPf(const std::string &name) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e1, const Expr &e2) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) | CVC3::TheoremProducer | |
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
newPf(const std::string &name, const std::vector< Expr > &args) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
newPf(const std::string &name, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
newPf(const Proof &label, const Expr &frm, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const Proof &label, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) | CVC3::TheoremProducer | |
newPf(const std::vector< Proof > &labels, const Proof &pf) | CVC3::TheoremProducer | |
newReflTheorem(const Expr &e) | CVC3::TheoremProducer | inlineprotected |
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
nonLinearIneqSignSplit(const Theorem &ineqThm) | CVC3::ArithTheoremProducer | virtual |
oneElimination(const Expr &x) | CVC3::ArithTheoremProducer | virtual |
plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind) | CVC3::ArithTheoremProducer | virtual |
powEqZero(const Expr &expr) | CVC3::ArithTheoremProducer | virtual |
powerOfOne(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr) | CVC3::ArithTheoremProducer | virtual |
rat(Rational r) | CVC3::ArithTheoremProducer | inline |
realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta) | CVC3::ArithTheoremProducer | virtual |
realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha) | CVC3::ArithTheoremProducer | virtual |
realType() | CVC3::ArithTheoremProducer | inline |
rewriteLeavesConst(const Expr &e) | CVC3::ArithProofRules | virtual |
rightMinusLeft(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS) | CVC3::ArithTheoremProducer | virtual |
simplifiedMultExpr(std::vector< Expr > &mulKids) | CVC3::ArithTheoremProducer | virtual |
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVC3::TheoremProducer | protected |
splitGrayShadow(const Theorem &grayShadow) | CVC3::ArithTheoremProducer | virtual |
splitGrayShadowSmall(const Theorem &grayShadow) | CVC3::ArithTheoremProducer | virtual |
substitute(const Expr &term, ExprMap< Expr > &eMap) | CVC3::ArithTheoremProducer | private |
sumModM(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor) | CVC3::ArithTheoremProducer | private |
sumMulF(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor) | CVC3::ArithTheoremProducer | private |
TheoremProducer(TheoremManager *tm) | CVC3::TheoremProducer | |
trustedRewrite(const Expr &expr1, const Expr &expr2) | CVC3::ArithTheoremProducer | virtual |
uMinusToMult(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
varToMult(const Expr &e) | CVC3::ArithTheoremProducer | virtual |
withAssumptions() | CVC3::TheoremProducer | inline |
withProof() | CVC3::TheoremProducer | inline |
~ArithProofRules() | CVC3::ArithProofRules | inlinevirtual |
~TheoremProducer() | CVC3::TheoremProducer | inlinevirtual |