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

escjava.prover
Class ProverResponse

java.lang.Object
  extended byescjava.prover.ProverResponse
Direct Known Subclasses:
HarveyResponse, SammyResponse

public class ProverResponse
extends java.lang.Object


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

OK

public static ProverResponse OK
A singleton response code to indicate everything is fine.


FAIL

public 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. A response code of FAIL typically indicates a non-correctable situation. The info field should be consulted for additional information, and no further calls, but for ProverInterface#stop_prover() should be made.


YES

public static ProverResponse YES
A singleton response code to indicate a positive response to the last command.


NO

public static ProverResponse NO
A singleton response code to indicate a negative response to the last command.


COUNTER_EXAMPLE

public static ProverResponse COUNTER_EXAMPLE
A singleton response code to indicate a counter-example is available. The counter-example is contained in the formula field of this response object.


SYNTAX_ERROR

public static ProverResponse SYNTAX_ERROR
A singleton response code to indicate a syntax error in the corresponding prover call. The info field should be consulted for additional information.


PROGRESS_INFORMATION

public static ProverResponse PROGRESS_INFORMATION
A singleton response code to indicate that some progress information is available from the prover. The info field should be consulted for additional information.


TIMEOUT

public static ProverResponse TIMEOUT
A singleton response code to indicate that the prover has timed out on the corresponding prover call. The info and/or formula fields should be consulted for additional information.


INCONSISTENCY_WARNING

public 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. The info and/or formula fields should be consulted for additional information.


formula

public Formula formula
A formula. Typically, this field is used to represent a counter-example in response to a call to ProverInterface#is_valid(Formula).


info

public java.util.Properties info
A set of properties. Typically, this field is used to represent property/value pairs specific to reporting prover progress, state, resource utilization, etc.

Constructor Detail

ProverResponse

protected ProverResponse()
A private constructor that is only to be used during static initialization.

Method Detail

factory

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

The ESC/Java2 Project Homepage