fmrisc.ProofNavigator.Proving

Interface Prover

All Known Implementing Classes:

CVCL

public interface Prover

Method Summary

Modifier and Type	Method and Description
boolean	abort() Abort current prover activity.
void	addDeclaration(Declaration decl) add declaration
void	assertAxiom(Expression axiom) assert axiom about previously asserted declarations.
void	assertFormula(Expression formula) assert truth of formula.
void	generateCounterExamples(boolean generate) generate counterexamples, if possible.
java.lang.String	getError() error message, if last command signalled a problem
boolean	isOkay() true iff prover is okay after creation
void	popContext() End subcontext for formula assertions.
void	pushContext() Start a new subcontext for formula assertions.
Answer	queryFormula(Expression formula) query truth of formula.
Expression	simplifyExpression(Expression exp) simplify expression
void	terminate(boolean wait) Terminate prover instance.
void	tryHard(boolean hard) Try hard to simplify (potentially timeconsuming).

Method Detail

isOkay

boolean isOkay()

true iff prover is okay after creation

Returns:

true iff prover is okay

getError

java.lang.String getError()

error message, if last command signalled a problem

Returns:

error message

generateCounterExamples

void generateCounterExamples(boolean generate)

generate counterexamples, if possible.

Parameters:

generate - true iff counterexamples are to be generated

tryHard

void tryHard(boolean hard)

Try hard to simplify (potentially timeconsuming).

Parameters:

hard - true iff prover is to try hard.

addDeclaration

void addDeclaration(Declaration decl)

add declaration

Parameters:

decl - declaration that is added to prover state

assertAxiom

void assertAxiom(Expression axiom)

assert axiom about previously asserted declarations.

Parameters:

axiom - formula whose truth is asserted; declaration symbols must be only used in context of axiom.

pushContext

void pushContext()

Start a new subcontext for formula assertions.

popContext

void popContext()

End subcontext for formula assertions. All assertions since the last pushContext() are undone.

assertFormula

void assertFormula(Expression formula)

assert truth of formula.

Parameters:

formula - formula whose truth is asserted.

queryFormula

Answer queryFormula(Expression formula)

query truth of formula.

Parameters:

formula - formula whose truth is queried.

Returns:

the prover answer (null, if a problem occured)

simplifyExpression

Expression simplifyExpression(Expression exp)

simplify expression

Parameters:

exp - expression to be simplified

Returns:

the simplified expression (null, if a problem occured)

terminate

void terminate(boolean wait)

Terminate prover instance.

Parameters:

wait - true if to wait for termination.

abort

boolean abort()

Abort current prover activity.

Returns:

true iff new prover could be successfully started.