addEdge(const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
analyseConflict(const Expr &x, int kind) | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
arith | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
biggestEpsilon | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
computeModel() | CVC3::TheoryArithOld::DifferenceLogicGraph | |
core | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
d_pathLenghtThres | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
DifferenceLogicGraph(TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
EdgesList typedef | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
existsEdge(const Expr &x, const Expr &y) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
expandSharedTerm(const Expr &x) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
getEdge(const Expr &x, const Expr &y) | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
getEdgeTheorems(const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
getEdgeWeight(const Expr &x, const Expr &y) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
getUnsatTheorem() | CVC3::TheoryArithOld::DifferenceLogicGraph | |
getValuation(const Expr &x) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
getVariables(std::vector< Expr > &variables) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
Graph typedef | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
hasIncoming(const Expr &x) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
hasOutgoing(const Expr &x) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
incomingEdges | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
inCycle(const Expr &x) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
isUnsat() | CVC3::TheoryArithOld::DifferenceLogicGraph | |
leGraph | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
outgoingEdges | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
rules | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
setArith(TheoryArithOld *arith) | CVC3::TheoryArithOld::DifferenceLogicGraph | inline |
setRules(ArithProofRules *rules) | CVC3::TheoryArithOld::DifferenceLogicGraph | inline |
smallestPathDifference | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
sourceVertex | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
tryUpdate(const Expr &x, const Expr &y, const Expr &z) | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
unsat_theorem | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
varInCycle | CVC3::TheoryArithOld::DifferenceLogicGraph | protected |
writeGraph(std::ostream &out) | CVC3::TheoryArithOld::DifferenceLogicGraph | |
~DifferenceLogicGraph() | CVC3::TheoryArithOld::DifferenceLogicGraph | |