fmrisc.ProofNavigator.Syntax

Class ArrayTerm

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.QuantifiedExpression

fmrisc.ProofNavigator.Syntax.ArrayTerm

All Implemented Interfaces:

AST, Expression

public final class ArrayTerm
extends QuantifiedExpression

Handling of array terms.

Constructor Summary

Constructors

Constructor and Description
ArrayTerm(TypedIdentifier[] variables, Expression base) construct array term of variables and base term

Method Summary

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
QuantifiedExpression	construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
AxiomDeclaration	getAxiom() Get declaration of axiom replacing expression
ValueDeclaration	getConstant() Get declaration of constant replacing expression
ValueDeclIdentifier[]	getFree() Get free variables
Expression	getTerm() Get replacement term
Expression	instantiate() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
void	setAxiom(AxiomDeclaration d) Set declaration of axiom replacing expression
void	setConstant(ValueDeclaration d) Set declaration of constant replacing expression
void	setFree(ValueDeclIdentifier[] v) Set free variables
void	setTerm(Expression t) Set replacement term

Methods inherited from class fmrisc.ProofNavigator.Syntax.QuantifiedExpression

getBase, getPriority, getVariables, printCore, substitution

Methods inherited from class fmrisc.ProofNavigator.Syntax.ExpressionBase

printPriority

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTBase

print, printParens, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProofNavigator.Syntax.AST

print, printParens, toString

Constructor Detail

ArrayTerm

public ArrayTerm(TypedIdentifier[] variables,
                 Expression base)

construct array term of variables and base term

Parameters:

variables - the quantified variables

base - the base term

Method Detail

construct

public QuantifiedExpression construct(TypedIdentifier[] variables,
                                      Expression base)

Construct quantified expression.

Specified by:

construct in class QuantifiedExpression

Parameters:

variables - typed variables.

base - an expression.

Returns:

a quantified expression of the same kind as this expression with the denoted variables and base expression.

setConstant

public void setConstant(ValueDeclaration d)

Set declaration of constant replacing expression

Parameters:

d - the declaration

getConstant

public ValueDeclaration getConstant()

Get declaration of constant replacing expression

Returns:

the declaration

setAxiom

public void setAxiom(AxiomDeclaration d)

Set declaration of axiom replacing expression

Parameters:

d - the declaration

getAxiom

public AxiomDeclaration getAxiom()

Get declaration of axiom replacing expression

Returns:

the declaration

setTerm

public void setTerm(Expression t)

Set replacement term

Parameters:

t - the term

getTerm

public Expression getTerm()

Get replacement term

Returns:

the term

setFree

public void setFree(ValueDeclIdentifier[] v)

Set free variables

Parameters:

v - the variables

getFree

public ValueDeclIdentifier[] getFree()

Get free variables

Returns:

the variables

instantiate

public Expression instantiate()

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

Specified by:

instantiate in interface Expression

Overrides:

instantiate in class QuantifiedExpression

Returns:

the instantiated copy

accept

public AST accept(ASTVisitor visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Overrides:

accept in class QuantifiedExpression

Parameters:

visitor - the visitor who is accepted by this node.

Returns:

the result of the visit (may be null).