CVC3
|
#include <theory_arith_old.h>
Public Member Functions | |
bool | isDefined () const |
EdgeInfo () | |
Public Attributes | |
EpsRational | length |
int | path_length_in_edges |
Expr | in_path_vertex |
Theorem | explanation |
Definition at line 710 of file theory_arith_old.h.
|
inline |
Definition at line 723 of file theory_arith_old.h.
|
inline |
Returnes if the edge is well define (i.e. not +infinity)
Definition at line 721 of file theory_arith_old.h.
References path_length_in_edges.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), CVC3::TheoryArithOld::DifferenceLogicGraph::existsEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().
EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length |
The length of this edge
Definition at line 712 of file theory_arith_old.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(), CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::TheoryArithOld::tryPropagate(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().
int CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges |
The number of edges in this path
Definition at line 714 of file theory_arith_old.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), isDefined(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().
Expr CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex |
If this is a summary edge, a vertex in the path
Definition at line 716 of file theory_arith_old.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().
Theorem CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation |
If this is an original edge, the theorem that explains it
Definition at line 718 of file theory_arith_old.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), and CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems().