CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo Struct Reference

#include <theory_arith_old.h>

Collaboration diagram for CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo:

[legend]

List of all members.

Public Member Functions

• bool isDefined () const
• EdgeInfo ()

Public Attributes

• EpsRational length
• int path_length_in_edges
• Expr in_path_vertex
• Theorem explanation

---

Detailed Description

Definition at line 710 of file theory_arith_old.h.

---

Constructor & Destructor Documentation

CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::EdgeInfo

(

)

[inline]

Definition at line 723 of file theory_arith_old.h.

---

Member Function Documentation

bool CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined

(

)

const [inline]

Returnes if the edge is well define (i.e. not +infinity)

Definition at line 721 of file theory_arith_old.h.

References CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::existsEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

---

Member Data Documentation

EpsRational CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length

The length of this edge

Definition at line 712 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::TheoryArithOld::tryPropagate(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

int CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

Expr CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

Theorem CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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::TheoryArithOld::DifferenceLogicGraph::addEdge(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems().

---

The documentation for this struct was generated from the following file:

• theory_arith_old.h