Package escjava.prover

Class Summary

Atom	Atoms are S-expressions representing symbols.
CECEnum	This class is used privately by Simplify to enumerate the list of counter-example contexts found by Simplify to a given verification condition.
Cvc3
Formula
Harvey
HarveyResponse
NewProver
PPOutputStream	This class is a FilterOutputStream class designed for LISP-like input; it pretty prints the output by inserting spaces and newlines into the stream.
ProverResponse
Sammy
SammyResponse
SExp	S-Expression datatype for use in interfacing to the ESC Theorem prover, Simplify.
Signature
Simplify	The interface to the Simplify theorem prover program using Strings to send and S-expressions to receive.
SimplifyComment	An object of this class represent a progress comment produced by Simplify.
SimplifyOutput	Objects of this class represent possible normal outputs from Simplify.
SimplifyOutputSentinel	Objects of this class represent the summary part of the normal output from Simplify: valid, invalid, or unknown.
SimplifyResult	An object of this class represent a "result" produced by Simplify.
SInt
SList	SLists represent possibly-empty lists of SExps.
SNil	The single SNil instance represents the empty list of SExps.
SPair	A SPair is a pair of a SExp and a SList; together with the SNil class, it is used to implement lists of SExps.
SubProcess	Instances of this class represent subprocesses.
TeeOutputStream	This class is a FilterOutputStream class that forwards its given output to two given OutputStreams.
TriggerlessQuantWarning	An object of this class represent a "result" produced by Simplify.

Exception Summary

SExpTypeError	This checked exception is used to signal a dynamic "type error" in the use of S-expressions.
SubProcess.Died