|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectRules
BoolSimp
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".
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 |
public BoolSimp(boolean manual)
manual
- Die boolean Variable zeigt, ob manuell oder automatisch bewiesen wird. BoolRewriter
Method Detail |
public int getNumberOfRules()
getNumberOfRules
in class Rules
public SimpleNode getPattern(int i)
getPattern
in class Rules
public SimpleNode getSimpPattern(int i)
getSimpPattern
in class Rules
public SimpleNode getCondPattern(int i)
getCondPattern
in class Rules
public boolean hasCondPattern(int i)
hasCondPattern
in class Rules
public short getCondType(int i)
getCondType
in class Rules
SimpRule
public java.lang.String getIdNameOfSimplifiedCondPattern(int i)
getIdNameOfSimplifiedCondPattern
in class Rules
|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |