Package | Description |
---|---|
at.jku.risc.stout.nau.algo |
This package contains the classes of the rule based system
(
AntiUnifySystem ) to solve the nominal
anti-unification problem and an algorithm to solve the nominal
equivariance problem (EquivarianceSystem )
which is needed by the anti-unification algorithm. |
at.jku.risc.stout.nau.data |
This package contains the nominal parser and some container classes like
equation systems, freshness context and a container for nominal pairs.
|
at.jku.risc.stout.nau.data.atom |
This package contains the classes which are needed to build up the term tree
(E.g.: Atom,
Abstraction,
FunctionApplication,
Suspension,
SortAtom,
SortData,
NodeFactory,...).
|
Modifier and Type | Method and Description |
---|---|
Collection<? extends Atom> |
Equivariance.getAtoms() |
Modifier and Type | Method and Description |
---|---|
boolean |
EquivarianceSystem.putAtom(DebugLevel debugLevel,
PrintStream out,
Atom lAtom,
Atom rAtom) |
Modifier and Type | Method and Description |
---|---|
void |
EquivarianceSystem.start(Collection<? extends Atom> atoms,
FreshnessCtx nablaIn)
Initializes the permutation computation.
|
Constructor and Description |
---|
AntiUnifySystem(NodeFactory factory,
EquationSystem<AntiUnifyProblem> problemSet,
FreshnessCtx nablaIn,
Collection<? extends Atom> atoms,
List<AntiUnifyProblem> store,
FreshnessCtx nablaGen,
Substitution sigma)
Creates and initializes the rule based system.
|
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.
|
Modifier and Type | Field and Description |
---|---|
Class<? extends Atom> |
NodeFactory.classAtom
Class to use for atom instantiation.
|
Modifier and Type | Method and Description |
---|---|
Atom |
NodeFactory.newAtom(String name)
Instantiates an untyped atom.
|
Atom |
NodeFactory.newAtom(String name,
SortAtom sort)
Instantiates an atom of the specified sort.
|
Atom |
NodeFactory.newAtom(String name,
String sort)
Instantiates an atom of the specified sort.
|
Atom |
NodeFactory.obtainFreshAtom(SortAtom sort) |
Modifier and Type | Method and Description |
---|---|
Set<Atom> |
FreshnessCtx.get(Variable fresh) |
Set<Atom> |
InputParser.parseAtomSet(Reader in) |
Set<Atom> |
FreshnessCtx.removeAll(Variable var) |
Modifier and Type | Method and Description |
---|---|
void |
FreshnessCtx.addFreshConstraint(Atom atom,
NominalTerm... nomTerms)
Add freshness constraints as needed, such that the given atom is fresh in
all the given nominal terms.
|
boolean |
FreshnessCtx.contains(Atom atom,
Variable var) |
Set<Variable> |
FreshnessCtx.get(Atom fresh) |
boolean |
NominalPair.prooveFresh(Atom atom)
Tests whether the given atom is fresh in the nominal term respecting the
freshness context.
|
void |
FreshnessCtx.put(Atom freshA,
Collection<Variable> forVar) |
void |
FreshnessCtx.put(Atom freshA,
Variable... forVar) |
void |
FreshnessCtx.put(Variable forVar,
Atom... freshA) |
void |
FreshnessCtx.remove(Atom freshA,
Variable forVar) |
Set<Variable> |
FreshnessCtx.removeAll(Atom atom) |
void |
NominalPair.swap(Atom a1,
Atom a2)
Applies a swapping to this nominal pair.
|
FreshnessCtx |
FreshnessCtx.swap(Atom a,
Atom b)
Creates a new freshness context with swapped atoms.
|
Modifier and Type | Method and Description |
---|---|
void |
FreshnessCtx.put(Variable forVar,
Collection<Atom> freshA) |
Modifier and Type | Method and Description |
---|---|
Atom |
Abstraction.getBoundAtom() |
Atom |
Permutation.permute(Atom key)
Applies the permutation to the given Atom and returns the
permuted atom.
|
Atom |
Atom.permute(Permutation perm) |
Atom |
Permutation.permuteInverse(Atom key)
Applies the inverse permutation to the given Atom and
returns the inverse permuted atom.
|
Atom |
Atom.swap(Atom a1,
Atom a2) |
Modifier and Type | Method and Description |
---|---|
Map<Atom,Atom> |
Permutation.getInverse()
The internal Map representation of the inverse permutation.
|
Map<Atom,Atom> |
Permutation.getInverse()
The internal Map representation of the inverse permutation.
|
Map<Atom,Atom> |
Permutation.getPerm()
The internal Map representation of the permutation.
|
Map<Atom,Atom> |
Permutation.getPerm()
The internal Map representation of the permutation.
|
Modifier and Type | Method and Description |
---|---|
void |
Permutation.addSwappingHead(Atom a1,
Atom a2)
Adds a swapping at the head (left) of this sequence of swappings.
|
void |
Permutation.addSwappingTail(Atom a1,
Atom a2)
Adds a swapping at the tail (right) of this sequence of swappings.
|
boolean |
Atom.isFresh(Atom atom,
FreshnessCtx nabla) |
boolean |
FunctionApplication.isFresh(Atom atom,
FreshnessCtx nabla) |
boolean |
Suspension.isFresh(Atom atom,
FreshnessCtx nabla) |
boolean |
Abstraction.isFresh(Atom atom,
FreshnessCtx nabla) |
abstract boolean |
NominalTerm.isFresh(Atom atom,
FreshnessCtx nabla) |
Atom |
Permutation.permute(Atom key)
Applies the permutation to the given Atom and returns the
permuted atom.
|
Atom |
Permutation.permuteInverse(Atom key)
Applies the inverse permutation to the given Atom and
returns the inverse permuted atom.
|
void |
Abstraction.setBoundAtom(Atom boundAtom) |
Atom |
Atom.swap(Atom a1,
Atom a2) |
NominalTerm |
FunctionApplication.swap(Atom a1,
Atom a2) |
NominalTerm |
Suspension.swap(Atom a1,
Atom a2) |
NominalTerm |
Abstraction.swap(Atom a1,
Atom a2) |
abstract NominalTerm |
NominalTerm.swap(Atom a1,
Atom a2) |
Modifier and Type | Method and Description |
---|---|
void |
Atom.collectAtoms(Set<Atom> atoms) |
void |
FunctionApplication.collectAtoms(Set<Atom> atoms) |
void |
Suspension.collectAtoms(Set<Atom> atoms) |
void |
Abstraction.collectAtoms(Set<Atom> atoms) |
abstract void |
NominalTerm.collectAtoms(Set<Atom> atoms) |
Constructor and Description |
---|
Abstraction(Atom boundAtom,
NominalTerm subTerm) |