Class OrdSimp

java.lang.Object
  extended byRules
      extended byOrdSimp

class OrdSimp
extends Rules

Eine Instanz von OrdSimp stellt eine Reihe relationaler 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 relationalen Regel:
Muster: int(_X) < int(_Y)
Vereinfachungsmuster: true
Bedingung: _X < _Y

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 erfüllt, wenn die ganze Zahl "_X" kleiner als die ganze Zahl "_Y" ist. Der Vergleich ist möglich auf Grund des passenden "Musters".
Eine Beschreibung der verschiedenen Typen der Regeln findet sich in der Hilfe zur Klasse "SimpRule".

See Also:
SimpRule, SimpleNode

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

OrdSimp

public OrdSimp(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