CVCL::VCL::UserAssertion Class Reference

Structure to hold user assertions indexed by declaration order. More...

Collaboration diagram for CVCL::VCL::UserAssertion:

[legend]List of all members.

Public Member Functions

• UserAssertion ()

  Default constructor.
  

• UserAssertion (const Theorem &thm, const Theorem &tcc, size_t idx)

  Constructor.
  

• const Theorem & thm () const

  Fetching a Theorem.
  

• const Theorem & tcc () const

  Fetching a TCC.
  

• operator Theorem ()

  Auto-conversion to Theorem.
  

Private Attributes

• size_t d_idx
• Theorem d_thm
• Theorem d_tcc

  The theorem of the assertion (a |- a).
  

Friends

• bool operator< (const UserAssertion &a1, const UserAssertion &a2)

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

---

Detailed Description

Structure to hold user assertions indexed by declaration order.

Definition at line 98 of file vcl.h.

---

Constructor & Destructor Documentation

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

Default constructor. Definition at line 104 of file vcl.h.

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

Constructor. Definition at line 106 of file vcl.h.

---

Member Function Documentation

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

Fetching a Theorem. Definition at line 109 of file vcl.h. References d_thm.

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

Fetching a TCC. Definition at line 111 of file vcl.h. References d_tcc.

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

Auto-conversion to Theorem. Definition at line 113 of file vcl.h. References d_thm.

---

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 115 of file vcl.h.

---

Member Data Documentation

size_t CVCL::VCL::UserAssertion::d_idx [private]

Definition at line 99 of file vcl.h.

Theorem CVCL::VCL::UserAssertion::d_thm [private]

Definition at line 100 of file vcl.h. Referenced by operator Theorem(), and thm().

Theorem CVCL::VCL::UserAssertion::d_tcc [private]

The theorem of the assertion (a |- a). Definition at line 101 of file vcl.h. Referenced by tcc().

---

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

• vcl.h

---