Class BoolSimp

java.lang.Object
  extended byRules
      extended byBoolSimp

class BoolSimp
extends Rules

Eine Instanz von BoolSimp stellt eine Reihe boolescher Regeln zum Vereinfachen einer beliebigen Verifikationsbedingung bereit. Eine solche Regel besteht im Allgemeinen (je nach Typ) aus einem Muster, einem Vereinfachungsmuster und einer Bedingung, jeweils in Form eines Baumes (ein Objekt vom Typ SimpleNode), zusammengefasst zu einem Objekt vom Typ SimpRule.

Ein Beispiel einer booleschen Regel:
Muster: _X & _Z ==> _Y
Vereinfachungsmuster: true
Bedingung: _X ==> _Y vereinfacht zu true

Passt die zu untersuchende Verifikationsbedingung auf das "Muster" und ist die "Bedingung" erfüllt, wird sie zum "Vereinfachungsmuster" vereinfacht. In obigem Beispiel muss zum Testen der Bedingung versucht werden, "_X ==> _Y" mit den aus dem Unifizieren mit dem "Muster" entstandenen Belegungen für "_X" und "_Y" zu "true" zu vereinfachen.
Eine Beschreibung der verschiedenen Typen der Regeln findet sich in der Hilfe zur Klasse "SimpRule".

See Also:
SimpRule, SimpleNode

Constructor Summary
BoolSimp(boolean manual)
          Erzeugt die Regeln und füllt damit das Feld "rules".
 
Method Summary
 SimpleNode getCondPattern(int i)
          Liefert die "Bedingung" der i-ten Regel.
 short getCondType(int i)
          Liefert den Typ der i-ten Regel.
 java.lang.String getIdNameOfSimplifiedCondPattern(int i)
          Liefert den Bezeichner der freien Variablen in der "Bedingung" der i-ten Regel.
 int getNumberOfRules()
          Liefert die Anzahl der Vereinfachungsregeln.
 SimpleNode getPattern(int i)
          Liefert das "Muster" der i-ten Regel.
 SimpleNode getSimpPattern(int i)
          Liefert das "Vereinfachungsmuster" der i-ten Regel.
 boolean hasCondPattern(int i)
          Überprüft, ob die i-te Regel eine "Bedingung" benötigt.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

BoolSimp

public BoolSimp(boolean manual)
Erzeugt die Regeln und füllt damit das Feld "rules".

Parameters:
manual - Die boolean Variable zeigt, ob manuell oder automatisch bewiesen wird.
Die erste Regel, die erzeugt wird, dient zur Kontrolle, ob sie mit einem "BoolRewriter" umgeschrieben werden kann.
See Also:
BoolRewriter
Method Detail

getNumberOfRules

public int getNumberOfRules()
Liefert die Anzahl der Vereinfachungsregeln.

Specified by:
getNumberOfRules in class Rules

getPattern

public SimpleNode getPattern(int i)
Liefert das "Muster" der i-ten Regel.

Specified by:
getPattern in class Rules

getSimpPattern

public SimpleNode getSimpPattern(int i)
Liefert das "Vereinfachungsmuster" der i-ten Regel.

Specified by:
getSimpPattern in class Rules

getCondPattern

public SimpleNode getCondPattern(int i)
Liefert die "Bedingung" der i-ten Regel.

Specified by:
getCondPattern in class Rules

hasCondPattern

public boolean hasCondPattern(int i)
Überprüft, ob die i-te Regel eine "Bedingung" benötigt.

Specified by:
hasCondPattern in class Rules

getCondType

public short getCondType(int i)
Liefert den Typ der i-ten Regel.
Beschreibung der Typen: siehe SimpRule

Specified by:
getCondType in class Rules
See Also:
SimpRule

getIdNameOfSimplifiedCondPattern

public java.lang.String getIdNameOfSimplifiedCondPattern(int i)
Liefert den Bezeichner der freien Variablen in der "Bedingung" der i-ten Regel.

Specified by:
getIdNameOfSimplifiedCondPattern in class Rules