escjava.prover
Class Cvc3

java.lang.Object
  escjava.prover.NewProver
      escjava.prover.Cvc3

public class Cvc3

extends NewProver

Field Summary

(package private) static boolean	debug
private static escjava.prover.jniw.Cvc3Wrapper	wrapper

Fields inherited from class escjava.prover.NewProver

signature_defined, started

Constructor Summary

Cvc3(boolean debug)

Method Summary

ProverResponse	declare_axiom(Formula formula) Same as make_asumption.
ProverResponse	is_valid(Formula formula, java.util.Properties properties) Perform a query on a formula.
static void	main(java.lang.String[] argv)
ProverResponse	make_assumption(Formula formula) Asserts a formula to cvc3.
(package private) static void	printResponse(ProverResponse r)
ProverResponse	retract_assumption(int count) Retracts some number of previous assumptions.
ProverResponse	set_prover_resource_flags(java.util.Properties properties) Sets command line flags for CVC3.
ProverResponse	signature(Signature signature) Declares a signature to CVC3.
ProverResponse	start_prover() Starts a new instance of CVC3.
ProverResponse	stop_prover() Destroys the current instance of cvc3.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

wrapper

private static escjava.prover.jniw.Cvc3Wrapper wrapper

debug

static boolean debug

Constructor Detail

Cvc3

public Cvc3(boolean debug)

Method Detail

start_prover

public ProverResponse start_prover()

Starts a new instance of CVC3. This is necessary in order to redefine any functions or variables used.

Specified by:

start_prover in class NewProver

Returns:

OK (or exit)

set_prover_resource_flags

public ProverResponse set_prover_resource_flags(java.util.Properties properties)

Sets command line flags for CVC3. Flag are currently just strings in the properties.

Specified by:

set_prover_resource_flags in class NewProver

Parameters:

properties - is a table of the flags. Keys and entries are strings, and are concatenated together to form each flag (so there is no functional difference between ["a b",""] and ["a","b"]).

Returns:

OK or SYNTAX_ERROR, as appropriate.

signature

public ProverResponse signature(Signature signature)

Declares a signature to CVC3. The signature is assumed to be a string of a sequence of CVC-readable declaration commands (each terminated by a semicolon).

Specified by:

signature in class NewProver

Parameters:

signature - the signature of the new theory.

Returns:

ProverResponse.OK if no problems encountered, otherwise ProverResponse.FAIL.

declare_axiom

public ProverResponse declare_axiom(Formula formula)

Same as make_asumption.

Specified by:

declare_axiom in class NewProver

Parameters:

formula -

Returns:

a response code.

make_assumption

public ProverResponse make_assumption(Formula formula)

Asserts a formula to cvc3.

Specified by:

make_assumption in class NewProver

Parameters:

formula - the assumption to make.

Returns:

OK, FAIL, or INCONSISTENCY_WARNING. INCONSISTENCY_WARNING will indicate the current (post-assertion) context has been detected as inconsistent.

retract_assumption

public ProverResponse retract_assumption(int count)

Retracts some number of previous assumptions.

Specified by:

retract_assumption in class NewProver

Parameters:

count - the number of undos. If count < = 0 then do nothing. If count > the number of assertions, all assertions will be undone.

Returns:

OK.

is_valid

public ProverResponse is_valid(Formula formula,
                               java.util.Properties properties)

Perform a query on a formula.

Specified by:

is_valid in class NewProver

Parameters:

formula - the formula to be checked.

properties - not currently used

Returns:

YES (is valid), COUNTEREXAMPLE (possibly spurious), or TIMEOUT. Note is is possible to also distinguish truly invalid operations from invalid-but-possibly-incomplete ones, but there does not appear to be a ProverResponse for "don't know" responses that allows the (possible) counterexample.

stop_prover

public ProverResponse stop_prover()

Destroys the current instance of cvc3. It is necessary to call start_solver() to do further processing. Returns OK or FAIL.

Specified by:

stop_prover in class NewProver

Returns:

a response code.

printResponse

static void printResponse(ProverResponse r)

main

public static void main(java.lang.String[] argv)