CVC3
2.4.1
|
Structure to hold user assertions indexed by declaration order. More...
Public Member Functions | |
UserAssertion () | |
The proof of its TCC. More... | |
UserAssertion (const Theorem &thm, const Theorem &tcc, size_t idx) | |
Constructor. More... | |
const Theorem & | thm () const |
Fetching a Theorem. More... | |
const Theorem & | tcc () const |
Fetching a TCC. More... | |
operator Theorem () | |
Auto-conversion to Theorem. More... | |
Private Attributes | |
size_t | d_idx |
Theorem | d_thm |
Theorem | d_tcc |
The theorem of the assertion (a |- a) More... | |
Friends | |
bool | operator< (const UserAssertion &a1, const UserAssertion &a2) |
Comparison for use in std::map, to sort in declaration order. More... | |
Structure to hold user assertions indexed by declaration order.
|
inline |
|
inline |
Fetching a Theorem.
Definition at line 99 of file vcl.h.
Referenced by CVC3::VCL::getAssumptionsRec().
|
inline |
|
inline |
|
friend |
|
private |