|
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
escjava.prover.Harvey
Field Summary | |
(package private) static boolean |
debug
|
(package private) SubProcess |
P
|
Fields inherited from class escjava.prover.NewProver |
signature_defined, started |
Constructor Summary | |
Harvey(boolean debug)
|
Method Summary | |
ProverResponse |
declare_axiom(Formula formula)
Declare a new axiom in the current theory. |
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. |
static void |
main(java.lang.String[] argv)
|
ProverResponse |
make_assumption(Formula formula)
Make an assumption. |
ProverResponse |
retract_assumption(int count)
Retract some assumptions. |
ProverResponse |
set_prover_resource_flags(java.util.Properties properties)
Send arbitrary information to the prover. |
ProverResponse |
signature(Signature signature)
Send the signature of a new theory to the prover. |
ProverResponse |
start_prover()
Start up the prover. |
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 |
SubProcess P
static boolean debug
Constructor Detail |
public Harvey(boolean debug)
Method Detail |
public ProverResponse start_prover()
NewProver
start_prover
in class NewProver
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 ProverResponse set_prover_resource_flags(java.util.Properties properties)
NewProver
set_prover_resource_flags
in class NewProver
properties
- the set of property/value pairs to send to the
prover.
public ProverResponse signature(Signature signature)
NewProver
Signature
object, not by a null
value.
signature
in class NewProver
signature
- the signature of the new theory.
public ProverResponse declare_axiom(Formula formula)
NewProver
declare_axiom
in class NewProver
formula
-
public ProverResponse make_assumption(Formula formula)
NewProver
make_assumption
in class NewProver
formula
- the assumption to make.
public ProverResponse retract_assumption(int count)
NewProver
retract_assumption
in class NewProver
count
- the number of assumptions to retract.
public ProverResponse is_valid(Formula formula, java.util.Properties properties)
NewProver
is_valid
in class NewProver
formula
- the formula to check.properties
- a set of hints, primarily resource bounds on
this validity check.
public ProverResponse stop_prover()
NewProver
stop_prover
in class NewProver
public static void main(java.lang.String[] argv)
|
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 |