CVCL::TheoryArith Member List

This is the complete list of members for CVCL::TheoryArith, including all inherited members.

addBoundVar(const std::string &name, const Type &type)CVCL::Theory
addBoundVar(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
addSharedTerm(const Expr &e)CVCL::TheoryArith [virtual]
addSplitter(const Expr &e, int priority=0)CVCL::Theory
addToBuffer(const Theorem &thm)CVCL::TheoryArith [private]
assertEqualities(const Theorem &e)CVCL::Theory [virtual]
assertFact(const Theorem &e)CVCL::TheoryArith [virtual]
assertTypePred(const Expr &e, const Theorem &pred)CVCL::Theory [inline, virtual]
assignValue(const Expr &t, const Expr &val)CVCL::Theory [virtual]
assignValue(const Theorem &thm)CVCL::Theory [virtual]
assignVariables(std::vector< Expr > &v)CVCL::TheoryArith [private]
boolType()CVCL::Theory [inline]
canon(const Expr &e)CVCL::TheoryArith [private]
canon(const Theorem &thm)CVCL::TheoryArith [inline, private]
canonConjunctionEquiv(const Theorem &thm)CVCL::TheoryArith [private]
canonPred(const Theorem &thm)CVCL::TheoryArith [private]
canonPredEquiv(const Theorem &thm)CVCL::TheoryArith [private]
canonRec(const Expr &e)CVCL::TheoryArith [private]
canonSimplify(const Expr &e)CVCL::TheoryArith [private]
canonSimplify(const Theorem &thm)CVCL::TheoryArith [inline, private]
checkSat(bool fullEffort)CVCL::TheoryArith [virtual]
checkType(const Expr &e)CVCL::TheoryArith [virtual]
collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)CVCL::TheoryArith [private]
computeBaseType(const Type &t)CVCL::TheoryArith [virtual]
computeModel(const Expr &e, std::vector< Expr > &vars)CVCL::TheoryArith [virtual]
computeModelBasic(const std::vector< Expr > &v)CVCL::TheoryArith [virtual]
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVCL::TheoryArith [virtual]
computeNormalFactor(const Expr &rhs)CVCL::TheoryArith [private]
computeTCC(const Expr &e)CVCL::TheoryArith [virtual]
computeType(const Expr &e)CVCL::TheoryArith [virtual]
computeTypePred(const Type &t, const Expr &e)CVCL::TheoryArith [virtual]
createProofRules()CVCL::TheoryArith
d_bufferCVCL::TheoryArith [private]
d_bufferIdxCVCL::TheoryArith [private]
d_bufferThresCVCL::TheoryArith [private]
d_convertToDiffCVCL::TheoryArith [private]
d_countLeftCVCL::TheoryArith [private]
d_countRightCVCL::TheoryArith [private]
d_diseqCVCL::TheoryArith [private]
d_diseqIdxCVCL::TheoryArith [private]
d_freeConstDBCVCL::TheoryArith [private]
d_graphCVCL::TheoryArith [private]
d_inequalitiesLeftDBCVCL::TheoryArith [private]
d_inequalitiesRightDBCVCL::TheoryArith [private]
d_inModelCreationCVCL::TheoryArith [private]
d_intConstUsedCVCL::TheoryArith [private]
d_intTypeCVCL::TheoryArith [private]
d_intUsedCVCL::TheoryArith [private]
d_langUsedCVCL::TheoryArith [private]
d_realTypeCVCL::TheoryArith [private]
d_realUsedCVCL::TheoryArith [private]
d_rulesCVCL::TheoryArith [private]
d_sharedTermsCVCL::TheoryArith [private]
d_sharedVarsCVCL::TheoryArith [private]
d_theoryUsedCVCL::Theory [protected]
d_zeroVarCVCL::TheoryArith [private]
darkShadow(const Expr &lhs, const Expr &rhs)CVCL::TheoryArith [inline]
doSolve(const Theorem &e)CVCL::TheoryArith [private]
enqueueEquality(const Theorem &e)CVCL::Theory [virtual]
enqueueFact(const Theorem &e)CVCL::Theory [virtual]
falseExpr()CVCL::Theory [inline]
find(const Expr &e)CVCL::Theory
findBounds(const Expr &e, Rational &lub, Rational &glb)CVCL::TheoryArith [private]
findExpr(const Expr &e)CVCL::Theory [inline]
findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)CVCL::TheoryArith [private]
freeConstIneq(const Expr &ineq, bool varOnRHS)CVCL::TheoryArith [private]
getBaseType(const Expr &e)CVCL::Theory
getBaseType(const Type &tp)CVCL::Theory
getCommonRules()CVCL::Theory [inline]
getEM()CVCL::Theory [inline]
getLangUsed()CVCL::TheoryArith [inline]
getModelTerm(const Expr &e, std::vector< Expr > &v)CVCL::Theory
getModelValue(const Expr &e)CVCL::Theory
getName() const CVCL::Theory [inline]
getNumTheories()CVCL::Theory
getTCC(const Expr &e)CVCL::Theory
getTypePred(const Type &t, const Expr &e)CVCL::Theory
grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)CVCL::TheoryArith [inline]
hasTheory(int kind)CVCL::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVCL::Theory [inline]
inconsistent()CVCL::Theory [virtual]
installID(const std::string &name, const Expr &e)CVCL::Theory
intType()CVCL::TheoryArith [inline]
intUsed()CVCL::TheoryArith [inline]
isAtomicArithFormula(const Expr &e)CVCL::TheoryArith
isAtomicArithTerm(const Expr &e)CVCL::TheoryArith [private]
isInteger(const Expr &e)CVCL::TheoryArith [inline, private]
isIntegerDerive(const Expr &isIntE, const Theorem &thm)CVCL::TheoryArith [private]
isIntegerThm(const Expr &e)CVCL::TheoryArith [private]
isLeaf(const Expr &e)CVCL::Theory [inline]
isLeafIn(const Expr &e1, const Expr &e2)CVCL::Theory
isolateVariable(const Theorem &inputThm, bool &e1)CVCL::TheoryArith [private]
isStale(const Expr &e)CVCL::TheoryArith [private]
isStale(const Ineq &ineq)CVCL::TheoryArith [private]
isSyntacticRational(const Expr &e, Rational &r)CVCL::TheoryArith [private]
isSyntacticUMinusVar(const Expr &e, Expr &var)CVCL::TheoryArith [private]
kidsCanonical(const Expr &e)CVCL::TheoryArith [private]
leavesAreSimp(const Expr &e)CVCL::Theory
lessThanVar(const Expr &isolatedVar, const Expr &var2)CVCL::TheoryArith [private]
lookupVar(const std::string &name, Type *type)CVCL::Theory
newFunction(const std::string &name, const Type &type, bool computeTransClosure)CVCL::Theory
newFunction(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
newTypeExpr(const std::string &name)CVCL::Theory
newTypeExpr(const std::string &name, const Type &def)CVCL::Theory
newVar(const std::string &name, const Type &type)CVCL::Theory
newVar(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
normalize(const Expr &e)CVCL::TheoryArith [private]
normalize(const Theorem &thm)CVCL::TheoryArith [private]
normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)CVCL::TheoryArith [private]
notifyInconsistent(const Theorem &thm)CVCL::Theory [inline, virtual]
operator<<(std::ostream &os, const FreeConst &fc)CVCL::TheoryArith [friend]
operator<<(std::ostream &os, const Ineq &ineq)CVCL::TheoryArith [friend]
parseExpr(const Expr &e)CVCL::Theory [virtual]
parseExprOp(const Expr &e)CVCL::TheoryArith [virtual]
pickIntEqMonomial(const Expr &right)CVCL::TheoryArith [private]
pickMonomial(const Expr &right)CVCL::TheoryArith [private]
print(ExprStream &os, const Expr &e)CVCL::TheoryArith [virtual]
printLhs(ExprStream &os, const Expr &e)CVCL::TheoryArith [private]
printMinus(ExprStream &os, const Expr &parent, const Expr &e)CVCL::TheoryArith [private]
printPlus(ExprStream &os, const Expr &parent, const Expr &e)CVCL::TheoryArith [private]
printRational(ExprStream &os, const Expr &parent, const Expr &e, const Rational &r, bool checkLhs=true)CVCL::TheoryArith [private]
processBuffer()CVCL::TheoryArith [private]
processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)CVCL::TheoryArith [private]
processFiniteIntervals(const Expr &x)CVCL::TheoryArith [private]
processIntEq(const Theorem &eqn)CVCL::TheoryArith [private]
processRealEq(const Theorem &eqn)CVCL::TheoryArith [private]
processSimpleIntEq(const Theorem &eqn)CVCL::TheoryArith [private]
projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)CVCL::TheoryArith [private]
rat(Rational r)CVCL::TheoryArith [inline]
realType()CVCL::TheoryArith [inline]
realUsed()CVCL::TheoryArith [inline]
refineCounterExample()CVCL::TheoryArith [virtual]
reflexivityRule(const Expr &a)CVCL::Theory [inline]
registerKinds(Theory *theory, std::vector< int > &kinds)CVCL::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVCL::Theory
resolveID(const std::string &name)CVCL::Theory
rewrite(const Expr &e)CVCL::TheoryArith [virtual]
rewriteAnd(const Expr &e)CVCL::Theory [inline]
rewriteAtomic(const Expr &e)CVCL::Theory [inline, virtual]
rewriteCC(const Expr &e)CVCL::Theory
rewriteOr(const Expr &e)CVCL::Theory [inline]
rewriteToDiff(const Expr &e)CVCL::TheoryArith
separateMonomial(const Expr &e, Expr &c, Expr &var)CVCL::TheoryArith
setIncomplete(const std::string &reason)CVCL::Theory [virtual]
setInconsistent(const Theorem &e)CVCL::Theory [virtual]
setup(const Expr &e)CVCL::TheoryArith [virtual]
setupCC(const Expr &e)CVCL::Theory
setupRec(const Expr &e)CVCL::TheoryArith [private]
simplify(const Expr &e, bool forceRebuild=true)CVCL::Theory [virtual]
simplifyExpr(const Expr &e, bool forceRebuild=true)CVCL::Theory [inline]
simplifyOp(const Expr &e)CVCL::Theory [virtual]
simplifyRec(const Expr &e)CVCL::Theory [virtual]
solve(const Theorem &e)CVCL::TheoryArith [virtual]
solvedForm(const std::vector< Theorem > &solvedEqs)CVCL::TheoryArith [private]
subrangeType(const Expr &l, const Expr &r)CVCL::TheoryArith [inline]
substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)CVCL::TheoryArith [private]
substAndCanonize(const Theorem &eq, ExprMap< Theorem > &subst)CVCL::TheoryArith [private]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVCL::Theory [inline]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVCL::Theory [inline]
subtypePredicate(const Expr &e)CVCL::Theory
symmetryRule(const Theorem &a1_eq_a2)CVCL::Theory [inline]
Theory(TheoryCore *theoryCore, const std::string &name)CVCL::Theory
TheoryArith(VCL *vcl, TheoryCore *core)CVCL::TheoryArith
theoryCore()CVCL::Theory [inline]
theoryOf(int kind)CVCL::Theory
theoryOf(const Expr &e)CVCL::Theory
theoryUsed()CVCL::TheoryArith [inline, virtual]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVCL::Theory [inline]
trueExpr()CVCL::Theory [inline]
typePred(const Expr &e)CVCL::Theory
update(const Theorem &e, const Expr &d)CVCL::TheoryArith [virtual]
updateCC(const Theorem &e, const Expr &d)CVCL::Theory
updateHelper(const Expr &e)CVCL::Theory
updateStats(const Rational &c, const Expr &var)CVCL::TheoryArith [private]
updateStats(const Expr &monomial)CVCL::TheoryArith [private]
updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)CVCL::TheoryArith [private]
~Theory(void)CVCL::Theory [virtual]
~TheoryArith()CVCL::TheoryArith


Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by  doxygen 1.4.4