InvariantLemma

Object
- Lemma
- - InvariantLemma

All Implemented Interfaces:

Comparable<Lemma>
```
public class InvariantLemma
extends Lemma
```
InvariantLemmas are Lemmas created by printing a Daikon invariant in Simplify format, sometimes with some hacks.

Field Summary

Fields
Modifier and Type Field Description

String from

Invariant invariant
- Fields inherited from class Lemma
  formula, lemmas, summary

Constructor Summary

Constructors
Constructor Description

InvariantLemma(Invariant inv)

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`Class<? extends Invariant>`	`invClass()`	If this lemma came from an invariant, get its class.
`static InvariantLemma`	`makeLemmaAddOrig(Invariant inv)`	Make a lemma corresponding to the given invariant, except referring to the prestate versions of all the variables that inv referred to.
`String`	`summarize()`	Return a human-readable description.

Methods inherited from class Lemma
compareTo, lemmasList

Methods inherited from class Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - from
```
public String from
```
  - invariant
```
public Invariant invariant
```
- Constructor Detail
  - InvariantLemma
```
public InvariantLemma(Invariant inv)
```
- Method Detail
  - summarize
```
public String summarize(@GuardSatisfied InvariantLemma this)
```
    Description copied from class: Lemma
    
    Return a human-readable description.
    
    Overrides:
    
    summarize in class Lemma
  - invClass
```
public Class<? extends Invariant> invClass()
```
    If this lemma came from an invariant, get its class.
    
    Overrides:
    
    invClass in class Lemma
  - makeLemmaAddOrig
```
public static InvariantLemma makeLemmaAddOrig(Invariant inv)
```
    Make a lemma corresponding to the given invariant, except referring to the prestate versions of all the variables that inv referred to.