| addBoundVar(const std::string &name, const Type &type) | CVC3::Theory | |
| addBoundVar(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
| addInequalities(const Theorem &le_1, const Theorem &le_2) | CVC3::TheoryArithNew | [private] |
| addInequalities(const Theorem &le_1, const Theorem &le_2) | CVC3::TheoryArithNew | [private] |
| addSharedTerm(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| addSharedTerm(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
| addToBuffer(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| addToBuffer(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| allBounds | CVC3::TheoryArithNew | [private] |
| assertedExpr | CVC3::TheoryArithNew | [private] |
| assertedExpr | CVC3::TheoryArithNew | [private] |
| assertedExprCount | CVC3::TheoryArithNew | [private] |
| assertedExprCount | CVC3::TheoryArithNew | [private] |
| assertEqual(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assertEqual(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assertEqualities(const Theorem &e) | CVC3::Theory | [virtual] |
| assertFact(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| assertFact(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| assertLower(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assertLower(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assertTypePred(const Expr &e, const Theorem &pred) | CVC3::Theory | [inline, virtual] |
| assertUpper(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assertUpper(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| assignValue(const Expr &t, const Expr &val) | CVC3::Theory | [virtual] |
| assignValue(const Theorem &thm) | CVC3::Theory | [virtual] |
| assignVariables(std::vector< Expr > &v) | CVC3::TheoryArithNew | [private] |
| assignVariables(std::vector< Expr > &v) | CVC3::TheoryArithNew | [private] |
| beta | CVC3::TheoryArithNew | [private] |
| beta | CVC3::TheoryArithNew | [private] |
| boolType() | CVC3::Theory | [inline] |
| BoundInfoSet typedef | CVC3::TheoryArithNew | [private] |
| BoundInfoSet typedef | CVC3::TheoryArithNew | [private] |
| boundsAsString() | CVC3::TheoryArithNew | [private] |
| boundsAsString() | CVC3::TheoryArithNew | [private] |
| canon(const Expr &e) | CVC3::TheoryArithNew | [private, virtual] |
| canon(const Expr &e) | CVC3::TheoryArithNew | [private, virtual] |
| canonConjunctionEquiv(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonConjunctionEquiv(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonPred(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonPred(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonPredEquiv(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonPredEquiv(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| canonRec(const Expr &e) | CVC3::TheoryArith | [protected] |
| canonSimp(const Expr &e) | CVC3::TheoryArith | [protected] |
| canonSimplify(const Expr &e) | CVC3::TheoryArithNew | [private] |
| canonSimplify(const Theorem &thm) | CVC3::TheoryArithNew | [inline, private] |
| canonSimplify(const Expr &e) | CVC3::TheoryArithNew | [private] |
| canonSimplify(const Theorem &thm) | CVC3::TheoryArithNew | [inline, private] |
| canonThm(const Theorem &thm) | CVC3::TheoryArith | [inline] |
| checkAssertEqInvariant(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| checkAssertEqInvariant(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| checkSat(bool fullEffort) | CVC3::TheoryArithNew | [virtual] |
| checkSat(bool fullEffort) | CVC3::TheoryArithNew | [virtual] |
| checkSatInteger() | CVC3::TheoryArithNew | [private] |
| checkSatInteger() | CVC3::TheoryArithNew | [private] |
| checkSatSimplex() | CVC3::TheoryArithNew | [private] |
| checkSatSimplex() | CVC3::TheoryArithNew | [private] |
| checkType(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| checkType(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache) | CVC3::TheoryArithNew | [private] |
| collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache) | CVC3::TheoryArithNew | [private] |
| computeBaseType(const Type &t) | CVC3::TheoryArithNew | [virtual] |
| computeBaseType(const Type &t) | CVC3::TheoryArithNew | [virtual] |
| computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryArithNew | [virtual] |
| computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryArithNew | [virtual] |
| computeModelBasic(const std::vector< Expr > &v) | CVC3::TheoryArithNew | [virtual] |
| computeModelBasic(const std::vector< Expr > &v) | CVC3::TheoryArithNew | [virtual] |
| computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::TheoryArithNew | [virtual] |
| computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::TheoryArithNew | [virtual] |
| computeNormalFactor(const Expr &rhs, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| computeNormalFactor(const Expr &rhs, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| computeTCC(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| computeTCC(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| computeType(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| computeType(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| computeTypePred(const Type &t, const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| computeTypePred(const Type &t, const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| consistent | CVC3::TheoryArithNew | [private] |
| consistent | CVC3::TheoryArithNew | [private] |
| createProofRules() | CVC3::TheoryArithNew | |
| createProofRules() | CVC3::TheoryArithNew | |
| d_buffer | CVC3::TheoryArithNew | [private] |
| d_buffer | CVC3::TheoryArithNew | [private] |
| d_bufferIdx | CVC3::TheoryArithNew | [private] |
| d_bufferIdx | CVC3::TheoryArithNew | [private] |
| d_bufferThres | CVC3::TheoryArithNew | [private] |
| d_bufferThres | CVC3::TheoryArithNew | [private] |
| d_countLeft | CVC3::TheoryArithNew | [private] |
| d_countLeft | CVC3::TheoryArithNew | [private] |
| d_countRight | CVC3::TheoryArithNew | [private] |
| d_countRight | CVC3::TheoryArithNew | [private] |
| d_diseq | CVC3::TheoryArithNew | [private] |
| d_diseq | CVC3::TheoryArithNew | [private] |
| d_diseqIdx | CVC3::TheoryArithNew | [private] |
| d_diseqIdx | CVC3::TheoryArithNew | [private] |
| d_freeConstDB | CVC3::TheoryArithNew | [private] |
| d_freeConstDB | CVC3::TheoryArithNew | [private] |
| d_graph | CVC3::TheoryArithNew | [private] |
| d_index1 | CVC3::TheoryArithNew | [private] |
| d_inequalitiesLeftDB | CVC3::TheoryArithNew | [private] |
| d_inequalitiesLeftDB | CVC3::TheoryArithNew | [private] |
| d_inequalitiesRightDB | CVC3::TheoryArithNew | [private] |
| d_inequalitiesRightDB | CVC3::TheoryArithNew | [private] |
| d_inModelCreation | CVC3::TheoryArithNew | [private] |
| d_inModelCreation | CVC3::TheoryArithNew | [private] |
| d_intType | CVC3::TheoryArith | [protected] |
| d_realType | CVC3::TheoryArith | [protected] |
| d_rules | CVC3::TheoryArithNew | [private] |
| d_rules | CVC3::TheoryArithNew | [private] |
| d_sharedTerms | CVC3::TheoryArithNew | [private] |
| d_sharedTerms | CVC3::TheoryArithNew | [private] |
| d_sharedTermsList | CVC3::TheoryArithNew | [private] |
| d_sharedVars | CVC3::TheoryArithNew | [private] |
| d_sharedVars | CVC3::TheoryArithNew | [private] |
| d_theoryUsed | CVC3::Theory | [protected] |
| darkShadow(const Expr &lhs, const Expr &rhs) | CVC3::TheoryArith | [inline] |
| DependenciesMap typedef | CVC3::TheoryArithNew | [private] |
| DependenciesMap typedef | CVC3::TheoryArithNew | [private] |
| dependenciesMap | CVC3::TheoryArithNew | [private] |
| deriveGomoryCut(const Expr &x_i) | CVC3::TheoryArithNew | [private] |
| deriveGomoryCut(const Expr &x_i) | CVC3::TheoryArithNew | [private] |
| doSolve(const Theorem &e) | CVC3::TheoryArithNew | [private] |
| doSolve(const Theorem &e) | CVC3::TheoryArithNew | [private] |
| enqueueFact(const Theorem &e) | CVC3::Theory | [virtual] |
| explanation | CVC3::TheoryArithNew | [private] |
| falseExpr() | CVC3::Theory | [inline] |
| find(const Expr &e) | CVC3::Theory | |
| findBounds(const Expr &e, Rational &lub, Rational &glb) | CVC3::TheoryArithNew | [private] |
| findBounds(const Expr &e, Rational &lub, Rational &glb) | CVC3::TheoryArithNew | [private] |
| findCoefficient(const Expr &var, const Expr &expr) | CVC3::TheoryArithNew | [private] |
| findCoefficient(const Expr &var, const Expr &expr) | CVC3::TheoryArithNew | [private] |
| findExpr(const Expr &e) | CVC3::Theory | [inline] |
| findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r) | CVC3::TheoryArithNew | [private] |
| findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r) | CVC3::TheoryArithNew | [private] |
| findReduced(const Expr &e) | CVC3::Theory | |
| findRef(const Expr &e) | CVC3::Theory | |
| freshVariables | CVC3::TheoryArithNew | [private] |
| getBaseType(const Expr &e) | CVC3::Theory | |
| getBaseType(const Type &tp) | CVC3::Theory | |
| getBeta(const Expr &x) | CVC3::TheoryArithNew | |
| getBeta(const Expr &x) | CVC3::TheoryArithNew | |
| getCommonRules() | CVC3::Theory | [inline] |
| getEM() | CVC3::Theory | [inline] |
| getLowerBound(const Expr &x) const | CVC3::TheoryArithNew | |
| getLowerBound(const Expr &x) const | CVC3::TheoryArithNew | |
| getLowerBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | [private] |
| getLowerBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | [private] |
| getLowerBoundThm(const Expr &x) const | CVC3::TheoryArithNew | |
| getLowerBoundThm(const Expr &x) const | CVC3::TheoryArithNew | |
| getModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::Theory | |
| getModelValue(const Expr &e) | CVC3::Theory | |
| getName() const | CVC3::Theory | [inline] |
| getNumTheories() | CVC3::Theory | |
| getTableauxEntry(const Expr &x_i, const Expr &x_j) | CVC3::TheoryArithNew | [private] |
| getTableauxEntry(const Expr &x_i, const Expr &x_j) | CVC3::TheoryArithNew | [private] |
| getTCC(const Expr &e) | CVC3::Theory | |
| getTypePred(const Type &t, const Expr &e) | CVC3::Theory | |
| getUpperBound(const Expr &x) const | CVC3::TheoryArithNew | |
| getUpperBound(const Expr &x) const | CVC3::TheoryArithNew | |
| getUpperBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | [private] |
| getUpperBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | [private] |
| getUpperBoundThm(const Expr &x) const | CVC3::TheoryArithNew | |
| getUpperBoundThm(const Expr &x) const | CVC3::TheoryArithNew | |
| getVariableIntroThm(const Expr &leftSide) | CVC3::TheoryArithNew | [private] |
| getVariableIntroThm(const Expr &leftSide) | CVC3::TheoryArithNew | [private] |
| grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2) | CVC3::TheoryArith | [inline] |
| hasTheory(int kind) | CVC3::Theory | |
| iffMP(const Theorem &e1, const Theorem &e1_iff_e2) | CVC3::Theory | [inline] |
| inconsistent() | CVC3::Theory | [virtual] |
| installID(const std::string &name, const Expr &e) | CVC3::Theory | |
| integer_lemma | CVC3::TheoryArithNew | [private] |
| integer_lemma | CVC3::TheoryArithNew | [private] |
| intType() | CVC3::TheoryArith | [inline] |
| intVariables | CVC3::TheoryArithNew | [private] |
| intVariables | CVC3::TheoryArithNew | [private] |
| isAtomicArithFormula(const Expr &e) | CVC3::TheoryArith | |
| isAtomicArithTerm(const Expr &e) | CVC3::TheoryArith | [protected] |
| isBasic(const Expr &x) const | CVC3::TheoryArithNew | [private] |
| isBasic(const Expr &x) const | CVC3::TheoryArithNew | [private] |
| isInteger(const Expr &e) | CVC3::TheoryArithNew | [inline, private] |
| isInteger(const Expr &e) | CVC3::TheoryArithNew | [inline, private] |
| isIntegerDerive(const Expr &isIntE, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| isIntegerDerive(const Expr &isIntE, const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| isIntegerThm(const Expr &e) | CVC3::TheoryArithNew | [private] |
| isIntegerThm(const Expr &e) | CVC3::TheoryArithNew | [private] |
| isLeaf(const Expr &e) | CVC3::Theory | [inline] |
| isLeafIn(const Expr &e1, const Expr &e2) | CVC3::Theory | |
| isolateVariable(const Theorem &inputThm, bool &e1) | CVC3::TheoryArithNew | [private] |
| isolateVariable(const Theorem &inputThm, bool &e1) | CVC3::TheoryArithNew | [private] |
| isStale(const Expr &e) | CVC3::TheoryArithNew | [private] |
| isStale(const Ineq &ineq) | CVC3::TheoryArithNew | [private] |
| isStale(const Expr &e) | CVC3::TheoryArithNew | [private] |
| isStale(const Ineq &ineq) | CVC3::TheoryArithNew | [private] |
| isSyntacticRational(const Expr &e, Rational &r) | CVC3::TheoryArith | |
| kidsCanonical(const Expr &e) | CVC3::TheoryArithNew | [private] |
| kidsCanonical(const Expr &e) | CVC3::TheoryArithNew | [private] |
| leavesAreSimp(const Expr &e) | CVC3::Theory | |
| lessThanVar(const Expr &isolatedVar, const Expr &var2) | CVC3::TheoryArithNew | [private] |
| lessThanVar(const Expr &isolatedVar, const Expr &var2) | CVC3::TheoryArithNew | [private] |
| lookupVar(const std::string &name, Type *type) | CVC3::Theory | |
| lowerBound | CVC3::TheoryArithNew | [private] |
| lowerBound | CVC3::TheoryArithNew | [private] |
| newFunction(const std::string &name, const Type &type, bool computeTransClosure) | CVC3::Theory | |
| newFunction(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
| newSubtypeExpr(const Expr &pred, const Expr &witness) | CVC3::Theory | |
| newTypeExpr(const std::string &name) | CVC3::Theory | |
| newTypeExpr(const std::string &name, const Type &def) | CVC3::Theory | |
| newVar(const std::string &name, const Type &type) | CVC3::Theory | |
| newVar(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
| NormalizationType enum name | CVC3::TheoryArithNew | [private] |
| NormalizationType enum name | CVC3::TheoryArithNew | [private] |
| normalize(const Expr &e, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| normalize(const Theorem &thm, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| normalize(const Expr &e, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| normalize(const Theorem &thm, NormalizationType type=NORMALIZE_GCD) | CVC3::TheoryArithNew | [private] |
| NORMALIZE_GCD enum value | CVC3::TheoryArithNew | [private] |
| NORMALIZE_UNIT enum value | CVC3::TheoryArithNew | [private] |
| normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2) | CVC3::TheoryArithNew | [private] |
| normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2) | CVC3::TheoryArithNew | [private] |
| notifyInconsistent(const Theorem &thm) | CVC3::Theory | [inline, virtual] |
| operator<<(std::ostream &os, const FreeConst &fc) | CVC3::TheoryArithNew | [friend] |
| operator<<(std::ostream &os, const Ineq &ineq) | CVC3::TheoryArithNew | [friend] |
| operator<<(std::ostream &os, const FreeConst &fc) | CVC3::TheoryArithNew | [friend] |
| operator<<(std::ostream &os, const Ineq &ineq) | CVC3::TheoryArithNew | [friend] |
| parseExpr(const Expr &e) | CVC3::Theory | [virtual] |
| parseExprOp(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| parseExprOp(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| pickIntEqMonomial(const Expr &right) | CVC3::TheoryArithNew | [private] |
| pickIntEqMonomial(const Expr &right) | CVC3::TheoryArithNew | [private] |
| pickMonomial(const Expr &right) | CVC3::TheoryArithNew | [private] |
| pickMonomial(const Expr &right) | CVC3::TheoryArithNew | [private] |
| pivot(const Expr &x_r, const Expr &x_s) | CVC3::TheoryArithNew | [private] |
| pivot(const Expr &x_r, const Expr &x_s) | CVC3::TheoryArithNew | [private] |
| pivotAndUpdate(const Expr &x_i, const Expr &x_j, const EpsRational &v) | CVC3::TheoryArithNew | [private] |
| pivotAndUpdate(const Expr &x_i, const Expr &x_j, const EpsRational &v) | CVC3::TheoryArithNew | [private] |
| pivotRule(const Theorem &eq, const Expr &var) | CVC3::TheoryArithNew | [private] |
| pivotRule(const Theorem &eq, const Expr &var) | CVC3::TheoryArithNew | [private] |
| print(ExprStream &os, const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| print(ExprStream &os, const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| printRational(ExprStream &os, const Rational &r, bool printAsReal=false) | CVC3::TheoryArith | [protected] |
| processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta) | CVC3::TheoryArithNew | [private] |
| processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta) | CVC3::TheoryArithNew | [private] |
| processFiniteIntervals(const Expr &x) | CVC3::TheoryArithNew | [private] |
| processFiniteIntervals(const Expr &x) | CVC3::TheoryArithNew | [private] |
| processIntEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| processIntEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| processRealEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| processRealEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| processSimpleIntEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| processSimpleIntEq(const Theorem &eqn) | CVC3::TheoryArithNew | [private] |
| projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS) | CVC3::TheoryArithNew | [private] |
| projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS) | CVC3::TheoryArithNew | [private] |
| propagate | CVC3::TheoryArithNew | [private] |
| propagateTheory(const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound) | CVC3::TheoryArithNew | [private] |
| propagateTheory(const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound) | CVC3::TheoryArithNew | [private] |
| rafineIntegerConstraints(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| rafineIntegerConstraints(const Theorem &thm) | CVC3::TheoryArithNew | [private] |
| rat(Rational r) | CVC3::TheoryArith | [inline] |
| realType() | CVC3::TheoryArith | [inline] |
| recursiveCanonSimpCheck(const Expr &e) | CVC3::TheoryArith | [protected] |
| refineCounterExample() | CVC3::TheoryArithNew | [virtual] |
| refineCounterExample() | CVC3::TheoryArithNew | [virtual] |
| reflexivityRule(const Expr &a) | CVC3::Theory | [inline] |
| registerAtom(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| registerAtom(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| registerKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
| registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false) | CVC3::Theory | |
| resolveID(const std::string &name) | CVC3::Theory | |
| rewrite(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| rewrite(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| rewriteAnd(const Expr &e) | CVC3::Theory | [inline] |
| rewriteAtomic(const Expr &e) | CVC3::Theory | [inline, virtual] |
| rewriteCC(const Expr &e) | CVC3::Theory | |
| rewriteOr(const Expr &e) | CVC3::Theory | [inline] |
| rewriteToDiff(const Expr &e) | CVC3::TheoryArith | |
| separateMonomial(const Expr &e, Expr &c, Expr &var) | CVC3::TheoryArithNew | [virtual] |
| separateMonomial(const Expr &e, Expr &c, Expr &var) | CVC3::TheoryArithNew | [virtual] |
| setIncomplete(const std::string &reason) | CVC3::Theory | [virtual] |
| setInconsistent(const Theorem &e) | CVC3::Theory | [virtual] |
| SetOfVariables typedef | CVC3::TheoryArithNew | [private] |
| SetOfVariables typedef | CVC3::TheoryArithNew | [private] |
| setup(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| setup(const Expr &e) | CVC3::TheoryArithNew | [virtual] |
| setupCC(const Expr &e) | CVC3::Theory | |
| setupRec(const Expr &e) | CVC3::TheoryArithNew | [private] |
| setupRec(const Expr &e) | CVC3::TheoryArithNew | [private] |
| setUsed() | CVC3::Theory | [inline, virtual] |
| simplify(const Expr &e) | CVC3::Theory | [virtual] |
| simplifyExpr(const Expr &e) | CVC3::Theory | [inline] |
| simplifyOp(const Expr &e) | CVC3::Theory | [virtual] |
| solve(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| solve(const Theorem &e) | CVC3::TheoryArithNew | [virtual] |
| solvedForm(const std::vector< Theorem > &solvedEqs) | CVC3::TheoryArithNew | [private] |
| solvedForm(const std::vector< Theorem > &solvedEqs) | CVC3::TheoryArithNew | [private] |
| subrangeType(const Expr &l, const Expr &r) | CVC3::TheoryArith | [inline] |
| substAndCanonize(const Expr &t, ExprMap< Theorem > &subst) | CVC3::TheoryArithNew | [private] |
| substAndCanonize(const Theorem &eq, ExprMap< Theorem > &subst) | CVC3::TheoryArithNew | [private] |
| substAndCanonize(const Expr &t, ExprMap< Theorem > &subst) | CVC3::TheoryArithNew | [private] |
| substAndCanonize(const Theorem &eq, ExprMap< Theorem > &subst) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeModTableaux(const Theorem &eq) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeModTableaux(const Expr &sum) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeModTableaux(const Theorem &eq) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeModTableaux(const Expr &sum) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeTableaux(const Theorem &eq) | CVC3::TheoryArithNew | [private] |
| substAndCanonizeTableaux(const Theorem &eq) | CVC3::TheoryArithNew | [private] |
| substitutivityRule(const Op &op, const std::vector< Theorem > &thms) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, int changed, const Theorem &thm) | CVC3::Theory | [inline] |
| symmetryRule(const Theorem &a1_eq_a2) | CVC3::Theory | [inline] |
| tableaux | CVC3::TheoryArithNew | [private] |
| tableauxAsString() const | CVC3::TheoryArithNew | [private] |
| tableauxAsString() const | CVC3::TheoryArithNew | [private] |
| TebleauxMap typedef | CVC3::TheoryArithNew | [private] |
| TebleauxMap typedef | CVC3::TheoryArithNew | [private] |
| Theory(TheoryCore *theoryCore, const std::string &name) | CVC3::Theory | |
| TheoryArith(TheoryCore *core, const std::string &name) | CVC3::TheoryArith | [inline] |
| TheoryArithNew(TheoryCore *core) | CVC3::TheoryArithNew | |
| TheoryArithNew(TheoryCore *core) | CVC3::TheoryArithNew | |
| theoryCore() | CVC3::Theory | [inline] |
| theoryOf(int kind) | CVC3::Theory | |
| theoryOf(const Expr &e) | CVC3::Theory | |
| theoryUsed() | CVC3::Theory | [inline, virtual] |
| transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVC3::Theory | [inline] |
| trueExpr() | CVC3::Theory | [inline] |
| typePred(const Expr &e) | CVC3::Theory | |
| unsatAsString() const | CVC3::TheoryArithNew | [private] |
| unsatAsString() const | CVC3::TheoryArithNew | [private] |
| unsatBasicVariables | CVC3::TheoryArithNew | [private] |
| unsatBasicVariables | CVC3::TheoryArithNew | [private] |
| update(const Theorem &e, const Expr &d) | CVC3::TheoryArithNew | [virtual] |
| update(const Expr &x_i, const EpsRational &v) | CVC3::TheoryArithNew | [private] |
| update(const Theorem &e, const Expr &d) | CVC3::TheoryArithNew | [virtual] |
| update(const Expr &x_i, const EpsRational &v) | CVC3::TheoryArithNew | [private] |
| updateCC(const Theorem &e, const Expr &d) | CVC3::Theory | |
| updateDependencies(const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar) | CVC3::TheoryArithNew | [private] |
| updateDependencies(const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar) | CVC3::TheoryArithNew | [private] |
| updateDependenciesAdd(const Expr &var, const Expr &sum) | CVC3::TheoryArithNew | [private] |
| updateDependenciesAdd(const Expr &var, const Expr &sum) | CVC3::TheoryArithNew | [private] |
| updateDependenciesRemove(const Expr &var, const Expr &sum) | CVC3::TheoryArithNew | [private] |
| updateDependenciesRemove(const Expr &var, const Expr &sum) | CVC3::TheoryArithNew | [private] |
| updateFreshVariables() | CVC3::TheoryArithNew | [private] |
| updateFreshVariables() | CVC3::TheoryArithNew | [private] |
| updateHelper(const Expr &e) | CVC3::Theory | |
| updateStats(const Rational &c, const Expr &var) | CVC3::TheoryArithNew | [private] |
| updateStats(const Expr &monomial) | CVC3::TheoryArithNew | [private] |
| updateStats(const Rational &c, const Expr &var) | CVC3::TheoryArithNew | [private] |
| updateStats(const Expr &monomial) | CVC3::TheoryArithNew | [private] |
| updateValue(const Expr &var, const Expr &e) | CVC3::TheoryArithNew | [private] |
| updateValue(const Expr &var, const Expr &e) | CVC3::TheoryArithNew | [private] |
| upperBound | CVC3::TheoryArithNew | [private] |
| upperBound | CVC3::TheoryArithNew | [private] |
| ~Theory(void) | CVC3::Theory | [virtual] |
| ~TheoryArith() | CVC3::TheoryArith | [inline] |
| ~TheoryArithNew() | CVC3::TheoryArithNew | |
| ~TheoryArithNew() | CVC3::TheoryArithNew | |
