|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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()
|
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |