Class RuleTable

java.lang.Object
  |
  +--java.util.Dictionary
        |
        +--java.util.Hashtable
              |
              +--RuleTable

All Implemented Interfaces:

Cloneable, Map, Serializable

public class RuleTable

extends Hashtable

This class implement the table of oriented rules of a system. The table map a function to a list of rewrite axiom (its definition).

Author:

P. URSO

See Also:

Function, FunctionDefinition, RewriteRule, Serialized Form

Inner classes inherited from class java.util.Map

Map.Entry

Constructor Summary

RuleTable()
Constructor of the table of rule.

RuleTable(Hypothese h)
Constructor from only one Hypothese.

Method Summary

RewriteRule	addRuleFrom(SpecialClause c) Makes a rule with the specified special clause if possible and add it to this table.
void	addToDefiniton(RewriteRule rule) Puts a new rewrite rule at the definitions.
SCList	getAllDefinitions() Returns a list of all definitions in this table.
FunctionDefinition	getDefinition(Function id) Gets the definition of a specified function in this table.
String	getPositions() Returns a string representation of all induction positions of functions defined in this table.
RewriteRule	lastUsed() Returns last rule used.
Hypothese	makeHypotheseFrom(Conjecture c) Makes an hypothese with the specified conjecture and add it to this table if the clause is oriented, add to hypothesis table if semi-oriented or just make an hypothese.
void	parsePositions(boolean mono) Parse positions in function definitions.
void	remove(SCList l) Removes all rewrite rules of a specified list from this table.
void	setLastUsed(RewriteRule rule) Sets last rule used.

Methods inherited from class java.util.Hashtable

clear, clone, contains, containsKey, containsValue, elements, entrySet, equals, get, hashCode, isEmpty, keys, keySet, put, putAll, rehash, remove, size, toString, values

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

RuleTable

public RuleTable(Hypothese h)

Constructor from only one Hypothese. If the hypothesis is not a Rewrite Rule, makes an empty table.

Parameters:

clause - the uniq clause of the table.

RuleTable

public RuleTable()

Constructor of the table of rule.

Method Detail

lastUsed

public RewriteRule lastUsed()

Returns last rule used.

setLastUsed

public void setLastUsed(RewriteRule rule)

Sets last rule used.

addToDefiniton

public void addToDefiniton(RewriteRule rule)

Puts a new rewrite rule at the definitions. The function to be mapped will be find in the rule.

Parameters:

rule - the rewrite rule.

remove

public void remove(SCList l)

Removes all rewrite rules of a specified list from this table.

Parameters:

l - list of special clauses to remove if they are oriented.

getDefinition

public FunctionDefinition getDefinition(Function id)

Gets the definition of a specified function in this table.

Parameters:

id - the function.

Returns:

the function definition.

addRuleFrom

public RewriteRule addRuleFrom(SpecialClause c)

Makes a rule with the specified special clause if possible and add it to this table. Such a rule could be make only if the clause is oriented.

Parameters:

c - the specified clause.

Returns:

the rewrite rule if it was created, null otherwise.

See Also:

Node

makeHypotheseFrom

public Hypothese makeHypotheseFrom(Conjecture c)

Makes an hypothese with the specified conjecture and add it to this table if the clause is oriented, add to hypothesis table if semi-oriented or just make an hypothese.

Parameters:

c - the specified clause.

Returns:

the hypothese created.

parsePositions

public void parsePositions(boolean mono)

Parse positions in function definitions. Sets induction positions map of defined function.

Parameters:

mono - true for a monomorphic rewrite system.

getAllDefinitions

public SCList getAllDefinitions()

Returns a list of all definitions in this table. The list is not backed to the table.

getPositions

public String getPositions()

Returns a string representation of all induction positions of functions defined in this table.