Object
- LemmaStack

All Implemented Interfaces:

Closeable, AutoCloseable
```
public class LemmaStack
extends Object
implements Closeable
```
A stack of Lemmas that shadows the stack of assumptions that Simplify keeps. Keeping this stack is necessary if we're to be able to restart Simplify from where we left off after it hangs, but it's also a convenient place to hang routines that any Simplify client can use.

Field Summary

Fields
Modifier and Type	Field	Description
`static boolean`	`dkconfig_print_contradictions`	Boolean.
`static boolean`	`dkconfig_remove_contradictions`	Boolean.
`static boolean`	`dkconfig_synchronous_errors`	Boolean.
`static long`	`SMALL_INTEGER`	Integers smaller in absolute value than this will be printed directly.

Constructor Summary

Constructors
Constructor Description

LemmaStack()
Create a new LemmaStack.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`char`	`checkForContradiction()`	Ask Simplify whether the assumptions we've pushed so far are contradictory.
`char`	`checkLemma(Lemma lemma)`	Ask Simplify whether a lemma is valid, given our assumptions.
`void`	`clear()`	Blow away everything on our stack and Simplify's.
`static void`	`clearInts()`
`void`	`close()`	Releases resources held by this.
`void`	`dumpLemmas(PrintStream out)`	Dump the state of the stack to a file, for debugging manually in Simplify.
`int`	`markLevel()`	Return a reference to the current position on the lemma stack.
`List<Set<Class<? extends Invariant>>>`	`minimizeClasses(String result)`
`List<Lemma>`	`minimizeContradiction()`	Return a set of contradictory assumptions from the stack (as a vector of Lemmas) which are minimal in the sense that no proper subset of them are contradictory as far as Simplify can tell.
`List<Lemma>`	`minimizeProof(Lemma lem)`	Return a set of assumptions from the stack (as a vector of Lemmas) that imply the given Lemma and which are minimal in the sense that no proper subset of them imply it as far as Simplify can tell.
`static void`	`noticeInt(long i)`	Keep track that we've seen this number in formulas, for the sake of pushOrdering.
`void`	`popLemma()`	Pop a lemma from our and Simplify's stacks.
`void`	`popToMark(int mark)`	Pop off lemmas from the stack until its level matches mark.
`static void`	`printLemmas(PrintStream out, List<Lemma> v)`	Convenience method to print a vector of lemmas, in both their human-readable and Simplify forms.
`boolean`	`pushLemma(Lemma lem)`	Push an assumption onto our and Simplify's stacks.
`void`	`pushLemmas(List<Lemma> newLemmas)`	Push a vector of assumptions onto our and Simplify's stacks.
`void`	`pushOrdering()`	For all the integers we've seen, tell Simplify about the ordering between them.
`void`	`removeContradiction()`	Remove some lemmas from the stack, such that our set of assumptions is no longer contradictory.
`void`	`removeLemma(Lemma bad)`	Search for the given lemma in the stack, and then remove it from both our stack and Simplify's.

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

- Field Detail
  - dkconfig_remove_contradictions
```
public static boolean dkconfig_remove_contradictions
```
    Boolean. Controls Daikon's response when inconsistent invariants are discovered while running Simplify. If false, Daikon will give up on using Simplify for that program point. If true, Daikon will try to find a small subset of the invariants that cause the contradiction and avoid them, to allow processing to continue. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual.
  - dkconfig_print_contradictions
```
public static boolean dkconfig_print_contradictions
```
    Boolean. Controls Daikon's response when inconsistent invariants are discovered while running Simplify. If true, Daikon will print an error message to the standard error stream listing the contradictory invariants. This is mainly intended for debugging Daikon itself, but can sometimes be helpful in tracing down other problems. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual.
  - dkconfig_synchronous_errors
```
public static boolean dkconfig_synchronous_errors
```
    Boolean. If true, ask Simplify to check a simple proposition after each assumption is pushed, providing an opportunity to wait for output from Simplify and potentially receive error messages about the assumption. When false, long sequences of assumptions may be pushed in a row, so that by the time an error message arrives, it's not clear which input caused the error. Of course, Daikon's input to Simplify isn't supposed to cause errors, so this option should only be needed for debugging.
  - SMALL_INTEGER
```
public static final long SMALL_INTEGER
```
    Integers smaller in absolute value than this will be printed directly. Larger integers will be printed abstractly (see Invariant.simplify_format_long and a comment there for details).
    
    See Also:
    
    Constant Field Values
- Constructor Detail
  - LemmaStack
```
public LemmaStack()
           throws SimplifyError
```
    Create a new LemmaStack.
    
    Throws:
    
    SimplifyError
- Method Detail
  - popLemma
```
public void popLemma()
```
    Pop a lemma from our and Simplify's stacks.
  - pushLemma
```
public boolean pushLemma(@UnknownInitialization(LemmaStack.class) LemmaStack this,
                         Lemma lem)
                  throws SimplifyError
```
    Push an assumption onto our and Simplify's stacks.
    
    Parameters:
    
    lem - the assumption
    
    Returns:
    
    true if success, false if Simplify times out
    
    Throws:
    
    SimplifyError
  - pushLemmas
```
public void pushLemmas(@UnknownInitialization(LemmaStack.class) LemmaStack this,
                       List<Lemma> newLemmas)
                throws SimplifyError
```
    Push a vector of assumptions onto our and Simplify's stacks.
    
    Throws:
    
    SimplifyError
  - checkLemma
```
public char checkLemma(Lemma lemma)
                throws SimplifyError
```
    Ask Simplify whether a lemma is valid, given our assumptions. Returns 'T' if Simplify says yes, 'F' if Simplify says no, or '?' if we have to kill Simplify because it won't answer.
    
    Throws:
    
    SimplifyError
  - checkForContradiction
```
public char checkForContradiction()
                           throws SimplifyError
```
    Ask Simplify whether the assumptions we've pushed so far are contradictory. Returns 'T' if Simplify says yes, 'F' if Simplify says no, or '?' if we have to kill Simplify because it won't answer.
    
    Throws:
    
    SimplifyError
  - minimizeClasses
```
public List<Set<Class<? extends Invariant>>> minimizeClasses(String result)
```
  - minimizeContradiction
```
public List<Lemma> minimizeContradiction()
                                  throws SimplifyError
```
    Return a set of contradictory assumptions from the stack (as a vector of Lemmas) which are minimal in the sense that no proper subset of them are contradictory as far as Simplify can tell.
    
    Throws:
    
    SimplifyError
  - minimizeProof
```
public List<Lemma> minimizeProof(Lemma lem)
                          throws SimplifyError
```
    Return a set of assumptions from the stack (as a vector of Lemmas) that imply the given Lemma and which are minimal in the sense that no proper subset of them imply it as far as Simplify can tell.
    
    Throws:
    
    SimplifyError
  - removeContradiction
```
public void removeContradiction()
                         throws SimplifyError
```
    Remove some lemmas from the stack, such that our set of assumptions is no longer contradictory. This is not a very principled thing to do, but it's better than just giving up. The approach is relatively slow, trying not to remove too many lemmas.
    
    Throws:
    
    SimplifyError
  - removeLemma
```
public void removeLemma(Lemma bad)
                 throws SimplifyError
```
    Search for the given lemma in the stack, and then remove it from both our stack and Simplify's. This is rather inefficient.
    
    Throws:
    
    SimplifyError
  - clear
```
public void clear()
```
    Blow away everything on our stack and Simplify's.
  - markLevel
```
public int markLevel()
```
    Return a reference to the current position on the lemma stack. If, after pushing some stuff, you want to get back here, pass the mark to popToMark(). This will only work if you use these routines in a stack-disciplined way, of course. In particular, beware that removeContradiction() invalidates marks, since it can remove a lemma from anywhere on the stack.
  - popToMark
```
public void popToMark(int mark)
```
    Pop off lemmas from the stack until its level matches mark.
  - printLemmas
```
public static void printLemmas(PrintStream out,
                               List<Lemma> v)
```
    Convenience method to print a vector of lemmas, in both their human-readable and Simplify forms.
  - dumpLemmas
```
public void dumpLemmas(PrintStream out)
```
    Dump the state of the stack to a file, for debugging manually in Simplify.
  - noticeInt
```
public static void noticeInt(long i)
```
    Keep track that we've seen this number in formulas, for the sake of pushOrdering.
  - clearInts
```
public static void clearInts()
```
  - pushOrdering
```
public void pushOrdering()
                  throws SimplifyError
```
    For all the integers we've seen, tell Simplify about the ordering between them.
    
    Throws:
    
    SimplifyError
  - close
```
public void close(@GuardSatisfied LemmaStack this)
```
    Releases resources held by this.
    
    Specified by:
    
    close in interface AutoCloseable
    
    Specified by:
    
    close in interface Closeable

Class LemmaStack

Field Summary

Constructor Summary

Method Summary

Methods inherited from class Object

Field Detail

dkconfig_remove_contradictions

dkconfig_print_contradictions

dkconfig_synchronous_errors

SMALL_INTEGER

Constructor Detail

LemmaStack

Method Detail

popLemma

pushLemma

pushLemmas

checkLemma

checkForContradiction

minimizeClasses

minimizeContradiction

minimizeProof

removeContradiction

removeLemma

clear

markLevel

popToMark

printLemmas

dumpLemmas

noticeInt

clearInts

pushOrdering

close