fmrisc.ProofNavigator.Syntax

Class ExistsFormula

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.QuantifiedExpression

fmrisc.ProofNavigator.Syntax.ExistsFormula

All Implemented Interfaces:

AST, Expression

public final class ExistsFormula
extends QuantifiedExpression

Handling of universally quantified formulas.

Constructor Summary

Constructors

Constructor and Description
ExistsFormula(TypedIdentifier[] variables, Expression base) construct exists formula of variables and base formula

Method Summary

Modifier and Type	Method and Description
QuantifiedExpression	construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Syntax.QuantifiedExpression

accept, getBase, getPriority, getVariables, instantiate, 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

ExistsFormula

public ExistsFormula(TypedIdentifier[] variables,
                     Expression base)

construct exists formula of variables and base formula

Parameters:

variables - the quantified variables

base - the base formula

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.

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in interface AST

Overrides:

printCore in class QuantifiedExpression

Parameters:

out - the stream on which the text is written