Class BoolRewriter

java.lang.Object
  extended byBoolRewriter

class BoolRewriter
extends java.lang.Object

Ein BoolRewriter schreibt einen booleschen Ausdruck der Form "id(~V) == _E ==> _B" so um, dass der Identifier "~V" im Ausdruck "_B" durch "_E" ersetzt wird.


Constructor Summary
BoolRewriter(SimpleNode condition, ListOfSubstitutions theta)
          Erzeugt einen BoolRewriter für einen booleschen Ausdruck.
 
Method Summary
 SimpleNode isDefined(SimpleNode node)
          Prüft, unter welchen Bedingungen ein algebraischer Ausdruck wohldefiniert ist.
 ListOfSubstitutions rewrite()
          Ersetzt im Baum bExprNode den Identifier vNode durch den Ausdruck exprNode.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

BoolRewriter

public BoolRewriter(SimpleNode condition,
                    ListOfSubstitutions theta)
Erzeugt einen BoolRewriter für einen booleschen Ausdruck.

Parameters:
condition - Umzuschreibender boolescher Ausdruck.
theta - Liste der beim Unifizieren erzeugten Substitutionen.
Method Detail

rewrite

public ListOfSubstitutions rewrite()
Ersetzt im Baum bExprNode den Identifier vNode durch den Ausdruck exprNode.
Benötigt einen Occur-Check.

Returns:
Die Substitutionen zum Umschreiben der condition. Ergebnis des Umschreibens: _C ==> _D
See Also:
SimpleNode.notOccur(String nodeName)

isDefined

public SimpleNode isDefined(SimpleNode node)
Prüft, unter welchen Bedingungen ein algebraischer Ausdruck wohldefiniert ist.
Eine Bedingung, welche entstehen kann, ist beispielsweis dass eine Zahl, durch die geteilt wird, ungleich Null ist. Die Methode erzeugt einen booleschen Ausdruck, der noch vereinfacht werden muss.

Parameters:
node - Zu prüfender algebraischer Ausdruck.
Returns:
Der boolesche Ausdruck für die Überprüfung der Wohldefiniertheit.