fmrisc.ProgramExplorer.Judgements

Enum Simplification.Tag

java.lang.Object

java.lang.Enum<Simplification.Tag>

fmrisc.ProgramExplorer.Judgements.Simplification.Tag

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<Simplification.Tag>

Enclosing class:

Simplification

public static enum Simplification.Tag
extends java.lang.Enum<Simplification.Tag>

The following simplifications are implemented: o Some "quasi-normalization": (A /\ B) /\ C to A /\ (B /\ C) (A \/ B) \/ C to A \/ (B \/ C) A imp (B imp C) to (A /\ B) imp C This simplifies pretty-printing and further processing. o Pulling negation inside ~~A to A ~(A /\ B) to ~A \/ ~B ~(A \/ B) to ~A /\ ~B ~(A imp B) to A /\ ~B ~(A equiv B) to A xor B ~(A xor B) to A equiv B ~(FORALL x: A) to EXISTS x: ~A ~(EXISTS x: A) to FORALL x: ~A ~(LET ... in A) to LET ... in ~A) ~(x=a) to x /= a, ~(x/=a) to x=a ~(x leq a) to x gt a, ~(x lt a) to x geq a ~(x leq a) to x lt a, ~(x gt a) to x leq a As a consequence, negation can appear only at the level of atomic predicates and IF-THEN-ELSE (for which there is no convenient simplification). o Removing superfluous quantifiers (Q x: A) to A, if x not free in A (let x=... in A) to A, if x not free in A (FORALL x: x=T imp A) to A[T/x], if x occurs at most once in A (EXISTS x: x=T /\ A) to A[T/x], if x occurs at most once in A (let x=T in A) to A[T/x], if x occurs at most once in A o Pulling quantifiers outside Conjunction and disjunction: (FORALL x: A) /\ B to (FORALL y: A[y/x] /\ B) y not free in A or B (if possible, choose y=x to avoid substitution) The same for \/ instead of /\. The same for EXISTS instead of FORALL. The same for both sides switched. Above rule is overridden by: (FORALL x: A) /\ (FORALL y: B) to (FORALL z: A[z/x] /\ B[z/x]) (EXISTS x: A) \/ (EXISTS y: B) to (EXISTS z: A[z/x] \/ B[z/x]) z not free in A or B (if possible, choose z in {x,y} to avoid one substitution) Implication: (FORALL x: A) imp B to (EXISTS y: A[y/x] imp B) (EXISTS x: A) imp B to (FORALL y: A[y/x] imp B) A imp (FORALL x: B) to (FORALL y: A imp B[y/x]) A imp (EXISTS x: B) to (EXISTS y: A imp B[y/x]) No convenient rules for equiv, XOR, IF. Future ideas (not yet implemented): o Sort defining (in)equalities in topological dependence order y = ..x.. /\ x = ... to x = ... /\ y = ..x..

Enum Constant Summary

Enum Constants

Enum Constant and Description
AND
ARRAYTERM
EQUALS
EXISTS
FORALL
GREATER
GREATEREQUAL
IMPLIES
LAMBDAFORMULA
LAMBDATERM
LESS
LESSEQUAL
NOTEQUALS
OR
SIMILAR

Method Summary

Modifier and Type	Method and Description
static Simplification.Tag	valueOf(java.lang.String name) Returns the enum constant of this type with the specified name.
static Simplification.Tag[]	values() Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum

compareTo, equals, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Detail

AND

public static final Simplification.Tag AND

OR

public static final Simplification.Tag OR

IMPLIES

public static final Simplification.Tag IMPLIES

FORALL

public static final Simplification.Tag FORALL

EXISTS

public static final Simplification.Tag EXISTS

ARRAYTERM

public static final Simplification.Tag ARRAYTERM

LAMBDATERM

public static final Simplification.Tag LAMBDATERM

LAMBDAFORMULA

public static final Simplification.Tag LAMBDAFORMULA

EQUALS

public static final Simplification.Tag EQUALS

NOTEQUALS

public static final Simplification.Tag NOTEQUALS

LESS

public static final Simplification.Tag LESS

LESSEQUAL

public static final Simplification.Tag LESSEQUAL

GREATER

public static final Simplification.Tag GREATER

GREATEREQUAL

public static final Simplification.Tag GREATEREQUAL

SIMILAR

public static final Simplification.Tag SIMILAR

Method Detail

values

public static Simplification.Tag[] values()

Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:

for (Simplification.Tag c : Simplification.Tag.values())
    System.out.println(c);

Returns:

an array containing the constants of this enum type, in the order they are declared

valueOf

public static Simplification.Tag valueOf(java.lang.String name)

Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)

Parameters:

name - the name of the enum constant to be returned.

Returns:

the enum constant with the specified name

Throws:

java.lang.IllegalArgumentException - if this enum type has no constant with the specified name

java.lang.NullPointerException - if the argument is null