CVC3  2.4.1
CVC3::TheoryArithOld Member List

This is the complete list of members for CVC3::TheoryArithOld, 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
addMultiplicativeSignSplit(const Theorem &case_split_thm)CVC3::TheoryArithOldvirtual
addPairToArithOrder(const Expr &smaller, const Expr &bigger)CVC3::TheoryArithOldvirtual
addSharedTerm(const Expr &e)CVC3::TheoryArithOldvirtual
addSplitter(const Expr &e, int priority=0)CVC3::Theory
addToBuffer(const Theorem &thm, bool priority=false)CVC3::TheoryArithOldprivate
alreadyProjectedCVC3::TheoryArithOldprivate
assertEqualities(const Theorem &e)CVC3::Theoryvirtual
assertFact(const Theorem &e)CVC3::TheoryArithOldvirtual
assertTypePred(const Expr &e, const Theorem &pred)CVC3::Theoryinlinevirtual
assignValue(const Expr &t, const Expr &val)CVC3::Theoryvirtual
assignValue(const Theorem &thm)CVC3::Theoryvirtual
assignVariables(std::vector< Expr > &v)CVC3::TheoryArithOldprivate
AtomsMap typedefCVC3::TheoryArithOldprivate
boolType()CVC3::Theoryinline
BoundsQueryType enum nameCVC3::TheoryArithOldprivate
bufferedInequalitiesCVC3::TheoryArithOldprivate
canon(const Expr &e)CVC3::TheoryArithOldprivatevirtual
canonConjunctionEquiv(const Theorem &thm)CVC3::TheoryArithOldprivate
canonPred(const Theorem &thm)CVC3::TheoryArithOldprivate
canonPredEquiv(const Theorem &thm)CVC3::TheoryArithOldprivate
canonRec(const Expr &e)CVC3::TheoryArithprotected
canonSimp(const Expr &e)CVC3::TheoryArithprotected
canonSimplify(const Expr &e)CVC3::TheoryArithOldprivate
canonSimplify(const Theorem &thm)CVC3::TheoryArithOldinlineprivate
canonThm(const Theorem &thm)CVC3::TheoryArithinline
canPickEqMonomial(const Expr &right)CVC3::TheoryArithOldprivate
checkAssertEqInvariant(const Theorem &e)CVC3::TheoryArithOldvirtual
checkIntegerEquality(const Theorem &thm)CVC3::TheoryArithOldprivate
checkSat(bool fullEffort)CVC3::TheoryArithOldvirtual
checkType(const Expr &e)CVC3::TheoryArithOldvirtual
collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)CVC3::TheoryArithOldprivate
computeBaseType(const Type &t)CVC3::TheoryArithOldvirtual
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::TheoryArithOldvirtual
computeModelBasic(const std::vector< Expr > &v)CVC3::TheoryArithOldvirtual
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::TheoryArithOldvirtual
computeNormalFactor(const Expr &rhs, bool normalizeConstants)CVC3::TheoryArithOldprivate
computeTCC(const Expr &e)CVC3::TheoryArithOldvirtual
computeTermBounds()CVC3::TheoryArithOldprivate
computeType(const Expr &e)CVC3::TheoryArithOldvirtual
computeTypePred(const Type &t, const Expr &e)CVC3::TheoryArithOldvirtual
createProofRulesOld()CVC3::TheoryArithOld
currentMaxCoefficient(Expr var)CVC3::TheoryArithOldprivate
d_buffer_0CVC3::TheoryArithOldprivate
d_buffer_1CVC3::TheoryArithOldprivate
d_buffer_2CVC3::TheoryArithOldprivate
d_buffer_3CVC3::TheoryArithOldprivate
d_bufferIdx_0CVC3::TheoryArithOldprivate
d_bufferIdx_1CVC3::TheoryArithOldprivate
d_bufferIdx_2CVC3::TheoryArithOldprivate
d_bufferIdx_3CVC3::TheoryArithOldprivate
d_bufferThresCVC3::TheoryArithOldprivate
d_countLeftCVC3::TheoryArithOldprivate
d_countRightCVC3::TheoryArithOldprivate
d_diseqCVC3::TheoryArithOldprivate
d_diseqIdxCVC3::TheoryArithOldprivate
d_freeConstDBCVC3::TheoryArithOldprivate
d_graphCVC3::TheoryArithOldprivate
d_grayShadowThresCVC3::TheoryArithOldprivate
d_inequalitiesLeftDBCVC3::TheoryArithOldprivate
d_inequalitiesRightDBCVC3::TheoryArithOldprivate
d_inModelCreationCVC3::TheoryArithOldprivate
d_intTypeCVC3::TheoryArithprotected
d_kindsCVC3::TheoryArithprotected
d_realTypeCVC3::TheoryArithprotected
d_rulesCVC3::TheoryArithOldprivate
d_sharedTermsCVC3::TheoryArithOldprivate
d_sharedTermsListCVC3::TheoryArithOldprivate
d_sharedVarsCVC3::TheoryArithOldprivate
d_splitSignCVC3::TheoryArithOldprivate
d_theoryUsedCVC3::Theoryprotected
d_varConstrainedMinusCVC3::TheoryArithOldprivate
d_varConstrainedPlusCVC3::TheoryArithOldprivate
darkShadow(const Expr &lhs, const Expr &rhs)CVC3::TheoryArithinline
diff_logic_sizeCVC3::TheoryArithOldprivate
diffLogicGraphCVC3::TheoryArithOldprivate
diffLogicOnlyCVC3::TheoryArithOldprivate
diseqSplitAlreadyCVC3::TheoryArithOldprivate
dontBufferCVC3::TheoryArithOldprivate
doSolve(const Theorem &e)CVC3::TheoryArithOldprivate
enqueueFact(const Theorem &e)CVC3::Theoryvirtual
enqueueSE(const Theorem &e)CVC3::Theoryvirtual
extractTermsFromInequality(const Expr &inequality, Rational &c1, Expr &t1, Rational &c2, Expr &t2)CVC3::TheoryArithOldprivate
falseExpr()CVC3::Theoryinline
find(const Expr &e)CVC3::Theory
findBounds(const Expr &e, Rational &lub, Rational &glb)CVC3::TheoryArithOldprivate
findExpr(const Expr &e)CVC3::Theoryinline
findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)CVC3::TheoryArithOldprivate
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::TheoryArithOldvirtual
fixCurrentMaxCoefficient(Expr variable, Rational max)CVC3::TheoryArithOldprivate
fixedMaxCoefficientCVC3::TheoryArithOldprivate
formulaAtomLowerBoundCVC3::TheoryArithOldprivate
formulaAtomsCVC3::TheoryArithOldprivate
formulaAtomUpperBoundCVC3::TheoryArithOldprivate
freeConstIneq(const Expr &ineq, bool varOnRHS)CVC3::TheoryArithOldprivate
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getCommonRules()CVC3::Theoryinline
getEM()CVC3::Theoryinline
getFactors(const Expr &e, std::set< Expr > &factors)CVC3::TheoryArithOldprivate
getLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::Theory
getName() const CVC3::Theoryinline
getNumTheories()CVC3::Theory
getTCC(const Expr &e)CVC3::Theory
getTypePred(const Type &t, const Expr &e)CVC3::Theory
getUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)CVC3::TheoryArithinline
hasLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldinlineprivate
hasTheory(int kind)CVC3::Theory
hasUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldinlineprivate
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theoryinline
inconsistent()CVC3::Theoryvirtual
inequalityToFind(const Theorem &inequalityThm, bool normalizeRHS)CVC3::TheoryArithOldprivate
installID(const std::string &name, const Expr &e)CVC3::Theory
intType()CVC3::TheoryArithinline
isAtomicArithFormula(const Expr &e)CVC3::TheoryArith
isAtomicArithTerm(const Expr &e)CVC3::TheoryArithprotected
isBounded(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
isConstrained(const Expr &t, bool intOnly=true, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
isConstrainedAbove(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
isConstrainedBelow(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)CVC3::TheoryArithOldprivate
isInteger(const Expr &e)CVC3::TheoryArithOldinline
isIntegerDerive(const Expr &isIntE, const Theorem &thm)CVC3::TheoryArithOldprivate
isIntegerThm(const Expr &e)CVC3::TheoryArithOldprivate
isLeaf(const Expr &e)CVC3::Theoryinline
isLeafIn(const Expr &e1, const Expr &e2)CVC3::Theory
isNonlinearEq(const Expr &e)CVC3::TheoryArithOld
isNonlinearSumTerm(const Expr &term)CVC3::TheoryArithOld
isolateVariable(const Theorem &inputThm, bool &e1)CVC3::TheoryArithOldprivate
isPowerEquality(const Expr &nonlinearEq, Rational &constant, Expr &power1)CVC3::TheoryArithOld
isPowersEquality(const Expr &nonlinearEq, Expr &power1, Expr &power2)CVC3::TheoryArithOld
isStale(const Expr &e)CVC3::TheoryArithOldprivate
isStale(const Ineq &ineq)CVC3::TheoryArithOldprivate
isSyntacticRational(const Expr &e, Rational &r)CVC3::TheoryArith
isUnconstrained(const Expr &t)CVC3::TheoryArithOld
kidsCanonical(const Expr &e)CVC3::TheoryArithOldprivate
leavesAreNumConst(const Expr &e)CVC3::TheoryArith
leavesAreSimp(const Expr &e)CVC3::Theory
lessThanVar(const Expr &isolatedVar, const Expr &var2)CVC3::TheoryArithOldprivate
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
maxCoefficientLeftCVC3::TheoryArithOldprivate
maxCoefficientRightCVC3::TheoryArithOldprivate
multiplicativeSignSplitsCVC3::TheoryArithOldprivate
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
nonlinearSignSplit() const CVC3::TheoryArithOldinline
normalize(const Expr &e)CVC3::TheoryArithOldprivate
normalize(const Theorem &thm)CVC3::TheoryArithOldprivate
normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)CVC3::TheoryArithOldprivate
notifyInconsistent(const Theorem &thm)CVC3::Theoryinlinevirtual
operator<<(std::ostream &os, const FreeConst &fc)CVC3::TheoryArithOldfriend
operator<<(std::ostream &os, const Ineq &ineq)CVC3::TheoryArithOldfriend
parseExpr(const Expr &e)CVC3::Theoryvirtual
parseExprOp(const Expr &e)CVC3::TheoryArithOldvirtual
pickIntEqMonomial(const Expr &right, Expr &isolated, bool &nonlin)CVC3::TheoryArithOldprivate
pickMonomial(const Expr &right)CVC3::TheoryArithOldprivate
print(ExprStream &os, const Expr &e)CVC3::TheoryArithOldvirtual
printRational(ExprStream &os, const Rational &r, bool printAsReal=false)CVC3::TheoryArithprotected
processBuffer()CVC3::TheoryArithOldprivate
processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)CVC3::TheoryArithOldprivate
processFiniteIntervals(const Expr &x)CVC3::TheoryArithOldprivate
processIntEq(const Theorem &eqn)CVC3::TheoryArithOldprivate
processRealEq(const Theorem &eqn)CVC3::TheoryArithOldprivate
processSimpleIntEq(const Theorem &eqn)CVC3::TheoryArithOldprivate
projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)CVC3::TheoryArithOldprivate
QueryWithCacheAll enum valueCVC3::TheoryArithOldprivate
QueryWithCacheLeaves enum valueCVC3::TheoryArithOldprivate
QueryWithCacheLeavesAndConstrainedComputation enum valueCVC3::TheoryArithOldprivate
rafineInequalityToInteger(const Theorem &thm)CVC3::TheoryArithOldprivate
rat(Rational r)CVC3::TheoryArithinline
realType()CVC3::TheoryArithinline
recursiveCanonSimpCheck(const Expr &e)CVC3::TheoryArithprotected
refineCounterExample()CVC3::TheoryArithOldvirtual
reflexivityRule(const Expr &a)CVC3::Theoryinline
registerAtom(const Expr &e)CVC3::TheoryArithOldprivatevirtual
CVC3::TheoryArith::registerAtom(const Expr &e, const Theorem &thm)CVC3::Theoryvirtual
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::TheoryArithOldvirtual
rewriteAnd(const Expr &e)CVC3::Theoryinline
rewriteAtomic(const Expr &e)CVC3::Theoryinlinevirtual
rewriteCC(const Expr &e)CVC3::Theory
rewriteIte(const Expr &e)CVC3::Theory
rewriteOr(const Expr &e)CVC3::Theoryinline
rewriteToDiff(const Expr &e)CVC3::TheoryArith
selectSmallestByCoefficient(const std::vector< Expr > &input, std::vector< Expr > &output)CVC3::TheoryArithOldprivate
separateMonomial(const Expr &e, Expr &c, Expr &var)CVC3::TheoryArithOldvirtual
setIncomplete(const std::string &reason)CVC3::Theoryvirtual
setInconsistent(const Theorem &e)CVC3::Theoryvirtual
setup(const Expr &e)CVC3::TheoryArithOldvirtual
setupCC(const Expr &e)CVC3::Theory
setupRec(const Expr &e)CVC3::TheoryArithOldprivate
setUsed()CVC3::Theoryinlinevirtual
shared_index_1CVC3::TheoryArithOldprivate
shared_index_2CVC3::TheoryArithOldprivate
simplify(const Expr &e)CVC3::Theoryvirtual
simplifyExpr(const Expr &e)CVC3::Theoryinline
simplifyOp(const Expr &e)CVC3::Theoryvirtual
solve(const Theorem &e)CVC3::TheoryArithOldvirtual
solvedForm(const std::vector< Theorem > &solvedEqs)CVC3::TheoryArithOldprivate
subrangeType(const Expr &l, const Expr &r)CVC3::TheoryArithinline
substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)CVC3::TheoryArithOldprivate
substAndCanonize(const Theorem &eq, ExprMap< Theorem > &subst)CVC3::TheoryArithOldprivate
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)CVC3::Theoryinline
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, int changed, const Theorem &thm)CVC3::Theoryinline
symmetryRule(const Theorem &a1_eq_a2)CVC3::Theoryinline
termConstrainedAboveCVC3::TheoryArithOldprivate
termConstrainedBelowCVC3::TheoryArithOldprivate
termDegree(const Expr &e)CVC3::TheoryArithOldprivate
termLowerBoundCVC3::TheoryArithOldprivate
termLowerBoundedCVC3::TheoryArithOldprivate
termLowerBoundThmCVC3::TheoryArithOldprivate
termUpperBoundCVC3::TheoryArithOldprivate
termUpperBoundedCVC3::TheoryArithOldprivate
termUpperBoundThmCVC3::TheoryArithOldprivate
Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
TheoryArith(TheoryCore *core, const std::string &name)CVC3::TheoryArithinline
TheoryArithOld(TheoryCore *core)CVC3::TheoryArithOld
theoryCore()CVC3::Theoryinline
theoryOf(int kind)CVC3::Theory
theoryOf(const Type &e)CVC3::Theory
theoryOf(const Expr &e)CVC3::Theory
theoryPreprocess(const Expr &e)CVC3::Theoryinlinevirtual
theoryUsed()CVC3::Theoryinlinevirtual
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theoryinline
trueExpr()CVC3::Theoryinline
tryPropagate(const Expr &x, const Expr &y, const DifferenceLogicGraph::EdgeInfo &x_y_edge, int kind)CVC3::TheoryArithOld
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
update(const Theorem &e, const Expr &d)CVC3::TheoryArithOldvirtual
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateConstrained(const Expr &t)CVC3::TheoryArithOld
updateHelper(const Expr &e)CVC3::Theory
updateStats(const Rational &c, const Expr &var)CVC3::TheoryArithOldprivate
updateStats(const Expr &monomial)CVC3::TheoryArithOldprivate
updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)CVC3::TheoryArithOldprivate
zeroCVC3::TheoryArithOldprivate
~Theory(void)CVC3::Theoryvirtual
~TheoryArith()CVC3::TheoryArithinline
~TheoryArithOld()CVC3::TheoryArithOld