CVC3
Public Member Functions | Public Attributes | List of all members
CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo Struct Reference

#include <theory_arith_old.h>

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

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::DifferenceLogicGraph::EdgeInfo::EdgeInfo ( )
inline

Definition at line 723 of file theory_arith_old.h.

Member Function Documentation

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined ( ) const
inline

Member Data Documentation

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length
int CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges
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().


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