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 NewProver

java.lang.Object
  extended byescjava.prover.NewProver
Direct Known Subclasses:
Harvey, Sammy

public abstract class NewProver
extends java.lang.Object


Field Summary
 boolean signature_defined
           
 boolean started
           
 
Constructor Summary
NewProver()
           
 
Method Summary
abstract  ProverResponse declare_axiom(Formula formula)
          Declare a new axiom in the current theory.
abstract  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.
abstract  ProverResponse make_assumption(Formula formula)
          Make an assumption.
abstract  ProverResponse retract_assumption(int count)
          Retract some assumptions.
abstract  ProverResponse set_prover_resource_flags(java.util.Properties properties)
          Send arbitrary information to the prover.
abstract  ProverResponse signature(Signature signature)
          Send the signature of a new theory to the prover.
abstract  ProverResponse start_prover()
          Start up the prover.
abstract  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

started

public boolean started

signature_defined

public boolean signature_defined
Constructor Detail

NewProver

public NewProver()
Method Detail

start_prover

public abstract ProverResponse start_prover()
Start up the prover. After the prover is started correctly it should be ready to receive any of the commands embodied by all the other methods of this API.

Returns:
a response code. A response code of 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.

set_prover_resource_flags

public abstract ProverResponse set_prover_resource_flags(java.util.Properties properties)
Send arbitrary information to the prover. Typically this information is not mandatory and is only suggestions or informative information from the front-end. This data is highly prover-dependent.

Parameters:
properties - the set of property/value pairs to send to the prover.
Returns:
a response code.

signature

public abstract ProverResponse signature(Signature signature)
Send the signature of a new theory to the prover. Note that an empty signature is denoted by an empty Signature object, not by a null value.

Parameters:
signature - the signature of the new theory.
Returns:
a response code.

declare_axiom

public abstract ProverResponse declare_axiom(Formula formula)
Declare a new axiom in the current theory.

Parameters:
formula -
Returns:
a response code.

make_assumption

public abstract ProverResponse make_assumption(Formula formula)
Make an assumption.

Parameters:
formula - the assumption to make.
Returns:
a response code.

retract_assumption

public abstract ProverResponse retract_assumption(int count)
Retract some assumptions.

Parameters:
count - the number of assumptions to retract.
Returns:
a response code.

is_valid

public abstract 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.

Parameters:
formula - the formula to check.
properties - a set of hints, primarily resource bounds on this validity check.
Returns:
a response code.
Design:
kiniry 30 June 2004 - Possible alternative names for this method include check(), is_entailed(), is_an_entailed_model_of(). I prefer is_valid().

stop_prover

public abstract ProverResponse stop_prover()
Stop the prover.

Returns:
a response 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