de.uni_tuebingen.sfb.lichtenstein.formulas
Class FormulaTemplate

java.lang.Object
  extended by 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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

FormulaTemplate

public FormulaTemplate(Formula template,
                       Variable... dummies)
                throws 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.
Postconditions:
  • The given template formula is stored as template formula | new.getTemplateFormula() == template
  • The number of dummies is the same as the length of the given list of dummies. | new.getNbDummies() == dummies.length
  • 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 - [CAN] 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 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 - [CAN] If the number of supplied variables is not the same as the number of dummy variables. | inputVariables.length != getNbDummies()
    FunctionArgumentsMismatchException - [CAN] 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 - [CAN] If the index is bigger than or equal to the number of dummies or smaller than zero. | index < 0 || index >= getNbDummies()


    © Copyright 2008 Hendrik Maryns   Creative Commons License