CVC3

CVC3::TheoryArithNew Member List

This is the complete list of members for CVC3::TheoryArithNew, including all inherited members.
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 [inline, virtual]
addPairToArithOrder(const Expr &smaller, const Expr &bigger)CVC3::TheoryArith [inline, virtual]
addSharedTerm(const Expr &e)CVC3::TheoryArithNew [virtual]
addSplitter(const Expr &e, int priority=0)CVC3::Theory
addToBuffer(const Theorem &thm)CVC3::TheoryArithNew [private]
allBoundsCVC3::TheoryArithNew [private]
assertedExprCVC3::TheoryArithNew [private]
assertedExprCountCVC3::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 [inline, virtual]
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]
betaCVC3::TheoryArithNew [private]
boolType()CVC3::Theory [inline]
BoundInfoSet typedefCVC3::TheoryArithNew [private]
boundsAsString()CVC3::TheoryArithNew [private]
canon(const Expr &e)CVC3::TheoryArithNew [private, virtual]
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 [inline, private]
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]
consistentCVC3::TheoryArithNew [private]
createProofRules()CVC3::TheoryArithNew
d_bufferCVC3::TheoryArithNew [private]
d_bufferIdxCVC3::TheoryArithNew [private]
d_bufferThresCVC3::TheoryArithNew [private]
d_countLeftCVC3::TheoryArithNew [private]
d_countRightCVC3::TheoryArithNew [private]
d_diseqCVC3::TheoryArithNew [private]
d_diseqIdxCVC3::TheoryArithNew [private]
d_freeConstDBCVC3::TheoryArithNew [private]
d_graphCVC3::TheoryArithNew [private]
d_inequalitiesLeftDBCVC3::TheoryArithNew [private]
d_inequalitiesRightDBCVC3::TheoryArithNew [private]
d_inModelCreationCVC3::TheoryArithNew [private]
d_intTypeCVC3::TheoryArith [protected]
d_kindsCVC3::TheoryArith [protected]
d_realTypeCVC3::TheoryArith [protected]
d_rulesCVC3::TheoryArithNew [private]
d_sharedTermsCVC3::TheoryArithNew [private]
d_sharedVarsCVC3::TheoryArithNew [private]
d_theoryUsedCVC3::Theory [protected]
darkShadow(const Expr &lhs, const Expr &rhs)CVC3::TheoryArith [inline]
DependenciesMap typedefCVC3::TheoryArithNew [private]
dependenciesMapCVC3::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]
explanationCVC3::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]
freshVariablesCVC3::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_lemmaCVC3::TheoryArithNew [private]
intType()CVC3::TheoryArith [inline]
intVariablesCVC3::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
lowerBoundCVC3::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 nameCVC3::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 valueCVC3::TheoryArithNew [private]
NORMALIZE_UNIT enum valueCVC3::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]
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]
propagateCVC3::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 [inline, virtual]
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 typedefCVC3::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 [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]
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]
tableauxCVC3::TheoryArithNew [private]
tableauxAsString() const CVC3::TheoryArithNew [private]
TebleauxMap typedefCVC3::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 [inline, virtual]
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
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]
unsatBasicVariablesCVC3::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]
upperBoundCVC3::TheoryArithNew [private]
~Theory(void)CVC3::Theory [virtual]
~TheoryArith()CVC3::TheoryArith [inline]
~TheoryArithNew()CVC3::TheoryArithNew
Generated on Thu Sep 1 2011 19:35:13 for CVC3 by  doxygen 1.7.3