Class AlgSimp

java.lang.Object
  extended byRules
      extended byAlgSimp

class AlgSimp
extends Rules

Eine Instanz von AlgSimp stellt eine Reihe algebraischer 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 algebraischen Regel:
Muster: int(_X) + int(_Y)
Vereinfachungsmuster: int(_Z)
Bedingung: _X + _Y = _Z

Passt die zu untersuchende Verifikationsbedingung auf das "Muster" und ist die "Bedingung" erfüllt, wird sie zum "Vereinfachungsmuster" vereinfacht. In obigem Beispiel ist die Bedingung immer erfüllt, denn es sind nur die Zahlen "_X" und "_Y" zu addieren, was auf Grund des passenden "Musters" immer möglich ist.
Eine Beschreibung der verschiedenen Typen der Regeln findet sich in der Hilfe zur Klasse "SimpRule".

See Also:
SimpRule, SimpleNode

Constructor Summary
AlgSimp(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

AlgSimp

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

Parameters:
manual - Die boolean Variable fragt ab, ob manuell oder automatisch bewiesen wird.
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