Package daikon.simplify

Class Lemma

Object

Lemma

All Implemented Interfaces:

Comparable<Lemma>

Direct Known Subclasses:

InvariantLemma

public class Lemma
extends Object
implements Comparable<Lemma>

A lemma is an object that wraps a Simplify formula representing some logical statement. The only other thing it adds is a short human-readable description, suitable for debugging.

Members of the Lemma class proper represent general theorems, which we give to Simplify as background, with hand-written descriptions.

Field Summary

Fields

Modifier and Type	Field	Description
String	formula
static Lemma[]	lemmas	All the theorems we give Simplify (without proof) to help it reason about predicates, functions, and constants that aren't built-in.
String	summary

Constructor Summary

Constructors

Constructor	Description
Lemma(String summary, String formula)

Method Summary

Modifier and Type	Method	Description
int	compareTo(Lemma other)
@Nullable Class<? extends Invariant>	invClass()	If this lemma came from an invariant, get its class.
static List<Lemma>	lemmasList()	Convenience function to give you lemmas[], but as a vector.
String	summarize()	Return a human-readable description.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

summary

public String summary

formula

public String formula

lemmas

public static Lemma[] lemmas

All the theorems we give Simplify (without proof) to help it reason about predicates, functions, and constants that aren't built-in.

Constructor Detail

Lemma

public Lemma(String summary,
             String formula)

Method Detail

summarize

public String summarize(@GuardSatisfied Lemma this)

Return a human-readable description.

invClass

public @Nullable Class<? extends Invariant> invClass()

If this lemma came from an invariant, get its class.

compareTo

@Pure
public int compareTo(@GuardSatisfied Lemma this,
                     Lemma other)

Specified by:

compareTo in interface Comparable<Lemma>

lemmasList

public static List<Lemma> lemmasList()

Convenience function to give you lemmas[], but as a vector.