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 CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.prover
Class ProverResponse

    java.lang.Object
      escjava.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)

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 CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage