public class OverflowChecker
extends java.lang.Object
Constructor and Description |
---|
OverflowChecker(SMTSort intsort) |
Modifier and Type | Method and Description |
---|---|
SMTTerm |
addGuardIfNecessary(SMTTerm t)
Adds a guard for the given term if that term may overflow.
|
java.util.List<SMTTerm> |
createGuards(java.util.Set<SMTTerm> terms)
Creates guards for the given terms
|
void |
processTerm(SMTTerm t)
Recursively adds overflow guards for non ground terms if necessary.
|
void |
searchArithGroundTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub)
Searches for arithmetical ground terms in sub and stores them in terms
|
void |
searchArithTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars,
java.util.List<SMTTermVariable> bind)
Searches for non ground terms in sub, and stores them in terms.
|
public OverflowChecker(SMTSort intsort)
public java.util.List<SMTTerm> createGuards(java.util.Set<SMTTerm> terms)
terms
- - the terms that must be guarded against integer overflowspublic SMTTerm addGuardIfNecessary(SMTTerm t)
t
- public void processTerm(SMTTerm t)
t
- public void searchArithTerms(java.util.Set<SMTTerm> terms, SMTTerm sub, java.util.Set<SMTTermVariable> universalVars, java.util.Set<SMTTermVariable> existentialVars, java.util.List<SMTTermVariable> bind)
terms
- list where the terms are storedsub
- the term to be searcheduniversalVars
- universal variablesexistentialVars
- existential variablesbind
- variables bounded by the current quantifierCopyright © 2003-2019 The KeY-Project.