| CmdAssume |
An Assume command pushes some proposition onto the assumption stack of the session.
|
| CmdCheck |
A Check command takes a given proposition and asks the Session to prove it.
|
| CmdRaw |
A Raw command provides no additional structure, allowing arbitrary commands (as long as they have
no output) to be sent to the prover.
|
| CmdUndoAssume |
An UndoAssume command removes an assumption from the assumption stack of the given session.
|
| InvariantLemma |
InvariantLemmas are Lemmas created by printing a Daikon invariant in Simplify format, sometimes
with some hacks.
|
| Lemma |
A lemma is an object that wraps a Simplify formula representing some logical statement.
|
| LemmaStack |
A stack of Lemmas that shadows the stack of assumptions that Simplify keeps.
|
| Session |
A session is a channel to the Simplify theorem-proving tool.
|
| SessionManager |
A SessionManager is a component which handles the threading interaction with the Session.
|
| SimpUtil |
Utility functions for the simplify package.
|