|
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.ProverResponse
Field Summary | |
static ProverResponse |
COUNTER_EXAMPLE
A singleton response code to indicate a counter-example is available. |
static 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. |
Formula |
formula
A formula. |
static 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. |
java.util.Properties |
info
A set of properties. |
static ProverResponse |
NO
A singleton response code to indicate a negative response to the last command. |
static ProverResponse |
OK
A singleton response code to indicate everything is fine. |
static ProverResponse |
PROGRESS_INFORMATION
A singleton response code to indicate that some progress information is available from the prover. |
static ProverResponse |
SYNTAX_ERROR
A singleton response code to indicate a syntax error in the corresponding prover call. |
static ProverResponse |
TIMEOUT
A singleton response code to indicate that the prover has timed out on the corresponding prover call. |
static ProverResponse |
YES
A singleton response code to indicate a positive response to the last command. |
Constructor Summary | |
protected |
ProverResponse()
A private constructor that is only to be used during static initialization. |
Method Summary | |
static ProverResponse |
factory(int return_code)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static ProverResponse OK
public static ProverResponse FAIL
info
field should be
consulted for additional information, and no further calls, but
for ProverInterface#stop_prover()
should be made.
public static ProverResponse YES
public static ProverResponse NO
public static ProverResponse COUNTER_EXAMPLE
formula
field of this response object.
public static ProverResponse SYNTAX_ERROR
info
field should be
consulted for additional information.
public static ProverResponse PROGRESS_INFORMATION
info
field should be consulted for additional information.
public static ProverResponse TIMEOUT
info
and/or
formula
fields should be consulted for additional
information.
public static ProverResponse INCONSISTENCY_WARNING
ProverInterface#declare_axiom(Formula)
and ProverInterface#make_assumption(Formula)
calls. The info
and/or formula
fields should be consulted for
additional information.
public Formula formula
ProverInterface#is_valid(Formula)
.
public java.util.Properties info
Constructor Detail |
protected ProverResponse()
Method Detail |
public static ProverResponse factory(int return_code)
|
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 |