| addAssoc(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | [private] |
| addInvR(const Expr &x) | CVCL::RefinedArithTheoremProducer | [private] |
| addLID(const Expr &x) | CVCL::RefinedArithTheoremProducer | [private] |
| addR(const Theorem &xEy, const Expr &z) | CVCL::RefinedArithTheoremProducer | |
| addRCancel(const Theorem &t) | CVCL::RefinedArithTheoremProducer | |
| addRID(const Expr &x) | CVCL::RefinedArithTheoremProducer | |
| addSymm(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | [private] |
| arithmetic(const Expr &lhs, const Expr &rhs) | CVCL::RefinedArithTheoremProducer | |
| ArithTheoremProducer(TheoremManager *tm, TheoryArith *theoryArith) | CVCL::ArithTheoremProducer | [inline] |
| cancelR(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | |
| canonCombineLikeTerms(const std::vector< Expr > &sumExprs) | CVCL::ArithTheoremProducer | [virtual] |
| canonComboLikeTerms(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonDivide(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonDivideConst(const Expr &c, const Expr &d) | CVCL::ArithTheoremProducer | [virtual] |
| canonDivideMult(const Expr &cx, const Expr &d) | CVCL::ArithTheoremProducer | [virtual] |
| canonDividePlus(const Expr &e, const Expr &d) | CVCL::ArithTheoremProducer | [virtual] |
| canonDivideVar(const Expr &e, const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonFlattenSum(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonInvert(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonInvertConst(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonInvertLeaf(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonInvertMult(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonInvertPow(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonMult(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultConstConst(const Expr &c1, const Expr &c2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultConstMult(const Expr &c, const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultConstPlus(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultConstSum(const Expr &c1, const Expr &sum) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultLeafLeaf(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultLeafOrPowMult(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultLeafOrPowOrMultPlus(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultMtermMterm(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultOne(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultPlusPlus(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultPowLeaf(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultPowPow(const Expr &e1, const Expr &e2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultTerm1Term2(const Expr &t1, const Expr &t2) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultTermConst(const Expr &c, const Expr &t) | CVCL::ArithTheoremProducer | [virtual] |
| canonMultZero(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| canonPlus(const Expr &e) | CVCL::RefinedArithTheoremProducer | [virtual] |
| canonPowConst(const Expr &pow) | CVCL::ArithTheoremProducer | [virtual] |
| canonUMinusToDivide(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| constPredicate(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| constRHSGrayShadow(const Rational &c, const Rational &b, const Rational &a) | CVCL::ArithTheoremProducer | |
| core | CVCL::RefinedArithTheoremProducer | [private] |
| d_checkProofs | CVCL::TheoremProducer | [protected] |
| d_em | CVCL::RefinedArithTheoremProducer | [private] |
| d_hole | CVCL::TheoremProducer | [protected] |
| d_pfOp | CVCL::TheoremProducer | [protected] |
| d_tm | CVCL::TheoremProducer | [protected] |
| darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) | CVCL::ArithTheoremProducer | [virtual] |
| darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) | CVCL::ArithTheoremProducer | [virtual] |
| darkShadow(const Expr &lhs, const Expr &rhs) | CVCL::ArithTheoremProducer | [inline] |
| diseqToIneq(const Theorem &diseq) | CVCL::ArithTheoremProducer | [virtual] |
| distribL(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | [private] |
| distribR(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | |
| divideDef(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | |
| eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars) | CVCL::ArithTheoremProducer | [virtual] |
| equalLeaves1(const Theorem &e) | CVCL::ArithTheoremProducer | [virtual] |
| equalLeaves2(const Theorem &e) | CVCL::ArithTheoremProducer | [virtual] |
| equalLeaves3(const Theorem &e) | CVCL::ArithTheoremProducer | [virtual] |
| equalLeaves4(const Theorem &e) | CVCL::ArithTheoremProducer | [virtual] |
| eval(const Expr &rational_expr) | CVCL::RefinedArithTheoremProducer | [private] |
| expandDarkShadow(const Theorem &darkShadow) | CVCL::ArithTheoremProducer | [virtual] |
| expandGrayShadow(const Theorem &grayShadow) | CVCL::ArithTheoremProducer | [virtual] |
| expandGrayShadow0(const Theorem &grayShadow) | CVCL::ArithTheoremProducer | [virtual] |
| expandGrayShadowConst(const Theorem &grayShadow) | CVCL::ArithTheoremProducer | [virtual] |
| finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt) | CVCL::ArithTheoremProducer | [virtual] |
| flipInequality(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| frac(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | |
| grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2) | CVCL::ArithTheoremProducer | [inline] |
| grayShadowConst(const Theorem &g) | CVCL::ArithTheoremProducer | [virtual] |
| greaterthan(const Expr &, const Expr &) | CVCL::ArithTheoremProducer | [static] |
| intType() | CVCL::ArithTheoremProducer | [inline] |
| intVarEqnConst(const Expr &eqn, const Theorem &isIntx) | CVCL::ArithTheoremProducer | [virtual] |
| inv(const Expr &x) | CVCL::RefinedArithTheoremProducer | |
| isIntConst(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight) | CVCL::ArithTheoremProducer | [virtual] |
| ltAddR(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | |
| ltScale(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | |
| ltTrans(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | |
| minusDef(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | |
| minusToPlus(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | [virtual] |
| multAssoc(const Expr &x, const Expr &y, const Expr &z) | CVCL::RefinedArithTheoremProducer | [private] |
| multEqn(const Expr &x, const Expr &y, const Expr &z) | CVCL::ArithTheoremProducer | [virtual] |
| multIneqn(const Expr &e, const Expr &z) | CVCL::ArithTheoremProducer | [virtual] |
| multInvR(const Expr &x) | CVCL::RefinedArithTheoremProducer | [private] |
| multLID(const Expr &x) | CVCL::RefinedArithTheoremProducer | [private] |
| multSymm(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | [private] |
| multZeroL(const Expr &e) | CVCL::RefinedArithTheoremProducer | |
| neg(const Expr &x) | CVCL::RefinedArithTheoremProducer | |
| negatedInequality(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVCL::TheoremProducer | [inline, protected] |
| newLabel(const Expr &e) | CVCL::TheoremProducer | |
| newPf(const std::string &name) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) | CVCL::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const Proof &label, const Expr &frm, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const Proof &label, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const Proof &pf) | CVCL::TheoremProducer | |
| newReflTheorem(const Expr &e, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| one | CVCL::RefinedArithTheoremProducer | [private] |
| plus(const Expr &x, const Expr &y) | CVCL::RefinedArithTheoremProducer | |
| plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind) | CVCL::ArithTheoremProducer | [virtual] |
| rat(Rational r) | CVCL::RefinedArithTheoremProducer | [inline] |
| realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta) | CVCL::ArithTheoremProducer | [virtual] |
| realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha) | CVCL::ArithTheoremProducer | [virtual] |
| realType() | CVCL::ArithTheoremProducer | [inline] |
| RefinedArithTheoremProducer(VCL *vcl) | CVCL::RefinedArithTheoremProducer | [inline] |
| rightMinusLeft(const Expr &e) | CVCL::ArithTheoremProducer | [virtual] |
| simplifiedMultExpr(std::vector< Expr > &mulKids) | CVCL::ArithTheoremProducer | [virtual] |
| soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVCL::TheoremProducer | [protected] |
| splitGrayShadow(const Theorem &grayShadow) | CVCL::ArithTheoremProducer | [virtual] |
| subst(Op op, const Expr &x, const Theorem &t) | CVCL::RefinedArithTheoremProducer | |
| subst(Op op, const Theorem &t, const Expr &x) | CVCL::RefinedArithTheoremProducer | |
| subst(Op op, const Theorem &t1, const Theorem &t2) | CVCL::RefinedArithTheoremProducer | |
| symm(const Theorem &t) | CVCL::RefinedArithTheoremProducer | |
| TheoremProducer(TheoremManager *tm) | CVCL::TheoremProducer | |
| trans(const Theorem &t1, const Theorem &t2) | CVCL::RefinedArithTheoremProducer | |
| trans(const Expr &e) | CVCL::RefinedArithTheoremProducer | |
| uMinusToMult(const Expr &e) | CVCL::RefinedArithTheoremProducer | [virtual] |
| vcl | CVCL::RefinedArithTheoremProducer | [private] |
| withAssumptions() | CVCL::TheoremProducer | [inline] |
| withProof() | CVCL::TheoremProducer | [inline] |
| zero | CVCL::RefinedArithTheoremProducer | [private] |
| ~ArithProofRules() | CVCL::ArithProofRules | [inline, virtual] |
| ~TheoremProducer() | CVCL::TheoremProducer | [inline, virtual] |
