ua.gradsoft.termware.set
Class SetPatternTerm

java.lang.Object
  ua.gradsoft.termware.Term
      ua.gradsoft.termware.AbstractComplexTerm
          ua.gradsoft.termware.set.SetPatternTerm

All Implemented Interfaces:

Serializable, Cloneable

public class SetPatternTerm
extends AbstractComplexTerm

Set pattern: term for expression { $x: $Y }. unify ({ frs, snd }, S) is succesfull if frs is unified with some element of S, and snd is unified with rest of set.

See Also:

Serialized Form

Field Summary

Fields inherited from class ua.gradsoft.termware.AbstractComplexTerm

emptyFv_

Method Summary

boolean	boundEquals(Term t) equality, when propositional variables are already bounded.
boolean	boundUnify(Term t, Substitution s) unification when we already have s and when same propositional variables means same things
PartialOrderingResult	concreteOrder(Term x, Substitution s) compare for 'more concrete' relation.
Term	createSame(Term[] newBody) create term, with same name but new body.
static Term	createSetPattern(Term frs, Term snd) return new set pattern.
boolean	emptyFv() true, if term does not contains free propositional variables.
boolean	freeEquals(Term t) Equality when all propositional variables are equal
int	getArity() get arity of term.
String	getName() get name of term.
Object	getNameIndex() get name index in bounded symbol table or sust string, if name in symbol table does not exists.
String	getPatternName() get name, for which we can forse unfication.
Object	getPatternNameIndex() get index for pattern name.
Term	getSubtermAt(int i) get i-th subterm.
int	maxFv() get maximum index of free propositional variable in term
int	minFv() get minimal index of free propositional variable in term.
void	print(PrintStream out) print term on out
void	setSubtermAt(int i, Term t) set i-th subterm.
void	shiftFv(int newMin) shift set of propositional variables to start from newMinFv
Term	subst(Substitution s) receive new term, which is sibstution of current term and s
boolean	substInside(Substitution s) apply substitution s to current term.
Term	termClone() do 'deep-clone' of object.

Methods inherited from class ua.gradsoft.termware.AbstractComplexTerm

clone, findSubtermIndexBoundEqualsTo, freeUnify, getBigDecimal, getBigInteger, getBoolean, getByte, getChar, getDouble, getFloat, getInt, getJavaObject, getLong, getNumber, getPrimaryType0, getShort, getString, getTerm, getXIndex, isAtom, isBigDecimal, isBigInteger, isBoolean, isByte, isChar, isComplexTerm, isDouble, isFloat, isInt, isJavaObject, isLong, isNil, isNumber, isShort, isString, isX, normalizeFv, print, recheckEmptyFv, resetFV, termCompare

Methods inherited from class ua.gradsoft.termware.Term

containsSubtermBoundEqualsTo, getAsBigDecimal, getAsBigInteger, getAsBoolean, getAsByte, getAsChar, getAsDouble, getAsFloat, getAsInt, getAsJavaObject, getAsLong, getAsNumber, getAsShort, getAsString, getPrimaryType1, println, println

Methods inherited from class java.lang.Object

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

Method Detail

createSetPattern

public static Term createSetPattern(Term frs,
                                    Term snd)
                             throws TermWareException

return new set pattern. frs_ - pattern snd_ - rest of set.

Throws:

TermWareException

getName

public final String getName()

Description copied from class: AbstractComplexTerm

get name of term. (i. e. functional symbold)

Specified by:

getName in class AbstractComplexTerm

Returns:

name

getNameIndex

public final Object getNameIndex()

Description copied from class: AbstractComplexTerm

get name index in bounded symbol table or sust string, if name in symbol table does not exists.

Specified by:

getNameIndex in class AbstractComplexTerm

getPatternName

public final String getPatternName()

Description copied from class: AbstractComplexTerm

get name, for which we can forse unfication.

Overrides:

getPatternName in class AbstractComplexTerm

getPatternNameIndex

public final Object getPatternNameIndex()

Description copied from class: AbstractComplexTerm

get index for pattern name.

Overrides:

getPatternNameIndex in class AbstractComplexTerm

getArity

public final int getArity()

Description copied from class: AbstractComplexTerm

get arity of term.

Specified by:

getArity in class AbstractComplexTerm

Returns:

arity of term

getSubtermAt

public Term getSubtermAt(int i)

Description copied from class: AbstractComplexTerm

get i-th subterm.

Specified by:

getSubtermAt in class AbstractComplexTerm

Parameters:

i - - index of subterm to get.

Returns:

subterm, which located by index i

setSubtermAt

public void setSubtermAt(int i,
                         Term t)

Description copied from class: AbstractComplexTerm

set i-th subterm.

Specified by:

setSubtermAt in class AbstractComplexTerm

Parameters:

i - - indext of subterm to set.

t - - subterm to set.

boundUnify

public boolean boundUnify(Term t,
                          Substitution s)
                   throws TermWareException

Description copied from class: Term

unification when we already have s and when same propositional variables means same things

Overrides:

boundUnify in class AbstractComplexTerm

Throws:

TermWareException

substInside

public boolean substInside(Substitution s)
                    throws TermWareException

apply substitution s to current term.

Overrides:

substInside in class AbstractComplexTerm

Returns:

true, if substitution change term, otherwise false

Throws:

TermWareException

subst

public Term subst(Substitution s)
           throws TermWareException

Description copied from class: AbstractComplexTerm

receive new term, which is sibstution of current term and s

Overrides:

subst in class AbstractComplexTerm

Throws:

TermWareException

freeEquals

public boolean freeEquals(Term t)
                   throws TermWareException

Equality when all propositional variables are equal

Overrides:

freeEquals in class AbstractComplexTerm

Parameters:

t - - term to compare.

Returns:

true, if terms are free-equals.

Throws:

TermWareException

boundEquals

public boolean boundEquals(Term t)
                    throws TermWareException

Description copied from class: Term

equality, when propositional variables are already bounded.

Overrides:

boundEquals in class AbstractComplexTerm

Parameters:

t - - term to compare.

Returns:

true, if terms are bound-equals.

Throws:

TermWareException

concreteOrder

public PartialOrderingResult concreteOrder(Term x,
                                           Substitution s)
                                    throws TermWareException

Description copied from class: Term

compare for 'more concrete' relation. i. e. x.<(concrete)<(y) means, that for each substitution of free variables sx exists substituion sy : x[sx] = y[sy] .
Substitution s store previously matched variables.

Specified by:

concreteOrder in class Term

Throws:

TermWareException

termClone

public Term termClone()
               throws TermWareException

Description copied from class: AbstractComplexTerm

do 'deep-clone' of object. i. e. after calling termClone we sure, that call of setSubtermAt() in any subtree of deepClone of original term does not affect original term.

Specified by:

termClone in class AbstractComplexTerm

Throws:

TermWareException

emptyFv

public boolean emptyFv()

Description copied from class: Term

true, if term does not contains free propositional variables. (fv-set for this term is empty.)

Overrides:

emptyFv in class AbstractComplexTerm

Returns:

true, if fv_set does not contains free proporsitional variables.

minFv

public int minFv()
          throws TermWareException

Description copied from class: Term

get minimal index of free propositional variable in term.

Overrides:

minFv in class AbstractComplexTerm

Returns:

index of propositional variable with minimal index.

Throws:

TermWareException

maxFv

public int maxFv()
          throws TermWareException

Description copied from class: Term

get maximum index of free propositional variable in term

Overrides:

maxFv in class AbstractComplexTerm

Returns:

index of propositional variable with maximal index.

Throws:

TermWareException

shiftFv

public void shiftFv(int newMin)
             throws TermWareException

Description copied from class: AbstractComplexTerm

shift set of propositional variables to start from newMinFv

Overrides:

shiftFv in class AbstractComplexTerm

Parameters:

newMin - new minimal index of propositional variable in term

Throws:

TermWareException

print

public void print(PrintStream out)

Description copied from class: Term

print term on out

Overrides:

print in class Term

Parameters:

out - - PrintStream, where to print term.

createSame

public Term createSame(Term[] newBody)
                throws TermWareException

Description copied from class: Term

create term, with same name but new body. If this term have arity 0, or other than original - throws exception.

Specified by:

createSame in class AbstractComplexTerm

Throws:

TermWareException