fmrisc.Proving.CVCL
Class CVCL

java.lang.Object
  fmrisc.Proving.CVCL.CVCL

All Implemented Interfaces:

Prover

public final class CVCL
extends java.lang.Object
implements Prover

CVC Lite interface

Constructor Summary

CVCL(java.lang.String command, java.io.PrintWriter log, boolean useMask)
Create CVCL instance by call of command

Method Summary

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 CVCL instance is not okay
static java.lang.String	getExternalName(ValueDeclIdentifier ident) create CVCL identifier from given name
static java.lang.String	getOriginalName(java.lang.String name) Get original name from external CVCL name.
boolean	isOkay() true iff CVCL instance is okay
Expression	parseExpression(java.lang.String string) Parse CVCL String as an expression.
void	popContext() End subcontext for formula assertions.
void	pushContext() Start a new subcontext for formula assertions.
Answer	queryFormula(Expression formula) Query truth of formula.
void	setError(java.lang.String message) set error message
Expression	simplifyExpression(Expression exp) Simplify expression.
void	terminate() Terminate prover instance.
java.lang.String	toCVCL(Expression exp) return CVCL representation of expression
void	tryHard(boolean hard) Try hard to simplify (potentially timeconsuming).

Methods inherited from class java.lang.Object

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

Constructor Detail

CVCL

public CVCL(java.lang.String command,
            java.io.PrintWriter log,
            boolean useMask)

Create CVCL instance by call of command

Parameters:

command - command line string to invoke CVCL

log - stream to log commands to (null, if none)

useMask - true iff quantified formulas are to be masked from CVCL.

Method Detail

getExternalName

public static java.lang.String getExternalName(ValueDeclIdentifier ident)

create CVCL identifier from given name

Parameters:

ident - an identifier

Returns:

an identifier usable for CVCL

getOriginalName

public static java.lang.String getOriginalName(java.lang.String name)

Get original name from external CVCL name.

Parameters:

name - a CVCL name (may be returned by getExternalName())

Returns:

the original name (may be name itself)

isOkay

public boolean isOkay()

true iff CVCL instance is okay

Specified by:

isOkay in interface Prover

Returns:

true iff CVCL instance is okay

getError

public java.lang.String getError()

error message, if CVCL instance is not okay

Specified by:

getError in interface Prover

Returns:

error message, if !isOkay()

setError

public void setError(java.lang.String message)

set error message

Parameters:

message - the error message

generateCounterExamples

public void generateCounterExamples(boolean generate)

generate counterexamples, if possible.

Specified by:

generateCounterExamples in interface Prover

Parameters:

generate - true iff counterexamples are to be generated

tryHard

public void tryHard(boolean hard)

Try hard to simplify (potentially timeconsuming).

Specified by:

tryHard in interface Prover

Parameters:

hard - true iff prover is to try hard.

terminate

public void terminate()

Terminate prover instance.

Specified by:

terminate in interface Prover

abort

public boolean abort()

Abort current prover activity.

Specified by:

abort in interface Prover

Returns:

true iff new prover could be successfully started.

toCVCL

public java.lang.String toCVCL(Expression exp)

return CVCL representation of expression

Parameters:

exp - an expression (formula or term)

Returns:

the CVCL representation of exp

parseExpression

public Expression parseExpression(java.lang.String string)

Parse CVCL String as an expression.

Parameters:

string - the CVCL representation of an expression.

Returns:

the corresponding expression (null, if an error occured)

addDeclaration

public void addDeclaration(Declaration decl)

Add declaration.

Specified by:

addDeclaration in interface Prover

Parameters:

decl - declaration that is added to prover state.

pushContext

public void pushContext()

Start a new subcontext for formula assertions.

Specified by:

pushContext in interface Prover

popContext

public void popContext()

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

Specified by:

popContext in interface Prover

assertAxiom

public void assertAxiom(Expression axiom)

assert axiom about previously asserted declarations.

Specified by:

assertAxiom in interface Prover

Parameters:

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

assertFormula

public void assertFormula(Expression formula)

Assert truth of formula.

Specified by:

assertFormula in interface Prover

Parameters:

formula - formula whose truth is asserted.

queryFormula

public Answer queryFormula(Expression formula)

Query truth of formula.

Specified by:

queryFormula in interface Prover

Parameters:

formula - formula whose truth is queried.

Returns:

the prover answer (null, if a problem occured).

simplifyExpression

public Expression simplifyExpression(Expression exp)

Simplify expression.

Specified by:

simplifyExpression in interface Prover

Parameters:

exp - expression to be simplified.

Returns:

the simplified expression (null, if a problem occured).