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 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]

Fetching a Theorem.

Definition at line 92 of file vcl.h.

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

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

Fetching a TCC.

Definition at line 94 of file vcl.h.

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

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

Auto-conversion to Theorem.

Definition at line 96 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 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: