CVC3
CVC3::ArithTheoremProducerOld Member List

This is the complete list of members for CVC3::ArithTheoremProducerOld, including all inherited members.

addInequalities(const Theorem &thm1, const Theorem &thm2)CVC3::ArithTheoremProducerOldvirtual
addInequalities(const std::vector< Theorem > &thms)CVC3::ArithTheoremProducerOldvirtual
ArithTheoremProducerOld(TheoremManager *tm, TheoryArithOld *theoryArith)CVC3::ArithTheoremProducerOldinline
canonCombineLikeTerms(const std::vector< Expr > &sumExprs)CVC3::ArithTheoremProducerOldvirtual
canonComboLikeTerms(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonDivide(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonDivideConst(const Expr &c, const Expr &d)CVC3::ArithTheoremProducerOldvirtual
canonDivideMult(const Expr &cx, const Expr &d)CVC3::ArithTheoremProducerOldvirtual
canonDividePlus(const Expr &e, const Expr &d)CVC3::ArithTheoremProducerOldvirtual
canonDivideVar(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonFlattenSum(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonInvert(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonInvertConst(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonInvertLeaf(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonInvertMult(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonInvertPow(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonMult(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonMultConstConst(const Expr &c1, const Expr &c2)CVC3::ArithTheoremProducerOldvirtual
canonMultConstMult(const Expr &c, const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonMultConstPlus(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultConstSum(const Expr &c1, const Expr &sum)CVC3::ArithTheoremProducerOldvirtual
canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)CVC3::ArithTheoremProducerOldvirtual
canonMultLeafLeaf(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultLeafOrPowMult(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultLeafOrPowOrMultPlus(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultMtermMterm(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonMultOne(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonMultPlusPlus(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultPowLeaf(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultPowPow(const Expr &e1, const Expr &e2)CVC3::ArithTheoremProducerOldvirtual
canonMultTerm1Term2(const Expr &t1, const Expr &t2)CVC3::ArithTheoremProducerOldvirtual
canonMultTermConst(const Expr &c, const Expr &t)CVC3::ArithTheoremProducerOldvirtual
canonMultZero(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonPlus(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
canonPowConst(const Expr &pow)CVC3::ArithTheoremProducerOldvirtual
canonUMinusToDivide(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)CVC3::ArithTheoremProducerOldvirtual
compactNonLinearTerm(const Expr &nonLinear)CVC3::ArithTheoremProducerOldvirtual
constPredicate(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
constRHSGrayShadow(const Rational &c, const Rational &b, const Rational &a)CVC3::ArithTheoremProducerOld
create_t(const Expr &eqn)CVC3::ArithTheoremProducerOldprivate
create_t2(const Expr &lhs, const Expr &rhs, const Expr &t)CVC3::ArithTheoremProducerOldprivate
create_t3(const Expr &lhs, const Expr &rhs, const Expr &t)CVC3::ArithTheoremProducerOldprivate
cycleConflict(const std::vector< Theorem > &inequalitites)CVC3::ArithTheoremProducerOldvirtual
d_checkProofsCVC3::TheoremProducerprotected
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_theoryArithCVC3::ArithTheoremProducerOldprivate
d_tmCVC3::TheoremProducerprotected
darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)CVC3::ArithTheoremProducerOldvirtual
darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)CVC3::ArithTheoremProducerOldvirtual
darkShadow(const Expr &lhs, const Expr &rhs)CVC3::ArithTheoremProducerOldinline
diseqToIneq(const Theorem &diseq)CVC3::ArithTheoremProducerOldvirtual
divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z)CVC3::ArithTheoremProducerOldvirtual
dummyTheorem(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
elimPower(const Expr &expr)CVC3::ArithTheoremProducerOldvirtual
elimPowerConst(const Expr &expr, const Rational &root)CVC3::ArithTheoremProducerOldvirtual
eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)CVC3::ArithTheoremProducerOldvirtual
eqToIneq(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
equalLeaves1(const Theorem &e)CVC3::ArithTheoremProducerOldvirtual
equalLeaves2(const Theorem &e)CVC3::ArithTheoremProducerOldvirtual
equalLeaves3(const Theorem &e)CVC3::ArithTheoremProducerOldvirtual
equalLeaves4(const Theorem &e)CVC3::ArithTheoremProducerOldvirtual
evenPowerEqNegConst(const Expr &expr)CVC3::ArithTheoremProducerOldvirtual
expandDarkShadow(const Theorem &darkShadow)CVC3::ArithTheoremProducerOldvirtual
expandGrayShadow(const Theorem &grayShadow)CVC3::ArithTheoremProducerOldvirtual
expandGrayShadow0(const Theorem &grayShadow)CVC3::ArithTheoremProducerOldvirtual
expandGrayShadowConst(const Theorem &grayShadow)CVC3::ArithTheoremProducerOldvirtual
expandGrayShadowRewrite(const Expr &theShadow)CVC3::ArithTheoremProducerOldvirtual
f(const Rational &i, const Rational &m)CVC3::ArithTheoremProducerOldprivate
finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)CVC3::ArithTheoremProducerOldvirtual
flipInequality(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
getLeaves(const Expr &e, std::set< Rational > &s, ExprHashMap< bool > &cache)CVC3::ArithTheoremProducerOldprivate
grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)CVC3::ArithTheoremProducerOldinline
grayShadowConst(const Theorem &g)CVC3::ArithTheoremProducerOldvirtual
greaterthan(const Expr &, const Expr &)CVC3::ArithTheoremProducerOldstatic
implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)CVC3::ArithTheoremProducerOldvirtual
implyEqualities(const std::vector< Theorem > &inequalities)CVC3::ArithTheoremProducerOldvirtual
implyNegatedInequality(const Expr &expr1, const Expr &expr2)CVC3::ArithTheoremProducerOldvirtual
implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)CVC3::ArithTheoremProducerOldvirtual
implyWeakerInequality(const Expr &expr1, const Expr &expr2)CVC3::ArithTheoremProducerOldvirtual
implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)CVC3::ArithTheoremProducerOldvirtual
integerSplit(const Expr &intVar, const Rational &intPoint)CVC3::ArithTheoremProducerOldvirtual
intEqIrrational(const Expr &expr, const Theorem &isInt)CVC3::ArithTheoremProducerOldvirtual
intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)CVC3::ArithTheoremProducerOldvirtual
intType()CVC3::ArithTheoremProducerOldinline
intVarEqnConst(const Expr &eqn, const Theorem &isIntx)CVC3::ArithTheoremProducerOldvirtual
isIntConst(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
IsIntegerElim(const Theorem &isIntx)CVC3::ArithTheoremProducerOldvirtual
leftMinusRight(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)CVC3::ArithTheoremProducerOldvirtual
lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)CVC3::ArithTheoremProducerOldvirtual
minusToPlus(const Expr &x, const Expr &y)CVC3::ArithTheoremProducerOldvirtual
modEq(const Rational &i, const Rational &m)CVC3::ArithTheoremProducerOldprivate
monomialModM(const Expr &e, const Rational &m, const Rational &divisor)CVC3::ArithTheoremProducerOldprivate
monomialMulF(const Expr &e, const Rational &m, const Rational &divisor)CVC3::ArithTheoremProducerOldprivate
moveSumConstantRight(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
multEqn(const Expr &x, const Expr &y, const Expr &z)CVC3::ArithTheoremProducerOldvirtual
multEqZero(const Expr &expr)CVC3::ArithTheoremProducerOldvirtual
multIneqn(const Expr &e, const Expr &z)CVC3::ArithTheoremProducerOldvirtual
negatedInequality(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducerinlineprotected
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::TheoremProducerinlineprotected
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
nonLinearIneqSignSplit(const Theorem &ineqThm)CVC3::ArithTheoremProducerOldvirtual
oneElimination(const Expr &x)CVC3::ArithTheoremProducerOldvirtual
plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind)CVC3::ArithTheoremProducerOldvirtual
powEqZero(const Expr &expr)CVC3::ArithTheoremProducerOldvirtual
powerOfOne(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)CVC3::ArithTheoremProducerOldvirtual
rat(Rational r)CVC3::ArithTheoremProducerOldinline
realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)CVC3::ArithTheoremProducerOldvirtual
realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)CVC3::ArithTheoremProducerOldvirtual
realType()CVC3::ArithTheoremProducerOldinline
rewriteLeavesConst(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
rightMinusLeft(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)CVC3::ArithTheoremProducerOldvirtual
simplifiedMultExpr(std::vector< Expr > &mulKids)CVC3::ArithTheoremProducerOldvirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
splitGrayShadow(const Theorem &grayShadow)CVC3::ArithTheoremProducerOldvirtual
splitGrayShadowSmall(const Theorem &grayShadow)CVC3::ArithTheoremProducerOldvirtual
substitute(const Expr &term, ExprMap< Expr > &eMap)CVC3::ArithTheoremProducerOldprivate
sumModM(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)CVC3::ArithTheoremProducerOldprivate
sumMulF(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)CVC3::ArithTheoremProducerOldprivate
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
trustedRewrite(const Expr &expr1, const Expr &expr2)CVC3::ArithTheoremProducerOldvirtual
uMinusToMult(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
varToMult(const Expr &e)CVC3::ArithTheoremProducerOldvirtual
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
~ArithProofRules()CVC3::ArithProofRulesinlinevirtual
~TheoremProducer()CVC3::TheoremProducerinlinevirtual