Classes
- struct EdgeInfo
- class EpsRational
Public Member Functions
- void getEdgeTheorems (const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems)
- EpsRational getEdgeWeight (const Expr &x, const Expr &y)
- bool hasIncoming (const Expr &x)
- bool hasOutgoing (const Expr &x)
- void writeGraph (std::ostream &out)
- void getVariables (std::vector< Expr > &variables)
- void setRules (ArithProofRules *rules)
- void setArith (TheoryArithOld *arith)
- DifferenceLogicGraph (TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context)
- ~DifferenceLogicGraph ()
- Theorem getUnsatTheorem ()
- bool isUnsat ()
- void computeModel ()
- Rational getValuation (const Expr &x)
- void addEdge (const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm)
- bool existsEdge (const Expr &x, const Expr &y)
- bool inCycle (const Expr &x)
- void expandSharedTerm (const Expr &x)
Protected Types
Protected Member Functions
- Graph::ElementReference getEdge (const Expr &x, const Expr &y)
- bool tryUpdate (const Expr &x, const Expr &y, const Expr &z)
- void analyseConflict (const Expr &x, int kind)
Protected Attributes
- const int * d_pathLenghtThres
- TheoryArithOld * arith
- TheoryCore * core
- ArithProofRules * rules
- CDO< Theorem > unsat_theorem
- CDO< Rational > biggestEpsilon
- CDO< Rational > smallestPathDifference
- Graph leGraph
- EdgesList incomingEdges
- EdgesList outgoingEdges
- CDMap< Expr, bool > varInCycle
- Expr sourceVertex
Detailed Description
Definition at line 456 of file theory_arith_old.h.
Member Typedef Documentation
typedef CDMap<Expr, EdgeInfo> CVC3::TheoryArithOld::DifferenceLogicGraph::Graph [protected] |
The graph itself, maps expressions (x-y) to the edge information
Definition at line 771 of file theory_arith_old.h.
typedef ExprMap<CDList<Expr>*> CVC3::TheoryArithOld::DifferenceLogicGraph::EdgesList [protected] |
Definition at line 776 of file theory_arith_old.h.
Constructor & Destructor Documentation
| TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph | ( | TheoryArithOld * | arith, |
| TheoryCore * | core, | ||
| ArithProofRules * | rules, | ||
| Context * | context | ||
| ) |
Class constructor.
Definition at line 4711 of file theory_arith_old.cpp.
| TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph | ( | ) |
Destructor
Definition at line 5024 of file theory_arith_old.cpp.
References CVC3::ExprMap< Data >::begin().
Member Function Documentation
| void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems | ( | const Expr & | x, |
| const Expr & | y, | ||
| const EdgeInfo & | edgeInfo, | ||
| std::vector< Theorem > & | outputTheorems | ||
| ) |
Given two vertices in the graph and an path edge, reconstruct all the theorems and put them in the output vector
Definition at line 4888 of file theory_arith_old.cpp.
References DebugAssert, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::int2string(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryArithOld::tryPropagate().
| TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::getEdgeWeight | ( | const Expr & | x, |
| const Expr & | y | ||
| ) |
Returns the current weight of the edge.
Definition at line 4778 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length.
Referenced by CVC3::TheoryArithOld::computeTermBounds().
| bool TheoryArithOld::DifferenceLogicGraph::hasIncoming | ( | const Expr & | x | ) |
Returns whether a vertex has incoming edges.
Definition at line 5809 of file theory_arith_old.cpp.
References CVC3::CDList< T >::size().
Referenced by CVC3::TheoryArithOld::computeTermBounds(), and CVC3::TheoryArithOld::isUnconstrained().
| bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing | ( | const Expr & | x | ) |
Returns whether a vertex has outgoing edges.
Definition at line 5827 of file theory_arith_old.cpp.
References CVC3::CDList< T >::size().
Referenced by CVC3::TheoryArithOld::computeTermBounds(), and CVC3::TheoryArithOld::isUnconstrained().
| TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference TheoryArithOld::DifferenceLogicGraph::getEdge | ( | const Expr & | x, |
| const Expr & | y | ||
| ) | [protected] |
Returns the edge (path) info for the given kind
- Parameters:
-
x the starting vertex y the ending vertex
- Returns:
- the edge information
Definition at line 4748 of file theory_arith_old.cpp.
References CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), and CVC3::CDList< T >::push_back().
| bool TheoryArithOld::DifferenceLogicGraph::tryUpdate | ( | const Expr & | x, |
| const Expr & | y, | ||
| const Expr & | z | ||
| ) | [protected] |
Try to update the shortest path from x to z using y.
Definition at line 4927 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::getType(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::Expr::toString(), and TRACE.
| void TheoryArithOld::DifferenceLogicGraph::writeGraph | ( | std::ostream & | out | ) |
Definition at line 5872 of file theory_arith_old.cpp.
References std::endl(), CVC3::CDList< T >::size(), and CVC3::Expr::toString().
Referenced by CVC3::TheoryArithOld::computeTermBounds().
| void TheoryArithOld::DifferenceLogicGraph::getVariables | ( | std::vector< Expr > & | variables | ) |
Fills the vector with all the variables (vertices) in the graph
Definition at line 5842 of file theory_arith_old.cpp.
References CVC3::Expr::begin().
Referenced by CVC3::TheoryArithOld::computeTermBounds().
| void CVC3::TheoryArithOld::DifferenceLogicGraph::setRules | ( | ArithProofRules * | rules | ) | [inline] |
Definition at line 806 of file theory_arith_old.h.
References rules.
Referenced by CVC3::TheoryArithOld::TheoryArithOld().
| void CVC3::TheoryArithOld::DifferenceLogicGraph::setArith | ( | TheoryArithOld * | arith | ) | [inline] |
Definition at line 810 of file theory_arith_old.h.
References arith.
Referenced by CVC3::TheoryArithOld::TheoryArithOld().
| Theorem TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem | ( | ) |
Returns the reference to the unsat theorem if there is a negative cycle in the graph.
- Returns:
- the unsat theorem
Definition at line 4724 of file theory_arith_old.cpp.
| bool TheoryArithOld::DifferenceLogicGraph::isUnsat | ( | ) |
Returns true if there is a negative cycle in the graph.
Definition at line 4728 of file theory_arith_old.cpp.
| void TheoryArithOld::DifferenceLogicGraph::computeModel | ( | ) |
Definition at line 5111 of file theory_arith_old.cpp.
References CVC3::Expr::begin(), and CVC3::Theorem::getExpr().
Referenced by CVC3::TheoryArithOld::assignVariables().
Definition at line 5150 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryArithOld::assignVariables().
| void TheoryArithOld::DifferenceLogicGraph::addEdge | ( | const Expr & | x, |
| const Expr & | y, | ||
| const Rational & | c, | ||
| const Theorem & | edge_thm | ||
| ) |
Adds an edge corresponding to the constraint x - y <= c.
- Parameters:
-
x variable x::Difference y variable y c rational c edge_thm the theorem for this edge
Definition at line 4788 of file theory_arith_old.cpp.
References DebugAssert, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::LT, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::CDList< T >::push_back(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), and TRACE.
Check if there is an edge from x to y
Definition at line 4732 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined().
| bool TheoryArithOld::DifferenceLogicGraph::inCycle | ( | const Expr & | x | ) |
Check if x is in a cycle
Definition at line 4744 of file theory_arith_old.cpp.
Referenced by CVC3::TheoryArithOld::computeTermBounds().
| void TheoryArithOld::DifferenceLogicGraph::expandSharedTerm | ( | const Expr & | x | ) |
Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides).
Definition at line 5020 of file theory_arith_old.cpp.
| void TheoryArithOld::DifferenceLogicGraph::analyseConflict | ( | const Expr & | x, |
| int | kind | ||
| ) | [protected] |
Produced the unsat theorem from a cycle x --> x of negative length
- Parameters:
-
x the variable to use for the conflict kind the kind of edges to consider
Definition at line 4907 of file theory_arith_old.cpp.
References DebugAssert, CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::int2string(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), and TRACE.
Member Data Documentation
const int* CVC3::TheoryArithOld::DifferenceLogicGraph::d_pathLenghtThres [protected] |
Threshold on path length to process (ignore bigger than and set incomplete)
Definition at line 750 of file theory_arith_old.h.
The arithmetic that's using this graph
Definition at line 753 of file theory_arith_old.h.
Referenced by setArith().
The core theory
Definition at line 756 of file theory_arith_old.h.
The arithmetic that is using u us
Definition at line 759 of file theory_arith_old.h.
Referenced by setRules().
The unsat theorem if available
Definition at line 762 of file theory_arith_old.h.
The biggest epsilon from EpsRational we used in paths
Definition at line 765 of file theory_arith_old.h.
The smallest rational difference we used in path relaxation
Definition at line 768 of file theory_arith_old.h.
Graph of <= paths
Definition at line 774 of file theory_arith_old.h.
List of vertices adjacent backwards to a vertex
Definition at line 779 of file theory_arith_old.h.
List of vertices adjacent forward to a vertex
Definition at line 781 of file theory_arith_old.h.
CDMap<Expr, bool> CVC3::TheoryArithOld::DifferenceLogicGraph::varInCycle [protected] |
Whether the variable is in a cycle
Definition at line 871 of file theory_arith_old.h.
Definition at line 873 of file theory_arith_old.h.
The documentation for this class was generated from the following files:
