de.uni_tuebingen.sfb.lichtenstein.formulas
Class FormulaTemplate

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaTemplate

public class FormulaTemplate
extends Object

A class that represents a template for a formula, in which certain free variables still have to be filled in to get a real formula.

This is some sort of formula builder. It works with an internal visitor. TODO: check for bound variables in constructor, in replacer, in ...?

Author:

Hendrik Maryns

Constructor Summary

FormulaTemplate(Formula template, Variable... dummies)
Initialize a new formula template, based on a formula and a list of dummy variables that appear in the formula.

Method Summary

Class<? extends Variable>	getDummyClass(int index) Returns the class of the indexth dummy variable.
Formula	getFormula(Variable... inputVariables) Return the formula that results from replacing the free variables which were supplied during the creation of this template by the variables supplied as arguments to this method.
int	getNbDummies() Returns the number of variables that has to be supplied to this template to create a formula.
Formula	getTemplateFormula() Return the formula that serves as a template.

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaTemplate

public FormulaTemplate(Formula template,
                       Variable... dummies)
                throws de.uni_tuebingen.sfb.lichtenstein.exceptions.FunctionArgumentsMismatchException

Initialize a new formula template, based on a formula and a list of dummy variables that appear in the formula.

Parameters:

template - The formula which is to serve as a template.

dummies - The variables in the formula which are dummy variables.

Postcondition:

The given template formula is stored as template formula

| new.getTemplateFormula() == template

Postcondition:

The number of dummies is the same as the length of the given list of dummies.

| new.getNbDummies() ==
       dummies.length

Postcondition:

The types of the stored dummies are the same as the types of the given dummies.

| for 0 <= i <
       dummies.length
| dummies[i].getClass() == new.getDummyClass(i)

Throws:

FunctionArgumentsMismatchException

If the formula does not contain any of the given dummy variables.

| for one 0 <= i < dummies.length | !
         template.contains(dummies[i])

Method Detail

getTemplateFormula

public Formula getTemplateFormula()

Return the formula that serves as a template.

Returns:

The template formula.

getFormula

public Formula getFormula(Variable... inputVariables)
                   throws de.uni_tuebingen.sfb.lichtenstein.exceptions.FunctionArgumentsMismatchException

Return the formula that results from replacing the free variables which were supplied during the creation of this template by the variables supplied as arguments to this method.

Parameters:

inputVariables - The variables that should be used instead of the dummy variables.

Returns:

The formula supplied at creation time, with the dummy variables replaced by the given variables, in that order.

Throws:

FunctionArgumentsMismatchException

If the number of supplied variables is not the same as the number of dummy variables.

|
         inputVariables.length != getNbDummies()

Throws:

FunctionArgumentsMismatchException

If the type of the supplied variables does not correspond to their respective dummy variable.

| for one 0 <=
         i < inputVariables.length
| inputVariables[i].getClass() != getDummyClass(i)

getNbDummies

public int getNbDummies()

Returns the number of variables that has to be supplied to this template to create a formula.

Returns:

The number of dummy variables.

getDummyClass

public Class<? extends Variable> getDummyClass(int index)
                                        throws ArrayIndexOutOfBoundsException

Returns the class of the indexth dummy variable. Thus, the indexth variable supplied to the getFormula method should be of this type.

Parameters:

index - The index of the dummy for which the class is wanted. Indices start from zero.

Returns:

The class of the dummy variable at the given index.

Throws:

ArrayIndexOutOfBoundsException

If the index is bigger than or equal to the number of dummies or smaller than zero.

| index < 0 || index >=
         getNbDummies()