addBoundVar(const std::string &name, const Type &type) | CVC3::Theory | |
addBoundVar(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
addGlobalLemma(const Theorem &thm, int priority=0) | CVC3::Theory | |
addInequalities(const Theorem &le_1, const Theorem &le_2) | CVC3::TheoryArithNew | private |
addMultiplicativeSignSplit(const Theorem &case_split_thm) | CVC3::TheoryArith | inlinevirtual |
addPairToArithOrder(const Expr &smaller, const Expr &bigger) | CVC3::TheoryArith | inlinevirtual |
addSharedTerm(const Expr &e) | CVC3::TheoryArithNew | virtual |
addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
addToBuffer(const Theorem &thm) | CVC3::TheoryArithNew | private |
allBounds | CVC3::TheoryArithNew | private |
assertedExpr | CVC3::TheoryArithNew | private |
assertedExprCount | 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 |
assertLower(const Expr &x_i, const EpsRational &c, const Theorem &thm) | CVC3::TheoryArithNew | private |
assertTypePred(const Expr &e, const Theorem &pred) | CVC3::Theory | inlinevirtual |
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 |
beta | CVC3::TheoryArithNew | private |
boolType() | CVC3::Theory | inline |
BoundInfoSet typedef | CVC3::TheoryArithNew | private |
boundsAsString() | CVC3::TheoryArithNew | private |
canon(const Expr &e) | CVC3::TheoryArithNew | privatevirtual |
canonConjunctionEquiv(const Theorem &thm) | CVC3::TheoryArithNew | private |
canonPred(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 | inlineprivate |
canonThm(const Theorem &thm) | CVC3::TheoryArith | inline |
checkAssertEqInvariant(const Theorem &e) | CVC3::TheoryArithNew | virtual |
checkSat(bool fullEffort) | CVC3::TheoryArithNew | virtual |
checkSatInteger() | CVC3::TheoryArithNew | private |
checkSatSimplex() | CVC3::TheoryArithNew | private |
checkType(const Expr &e) | CVC3::TheoryArithNew | virtual |
collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache) | CVC3::TheoryArithNew | private |
computeBaseType(const Type &t) | CVC3::TheoryArithNew | virtual |
computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryArithNew | virtual |
computeModelBasic(const 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 |
computeTCC(const Expr &e) | CVC3::TheoryArithNew | virtual |
computeType(const Expr &e) | CVC3::TheoryArithNew | virtual |
computeTypePred(const Type &t, const Expr &e) | CVC3::TheoryArithNew | virtual |
consistent | CVC3::TheoryArithNew | private |
createProofRules() | CVC3::TheoryArithNew | |
d_buffer | CVC3::TheoryArithNew | private |
d_bufferIdx | CVC3::TheoryArithNew | private |
d_bufferThres | CVC3::TheoryArithNew | private |
d_countLeft | CVC3::TheoryArithNew | private |
d_countRight | CVC3::TheoryArithNew | private |
d_diseq | CVC3::TheoryArithNew | private |
d_diseqIdx | CVC3::TheoryArithNew | private |
d_freeConstDB | CVC3::TheoryArithNew | private |
d_graph | CVC3::TheoryArithNew | private |
d_inequalitiesLeftDB | CVC3::TheoryArithNew | private |
d_inequalitiesRightDB | CVC3::TheoryArithNew | private |
d_inModelCreation | CVC3::TheoryArithNew | private |
d_intType | CVC3::TheoryArith | protected |
d_kinds | CVC3::TheoryArith | protected |
d_realType | CVC3::TheoryArith | protected |
d_rules | CVC3::TheoryArithNew | private |
d_sharedTerms | 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 | CVC3::TheoryArithNew | private |
deriveGomoryCut(const Expr &x_i) | CVC3::TheoryArithNew | private |
doSolve(const Theorem &e) | CVC3::TheoryArithNew | private |
enqueueFact(const Theorem &e) | CVC3::Theory | virtual |
enqueueSE(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 |
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 |
findReduce(const Expr &e) | CVC3::Theory | |
findReduced(const Expr &e) | CVC3::Theory | |
findRef(const Expr &e) | CVC3::Theory | |
finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize) | CVC3::TheoryArithNew | virtual |
freshVariables | CVC3::TheoryArithNew | private |
getBaseType(const Expr &e) | CVC3::Theory | |
getBaseType(const Type &tp) | CVC3::Theory | |
getBeta(const Expr &x) | CVC3::TheoryArithNew | |
getCommonRules() | CVC3::Theory | inline |
getEM() | CVC3::Theory | inline |
getLowerBound(const Expr &x) const | CVC3::TheoryArithNew | |
getLowerBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | private |
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 |
getTCC(const Expr &e) | CVC3::Theory | |
getTypePred(const Type &t, const Expr &e) | CVC3::Theory | |
getUpperBound(const Expr &x) const | CVC3::TheoryArithNew | |
getUpperBoundExplanation(const TebleauxMap::iterator &var_it) | CVC3::TheoryArithNew | private |
getUpperBoundThm(const Expr &x) const | CVC3::TheoryArithNew | |
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 |
intType() | CVC3::TheoryArith | inline |
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 |
isInteger(const Expr &e) | CVC3::TheoryArithNew | inline |
isIntegerDerive(const Expr &isIntE, const Theorem &thm) | 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 |
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 |
leavesAreNumConst(const Expr &e) | CVC3::TheoryArith | |
leavesAreSimp(const Expr &e) | CVC3::Theory | |
lessThanVar(const Expr &isolatedVar, const Expr &var2) | CVC3::TheoryArithNew | private |
lookupFunction(const std::string &name, Type *type) | CVC3::Theory | |
lookupTypeExpr(const std::string &name) | CVC3::Theory | |
lookupVar(const std::string &name, Type *type) | CVC3::Theory | |
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 |
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 |
notifyInconsistent(const Theorem &thm) | CVC3::Theory | inlinevirtual |
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 |
pickIntEqMonomial(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 |
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 |
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 |
processFiniteIntervals(const Expr &x) | CVC3::TheoryArithNew | private |
processIntEq(const Theorem &eqn) | CVC3::TheoryArithNew | private |
processRealEq(const Theorem &eqn) | CVC3::TheoryArithNew | private |
processSimpleIntEq(const Theorem &eqn) | 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 |
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 |
reflexivityRule(const Expr &a) | CVC3::Theory | inline |
registerAtom(const Expr &e) | CVC3::TheoryArithNew | virtual |
CVC3::TheoryArith::registerAtom(const Expr &e, const Theorem &thm) | CVC3::Theory | virtual |
registerKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false) | CVC3::Theory | |
renameExpr(const Expr &e) | CVC3::Theory | |
resolveID(const std::string &name) | CVC3::Theory | |
rewrite(const Expr &e) | CVC3::TheoryArithNew | virtual |
rewriteAnd(const Expr &e) | CVC3::Theory | inline |
rewriteAtomic(const Expr &e) | CVC3::Theory | inlinevirtual |
rewriteCC(const Expr &e) | CVC3::Theory | |
rewriteIte(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 |
setIncomplete(const std::string &reason) | CVC3::Theory | virtual |
setInconsistent(const Theorem &e) | CVC3::Theory | virtual |
SetOfVariables typedef | CVC3::TheoryArithNew | private |
setup(const Expr &e) | CVC3::TheoryArithNew | virtual |
setupCC(const Expr &e) | CVC3::Theory | |
setupRec(const Expr &e) | CVC3::TheoryArithNew | private |
setUsed() | CVC3::Theory | inlinevirtual |
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 |
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 |
substAndCanonizeModTableaux(const Theorem &eq) | CVC3::TheoryArithNew | private |
substAndCanonizeModTableaux(const Expr &sum) | 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 &t) | 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 |
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 | |
theoryCore() | CVC3::Theory | inline |
theoryOf(int kind) | CVC3::Theory | |
theoryOf(const Type &e) | CVC3::Theory | |
theoryOf(const Expr &e) | CVC3::Theory | |
theoryPreprocess(const Expr &e) | CVC3::Theory | inlinevirtual |
theoryUsed() | CVC3::Theory | inlinevirtual |
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVC3::Theory | inline |
trueExpr() | CVC3::Theory | inline |
typePred(const Expr &e) | CVC3::Theory | |
unregisterKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver) | CVC3::Theory | |
unsatAsString() const | 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 |
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 |
updateDependenciesAdd(const Expr &var, const Expr &sum) | CVC3::TheoryArithNew | private |
updateDependenciesRemove(const Expr &var, const Expr &sum) | 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 |
updateValue(const Expr &var, const Expr &e) | CVC3::TheoryArithNew | private |
upperBound | CVC3::TheoryArithNew | private |
~Theory(void) | CVC3::Theory | virtual |
~TheoryArith() | CVC3::TheoryArith | inline |
~TheoryArithNew() | CVC3::TheoryArithNew | |