Package org.sosy_lab.java_smt

Enum ResProofRule.ResAxiom

java.lang.Object

java.lang.Enum<ResProofRule.ResAxiom>

org.sosy_lab.java_smt.ResProofRule.ResAxiom

All Implemented Interfaces:

Serializable, Comparable<ResProofRule.ResAxiom>, ProofRule

Enclosing class:

ResProofRule

public static enum ResProofRule.ResAxiom
extends Enum<ResProofRule.ResAxiom>
implements ProofRule

Any operation that proves a term.

Enum Constant Summary

Enum Constants

Enum Constant	Description
ABS_DEF
AND_NEGATIVE
AND_POSITIVE
ASSUME
CONGRUENCE
CONST
DEL
DISTINCT_NEGATIVE
DISTINCT_POSITIVE
DIV_DEF
DIV_HIGH
DIV_LOW
DIVISIBLE_DEF
DT_ACYCLIC
DT_CONS
DT_EXHAUST
DT_MATCH
DT_PROJECT
DT_TEST_CONS
DT_TEST_CONS_PRIME
EQUAL_NEGATIVE1
EQUAL_NEGATIVE2
EQUAL_POSITIVE1
EQUAL_POSITIVE2
EQUALITY_NEGATIVE
EQUALITY_POSITIVE
EXISTS_NEGATIVE
EXISTS_POSITIVE
EXPAND
EXPAND_IS_INT
EXTDIFF
FALSE_NEGATIVE
FARKAS
FORALL_NEGATIVE
FORALL_POSITIVE
GE_DEF
GT_DEF
IMPLIES_NEGATIVE
IMPLIES_POSITIVE
ITE1
ITE2
MOD_DEF
NEG_DEF
NEG_DEF2
NOT_NEGATIVE
NOT_POSITIVE
OR_NEGATIVE
OR_POSITIVE
POLY_ADD
POLY_MUL
REFLEXIVITY
RESOLUTION
SELECTSTORE1
SELECTSTORE2
SYMMETRY
TO_INT_HIGH
TO_INT_LOW
TO_REAL
TOTAL
TOTAL_INT
TRANSITIVITY
TRICHOTOMY
TRUE_POSITIVE
XOR_NEGATIVE
XOR_POSITIVE

Method Summary

Modifier and Type	Method	Description
String	getFormula()	Get the formula of the proof rule.
String	getName()	Get the name of the proof rule.
static ResProofRule.ResAxiom	valueOf(String name)	Returns the enum constant of this type with the specified name.
static ResProofRule.ResAxiom[]	values()	Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum

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

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Detail

RESOLUTION

public static final ResProofRule.ResAxiom RESOLUTION

ASSUME

public static final ResProofRule.ResAxiom ASSUME

TRUE_POSITIVE

public static final ResProofRule.ResAxiom TRUE_POSITIVE

FALSE_NEGATIVE

public static final ResProofRule.ResAxiom FALSE_NEGATIVE

NOT_POSITIVE

public static final ResProofRule.ResAxiom NOT_POSITIVE

NOT_NEGATIVE

public static final ResProofRule.ResAxiom NOT_NEGATIVE

AND_POSITIVE

public static final ResProofRule.ResAxiom AND_POSITIVE

AND_NEGATIVE

public static final ResProofRule.ResAxiom AND_NEGATIVE

OR_POSITIVE

public static final ResProofRule.ResAxiom OR_POSITIVE

OR_NEGATIVE

public static final ResProofRule.ResAxiom OR_NEGATIVE

IMPLIES_POSITIVE

public static final ResProofRule.ResAxiom IMPLIES_POSITIVE

IMPLIES_NEGATIVE

public static final ResProofRule.ResAxiom IMPLIES_NEGATIVE

EQUAL_POSITIVE1

public static final ResProofRule.ResAxiom EQUAL_POSITIVE1

EQUAL_NEGATIVE1

public static final ResProofRule.ResAxiom EQUAL_NEGATIVE1

EQUAL_POSITIVE2

public static final ResProofRule.ResAxiom EQUAL_POSITIVE2

EQUAL_NEGATIVE2

public static final ResProofRule.ResAxiom EQUAL_NEGATIVE2

XOR_POSITIVE

public static final ResProofRule.ResAxiom XOR_POSITIVE

XOR_NEGATIVE

public static final ResProofRule.ResAxiom XOR_NEGATIVE

FORALL_POSITIVE

public static final ResProofRule.ResAxiom FORALL_POSITIVE

FORALL_NEGATIVE

public static final ResProofRule.ResAxiom FORALL_NEGATIVE

EXISTS_POSITIVE

public static final ResProofRule.ResAxiom EXISTS_POSITIVE

EXISTS_NEGATIVE

public static final ResProofRule.ResAxiom EXISTS_NEGATIVE

REFLEXIVITY

public static final ResProofRule.ResAxiom REFLEXIVITY

SYMMETRY

public static final ResProofRule.ResAxiom SYMMETRY

TRANSITIVITY

public static final ResProofRule.ResAxiom TRANSITIVITY

CONGRUENCE

public static final ResProofRule.ResAxiom CONGRUENCE

EQUALITY_POSITIVE

public static final ResProofRule.ResAxiom EQUALITY_POSITIVE

EQUALITY_NEGATIVE

public static final ResProofRule.ResAxiom EQUALITY_NEGATIVE

DISTINCT_POSITIVE

public static final ResProofRule.ResAxiom DISTINCT_POSITIVE

DISTINCT_NEGATIVE

public static final ResProofRule.ResAxiom DISTINCT_NEGATIVE

ITE1

public static final ResProofRule.ResAxiom ITE1

ITE2

public static final ResProofRule.ResAxiom ITE2

DEL

public static final ResProofRule.ResAxiom DEL

EXPAND

public static final ResProofRule.ResAxiom EXPAND

SELECTSTORE1

public static final ResProofRule.ResAxiom SELECTSTORE1

SELECTSTORE2

public static final ResProofRule.ResAxiom SELECTSTORE2

EXTDIFF

public static final ResProofRule.ResAxiom EXTDIFF

CONST

public static final ResProofRule.ResAxiom CONST

POLY_ADD

public static final ResProofRule.ResAxiom POLY_ADD

POLY_MUL

public static final ResProofRule.ResAxiom POLY_MUL

TO_REAL

public static final ResProofRule.ResAxiom TO_REAL

FARKAS

public static final ResProofRule.ResAxiom FARKAS

TRICHOTOMY

public static final ResProofRule.ResAxiom TRICHOTOMY

TOTAL

public static final ResProofRule.ResAxiom TOTAL

GT_DEF

public static final ResProofRule.ResAxiom GT_DEF

GE_DEF

public static final ResProofRule.ResAxiom GE_DEF

DIV_DEF

public static final ResProofRule.ResAxiom DIV_DEF

NEG_DEF

public static final ResProofRule.ResAxiom NEG_DEF

NEG_DEF2

public static final ResProofRule.ResAxiom NEG_DEF2

ABS_DEF

public static final ResProofRule.ResAxiom ABS_DEF

TOTAL_INT

public static final ResProofRule.ResAxiom TOTAL_INT

TO_INT_LOW

public static final ResProofRule.ResAxiom TO_INT_LOW

TO_INT_HIGH

public static final ResProofRule.ResAxiom TO_INT_HIGH

DIV_LOW

public static final ResProofRule.ResAxiom DIV_LOW

DIV_HIGH

public static final ResProofRule.ResAxiom DIV_HIGH

MOD_DEF

public static final ResProofRule.ResAxiom MOD_DEF

DIVISIBLE_DEF

public static final ResProofRule.ResAxiom DIVISIBLE_DEF

EXPAND_IS_INT

public static final ResProofRule.ResAxiom EXPAND_IS_INT

DT_PROJECT

public static final ResProofRule.ResAxiom DT_PROJECT

DT_CONS

public static final ResProofRule.ResAxiom DT_CONS

DT_TEST_CONS

public static final ResProofRule.ResAxiom DT_TEST_CONS

DT_TEST_CONS_PRIME

public static final ResProofRule.ResAxiom DT_TEST_CONS_PRIME

DT_EXHAUST

public static final ResProofRule.ResAxiom DT_EXHAUST

DT_ACYCLIC

public static final ResProofRule.ResAxiom DT_ACYCLIC

DT_MATCH

public static final ResProofRule.ResAxiom DT_MATCH

Method Detail

values

public static ResProofRule.ResAxiom[] 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 (ResProofRule.ResAxiom c : ResProofRule.ResAxiom.values())
    System.out.println(c);

Returns:

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

valueOf

public static ResProofRule.ResAxiom valueOf(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:

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

NullPointerException - if the argument is null

getName

public String getName()

Description copied from interface: ProofRule

Get the name of the proof rule.

Specified by:

getName in interface ProofRule

getFormula

public String getFormula()

Description copied from interface: ProofRule

Get the formula of the proof rule.

Specified by:

getFormula in interface ProofRule