at.jku.risc.stout.nau.algo

Class Equivariance

java.lang.Object

at.jku.risc.stout.nau.algo.Equivariance

public class Equivariance
extends Object

This class encapsulates the rule based system EquivarianceSystem and allows to justify the result by applying the computed permutation and testing alpha equivalence.

Author:

Alexander Baumgartner

Constructor Summary

Constructors

Constructor and Description
Equivariance(EquationSystem<EquivarianceProblem> eqSys, Collection<? extends Atom> atoms, FreshnessCtx nablaIn) Creates and initializes the encapsulated rule based system EquivarianceSystem with the given equation system, atoms and freshness context.

Method Summary

Methods

Modifier and Type	Method and Description
Permutation	compute(NodeFactory factory, boolean justify, DebugLevel debugLevel, PrintStream out) Calls the rule based system EquivarianceSystem and tries to justify the computed result if the second argument of this method is true.
Collection<? extends Atom>	getAtoms()
EquationSystem<EquivarianceProblem>	getEqSys()
FreshnessCtx	getNablaIn()

Methods inherited from class java.lang.Object

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

Constructor Detail

Equivariance

public Equivariance(EquationSystem<EquivarianceProblem> eqSys,
            Collection<? extends Atom> atoms,
            FreshnessCtx nablaIn)

Creates and initializes the encapsulated rule based system EquivarianceSystem with the given equation system, atoms and freshness context.

Method Detail

compute

public Permutation compute(NodeFactory factory,
                  boolean justify,
                  DebugLevel debugLevel,
                  PrintStream out)
                    throws ControlledException

Calls the rule based system EquivarianceSystem and tries to justify the computed result if the second argument of this method is true.

Throws:

ControlledException

getAtoms

public Collection<? extends Atom> getAtoms()

getEqSys

public EquationSystem<EquivarianceProblem> getEqSys()

getNablaIn

public FreshnessCtx getNablaIn()