CVC3::VCL::UserAssertion Class Reference
Structure to hold user assertions indexed by declaration order.
More...
List of all members.
Public Member Functions
Private Attributes
Friends
Detailed Description
Structure to hold user assertions indexed by declaration order.
Definition at line 81 of file vcl.h.
Constructor & Destructor Documentation
CVC3::VCL::UserAssertion::UserAssertion |
( |
|
) |
[inline] |
The proof of its TCC.
Default constructor
Definition at line 87 of file vcl.h.
CVC3::VCL::UserAssertion::UserAssertion |
( |
const Theorem & |
thm, |
|
|
const Theorem & |
tcc, |
|
|
size_t |
idx | |
|
) |
| | [inline] |
Constructor.
Definition at line 89 of file vcl.h.
Member Function Documentation
const Theorem& CVC3::VCL::UserAssertion::thm |
( |
|
) |
const [inline] |
const Theorem& CVC3::VCL::UserAssertion::tcc |
( |
|
) |
const [inline] |
CVC3::VCL::UserAssertion::operator Theorem |
( |
|
) |
[inline] |
Friends And Related Function Documentation
Comparison for use in std::map, to sort in declaration order.
Definition at line 98 of file vcl.h.
Member Data Documentation
Definition at line 82 of file vcl.h.
Definition at line 83 of file vcl.h.
The theorem of the assertion (a |- a).
Definition at line 84 of file vcl.h.
The documentation for this class was generated from the following file: