Uses of Class
escjava.prover.ProverResponse

Packages that use ProverResponse

escjava.prover

Uses of ProverResponse in escjava.prover

Subclasses of ProverResponse in escjava.prover

class	HarveyResponse
class	SammyResponse

Fields in escjava.prover declared as ProverResponse

static ProverResponse	ProverResponse.OK A singleton response code to indicate everything is fine.
static ProverResponse	ProverResponse.FAIL A singleton response code to indicate that something is seriously wrong with the corresponding call and/or the prover and a failure has taken place.
static ProverResponse	ProverResponse.YES A singleton response code to indicate a positive response to the last command.
static ProverResponse	ProverResponse.NO A singleton response code to indicate a negative response to the last command.
static ProverResponse	ProverResponse.COUNTER_EXAMPLE A singleton response code to indicate a counter-example is available.
static ProverResponse	ProverResponse.SYNTAX_ERROR A singleton response code to indicate a syntax error in the corresponding prover call.
static ProverResponse	ProverResponse.PROGRESS_INFORMATION A singleton response code to indicate that some progress information is available from the prover.
static ProverResponse	ProverResponse.TIMEOUT A singleton response code to indicate that the prover has timed out on the corresponding prover call.
static ProverResponse	ProverResponse.INCONSISTENCY_WARNING A singleton response code to indicate an inconsistency warning from the prover for one or more of the previous ProverInterface#declare_axiom(Formula) and ProverInterface#make_assumption(Formula) calls.

Methods in escjava.prover that return ProverResponse

static ProverResponse	SammyResponse.factory(int return_code)
ProverResponse	Sammy.start_prover()
ProverResponse	Sammy.set_prover_resource_flags(java.util.Properties properties)
ProverResponse	Sammy.signature(Signature signature)
ProverResponse	Sammy.declare_axiom(Formula formula)
ProverResponse	Sammy.make_assumption(Formula formula)
ProverResponse	Sammy.retract_assumption(int count)
ProverResponse	Sammy.is_valid(Formula formula, java.util.Properties properties)
ProverResponse	Sammy.stop_prover()
private ProverResponse	Sammy.execute(java.lang.String cmd) call to sammy using xml rpc commands available : start_solver set_flags type_declaration func_declaration add_assertion query backtrack stop_solver See sammy's cvcl/smt/README.TXT for further informations
static ProverResponse	ProverResponse.factory(int return_code)
abstract ProverResponse	NewProver.start_prover() Start up the prover.
abstract ProverResponse	NewProver.set_prover_resource_flags(java.util.Properties properties) Send arbitrary information to the prover.
abstract ProverResponse	NewProver.signature(Signature signature) Send the signature of a new theory to the prover.
abstract ProverResponse	NewProver.declare_axiom(Formula formula) Declare a new axiom in the current theory.
abstract ProverResponse	NewProver.make_assumption(Formula formula) Make an assumption.
abstract ProverResponse	NewProver.retract_assumption(int count) Retract some assumptions.
abstract ProverResponse	NewProver.is_valid(Formula formula, java.util.Properties properties) Check the validity of the given formula given the current theory, its axioms, and the current set of assumptions.
abstract ProverResponse	NewProver.stop_prover() Stop the prover.
static ProverResponse	HarveyResponse.factory(int return_code)
ProverResponse	Harvey.start_prover()
ProverResponse	Harvey.set_prover_resource_flags(java.util.Properties properties)
ProverResponse	Harvey.signature(Signature signature)
ProverResponse	Harvey.declare_axiom(Formula formula)
ProverResponse	Harvey.make_assumption(Formula formula)
ProverResponse	Harvey.retract_assumption(int count)
ProverResponse	Harvey.is_valid(Formula formula, java.util.Properties properties)
ProverResponse	Harvey.stop_prover()
ProverResponse	Cvc3.start_prover() Starts a new instance of CVC3.
ProverResponse	Cvc3.set_prover_resource_flags(java.util.Properties properties) Sets command line flags for CVC3.
ProverResponse	Cvc3.signature(Signature signature) Declares a signature to CVC3.
ProverResponse	Cvc3.declare_axiom(Formula formula) Same as make_asumption.
ProverResponse	Cvc3.make_assumption(Formula formula) Asserts a formula to cvc3.
ProverResponse	Cvc3.retract_assumption(int count) Retracts some number of previous assumptions.
ProverResponse	Cvc3.is_valid(Formula formula, java.util.Properties properties) Perform a query on a formula.
ProverResponse	Cvc3.stop_prover() Destroys the current instance of cvc3.

Methods in escjava.prover with parameters of type ProverResponse

(package private) static void

Cvc3.printResponse(ProverResponse r)