|
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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.prover.NewProver
Field Summary | |
boolean |
signature_defined
|
boolean |
started
|
Constructor Summary | |
NewProver()
|
Method Summary | |
abstract ProverResponse |
declare_axiom(Formula formula)
Declare a new axiom in the current theory. |
abstract ProverResponse |
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 |
make_assumption(Formula formula)
Make an assumption. |
abstract ProverResponse |
retract_assumption(int count)
Retract some assumptions. |
abstract ProverResponse |
set_prover_resource_flags(java.util.Properties properties)
Send arbitrary information to the prover. |
abstract ProverResponse |
signature(Signature signature)
Send the signature of a new theory to the prover. |
abstract ProverResponse |
start_prover()
Start up the prover. |
abstract ProverResponse |
stop_prover()
Stop the prover. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public boolean started
public boolean signature_defined
Constructor Detail |
public NewProver()
Method Detail |
public abstract ProverResponse start_prover()
ProverResponse.OK
indicates that the prover started successfully
and is ready to receive commands. A response code of ProverResponse.FAIL
indicates that the prover did not start
successfully and is not ready to receive commands. In the latter
case, ProverResponse.FAIL.info
can contain additional
arbitrary information about the failure.public abstract ProverResponse set_prover_resource_flags(java.util.Properties properties)
properties
- the set of property/value pairs to send to the
prover.
public abstract ProverResponse signature(Signature signature)
Signature
object, not by a null
value.
signature
- the signature of the new theory.
public abstract ProverResponse declare_axiom(Formula formula)
formula
-
public abstract ProverResponse make_assumption(Formula formula)
formula
- the assumption to make.
public abstract ProverResponse retract_assumption(int count)
count
- the number of assumptions to retract.
public abstract ProverResponse is_valid(Formula formula, java.util.Properties properties)
formula
- the formula to check.properties
- a set of hints, primarily resource bounds on
this validity check.
public abstract ProverResponse 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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |