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)