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 NewProver

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

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