Class RewriteSystem

java.lang.Object
  |
  +--RewriteSystem

All Implemented Interfaces:

Cloneable

public class RewriteSystem

extends Object

implements Cloneable

This class implements a rewrite system.

Author:

P. URSO

See Also:

RuleTable, SCList, ConjectureList

Field Summary

protected String	genTrack
protected String	splitTrack
protected String	stepTrack
protected String	track

Constructor Summary

RewriteSystem(String name, SCList axioms, IdentTable idt)
Constructor of the rewrite system.

Method Summary

ConjectureList	caseSimplify(Conjecture c) Applies a case rewrite step on a specified conjecture.
boolean	caseSimplify(ConjectureList l) Applies a case rewrite step on each conjecture of a specified list.
Object	clone() Creates and returns a copy of this object.
void	compile() Compiles this rewrite system.
boolean	forceHypothesis(ConjectureList l) Applies once hypothesis even if it's not a Rewrite Rule for each conjecture of a specified list.
Conjecture	generalize(Conjecture clause) Applies a generalize step on a specified conjecture.
boolean	generalize(ConjectureList l) Applies the generalize rule on a specified list of conjecture.
ConjectureList	generates(Conjecture c) Applies the generate rule on a specified conjecture.
Conjecture	generates(ConjectureList l) Applies the generate rule on a specified list of conjecture.
boolean	genSplitStep(ConjectureList l) Makes one cycle of spliting method.
boolean	genStep(ConjectureList conj) Make one cycle.
SCList	getAxioms() Returns the list of axioms of the system.
List	getFunctions(Type t) Gets all functions with a specified type of this system.
SCList	getHypotheses() Return the list of axioms of the system.
SCList	getLemmas() Returns the list of lemmas of the system.
String	getPositions() Returns a string representation of all induction positions of functions defined in this system.
List	getSorts() Gets all sorts of this system.
String	getSpecialPosition() Returns a string representation of all special positions of functions defined in this table.
String	getTestSets() Returns a string representation of all test sets of this system.
void	init() Inits rewrite system.
boolean	isMonomorphic() Says if this system is monomorphic.
boolean	isTotology(Conjecture clause) Tests if a specified conjecture is a totology.
Conjecture	normalForm(Conjecture c) Returns the normal form of a specified conjecture.
boolean	oneSplitStep(ConjectureList l) Makes one step of spliting method.
boolean	oneStep(ConjectureList conj) Rewrite list of conjecture.
boolean	pattern(ConjectureList l) Apply pattern splitting on a specified list of conjecture.
ConjectureList	removesEquals(ConjectureList list) Removes equalities that normal form of both sides are equals.
ConjectureList	removesTotology(ConjectureList list) Removes totologies in a specified list of conjectures.
void	setLemmas(SCList l) Sets Lemmas of rewrite system.
void	setTestSet(Type t, NodeList ts) Sets a test set of a speficied type.
void	setTypes() Sets types in whole rewrite system.
SpecialClause	simplify(Conjecture clause) Applies a rewrite step on a specified conjecture.
boolean	simplify(ConjectureList l) Applies a rewrite step on each conjecture of a specified list.
boolean	split(ConjectureList l) Split a specified list of conjecture.
void	splitingMotor(ConjectureList l) Direct spliting motor.
void	textualMotor(ConjectureList l) Direct textual motor.
void	toggles(ConjectureList list) Toggles boolean equalities from conditions to body on each conjecture of a specified list.
String	toString() Returns a string representation of the rewrite system rules.

Methods inherited from class java.lang.Object

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

Field Detail

track

protected String track

stepTrack

protected String stepTrack

genTrack

protected String genTrack

splitTrack

protected String splitTrack

Constructor Detail

RewriteSystem

public RewriteSystem(String name,
                     SCList axioms,
                     IdentTable idt)

Constructor of the rewrite system.

Parameters:

name - name of the system.

axioms - list of axioms of the system.

idt - table of identifiers.

Method Detail

isMonomorphic

public boolean isMonomorphic()

Says if this system is monomorphic.

compile

public void compile()

Compiles this rewrite system. Tries to orient axioms. Computes positions. Set monomorphic property.

setLemmas

public void setLemmas(SCList l)
               throws SemanticException

Sets Lemmas of rewrite system.

Throws:

SemanticException - if one of the lemmas is not weel typed.

getAxioms

public SCList getAxioms()

Returns the list of axioms of the system.

getLemmas

public SCList getLemmas()

Returns the list of lemmas of the system.

getHypotheses

public SCList getHypotheses()

Return the list of axioms of the system.

setTypes

public void setTypes()
              throws SemanticException

Sets types in whole rewrite system.

Throws:

SemanticException - if one of the axioms is not weel typed.

setTestSet

public void setTestSet(Type t,
                       NodeList ts)
                throws SemanticException

Sets a test set of a speficied type. If it is a boolean set, set type property.

Parameters:

t - the type.

ts - the test set.

Throws:

SemanticException - if the test set is not well typed.

isTotology

public boolean isTotology(Conjecture clause)

Tests if a specified conjecture is a totology.

Parameters:

clause - the conjecture.

removesTotology

public ConjectureList removesTotology(ConjectureList list)

Removes totologies in a specified list of conjectures.

Parameters:

list - the list of conjectures.

Returns:

list of removed conjectures (possibly empty)

removesEquals

public ConjectureList removesEquals(ConjectureList list)

Removes equalities that normal form of both sides are equals.

Parameters:

list - the list of conjectures.

Returns:

list of removed conjectures (possibly empty)

toggles

public void toggles(ConjectureList list)

Toggles boolean equalities from conditions to body on each conjecture of a specified list.

Parameters:

l - the list of conjecture.

simplify

public SpecialClause simplify(Conjecture clause)

Applies a rewrite step on a specified conjecture. Tries to find in the oriented rules the definition of functions apparing in the clause. Make one step to normal form.

Parameters:

clause - the conjecture

Returns:

the axiom who simplified the clause - null if none.

simplify

public boolean simplify(ConjectureList l)

Applies a rewrite step on each conjecture of a specified list.

Parameters:

l - the list of conjecture.

Returns:

true if one of these conjecture have been simplified.

forceHypothesis

public boolean forceHypothesis(ConjectureList l)

Applies once hypothesis even if it's not a Rewrite Rule for each conjecture of a specified list.

Parameters:

l - the list of conjecture.

Returns:

true if one of these conjecture have been simplified.

normalForm

public Conjecture normalForm(Conjecture c)

Returns the normal form of a specified conjecture. Applies simplify rule until no more simplification could be done.

Parameters:

clause - the conjecture

caseSimplify

public ConjectureList caseSimplify(Conjecture c)

Applies a case rewrite step on a specified conjecture. Tries to find in the oriented rules the definition of functions apparing in the clause.

Parameters:

c - the conjecture

Returns:

the list of conjectures simplified, null otherwise.

caseSimplify

public boolean caseSimplify(ConjectureList l)

Applies a case rewrite step on each conjecture of a specified list.

Parameters:

l - the list of conjecture.

Returns:

true if one of these conjecture have been simplified.

generates

public ConjectureList generates(Conjecture c)

Applies the generate rule on a specified conjecture. The variables of the conjecture where the generate will apply is chosen with induction positions of functions. These variable(s) will be replaced by Test Set elements.

Parameters:

c - the conjecture

Returns:

the list of generated conjectures, null if there is no more variable in the conjecture.

generates

public Conjecture generates(ConjectureList l)

Applies the generate rule on a specified list of conjecture.

Parameters:

l - the list of conjecture.

Returns:

the conjecture whose have been generated, null if none.

generalize

public Conjecture generalize(Conjecture clause)

Applies a generalize step on a specified conjecture. (Monomorphic System)

Parameters:

clause - the conjecture

Returns:

the generalized clause - null if not possible.

generalize

public boolean generalize(ConjectureList l)

Applies the generalize rule on a specified list of conjecture. (Monomorphic System).

Parameters:

l - the list of conjecture.

Returns:

true if generalize occurs, false otherwise.

split

public boolean split(ConjectureList l)

Split a specified list of conjecture. (Monomorphic System).

Parameters:

l - the list of conjecture.

Returns:

true if split occurs, false otherwise.

pattern

public boolean pattern(ConjectureList l)

Apply pattern splitting on a specified list of conjecture. (Monomorphic System).

Parameters:

l - the list of conjecture.

Returns:

true if patterns can be applied occurs, false otherwise.

oneStep

public boolean oneStep(ConjectureList conj)

Rewrite list of conjecture. Simplify + case simplify. Updates stepTrack.

Parameters:

l - the list of conjecture to rewrite.

Returns:

true if changes occurs, false otherwise.

genStep

public boolean genStep(ConjectureList conj)

Make one cycle. (Remove + rewrite) + forced hypothesis + (Remove + rewrite) + generates. Updates genTrack.

Parameters:

l - the list of conjecture to cycle.

Returns:

true if generates occurs, false otherwise.

oneSplitStep

public boolean oneSplitStep(ConjectureList l)

Makes one step of spliting method. Updates stepTrack. Could be remove, split or pattern use.

Parameters:

l - the list of conjecture to proof.

Returns:

true if changes occurs, false otherwise.

genSplitStep

public boolean genSplitStep(ConjectureList l)

Makes one cycle of spliting method. Updates genTrack. Use as much as possible oneSplitStep, and then generates.

Parameters:

l - the list of conjecture to proof.

Returns:

true if changes occurs, false otherwise.

textualMotor

public void textualMotor(ConjectureList l)

Direct textual motor.

splitingMotor

public void splitingMotor(ConjectureList l)

Direct spliting motor.

init

public void init()

Inits rewrite system. Removes old hypotheses from rules.

toString

public String toString()

Returns a string representation of the rewrite system rules.

Overrides:

toString in class Object

See Also:

Clause, RewriteRule

getPositions

public String getPositions()

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

getTestSets

public String getTestSets()

Returns a string representation of all test sets of this system.

getSpecialPosition

public String getSpecialPosition()

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

getSorts

public List getSorts()

Gets all sorts of this system.

Returns:

a list of Type.

See Also:

IdentTable

getFunctions

public List getFunctions(Type t)

Gets all functions with a specified type of this system.

Parameters:

t - a Type.

Returns:

a list of Function.

See Also:

IdentTable

clone

public Object clone()

Creates and returns a copy of this object.

Overrides:

clone in class Object