CVC3 2.4.1
Public Member Functions | Private Attributes | Friends
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 88 of file vcl.h.


Constructor & Destructor Documentation

CVC3::VCL::UserAssertion::UserAssertion ( ) [inline]

The proof of its TCC.

Default constructor

Definition at line 94 of file vcl.h.

CVC3::VCL::UserAssertion::UserAssertion ( const Theorem thm,
const Theorem tcc,
size_t  idx 
) [inline]

Constructor.

Definition at line 96 of file vcl.h.


Member Function Documentation

const Theorem& CVC3::VCL::UserAssertion::thm ( ) const [inline]

Fetching a Theorem.

Definition at line 99 of file vcl.h.

Referenced by CVC3::VCL::getAssumptionsRec().

const Theorem& CVC3::VCL::UserAssertion::tcc ( ) const [inline]

Fetching a TCC.

Definition at line 101 of file vcl.h.

Referenced by CVC3::VCL::getAssumptionsRec().

CVC3::VCL::UserAssertion::operator Theorem ( ) [inline]

Auto-conversion to Theorem.

Definition at line 103 of file vcl.h.


Friends And Related Function Documentation

bool operator< ( const UserAssertion a1,
const UserAssertion a2 
) [friend]

Comparison for use in std::map, to sort in declaration order.

Definition at line 105 of file vcl.h.


Member Data Documentation

Definition at line 89 of file vcl.h.

Definition at line 90 of file vcl.h.

The theorem of the assertion (a |- a)

Definition at line 91 of file vcl.h.


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