Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## 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()`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage