public class OverflowChecker
extends java.lang.Object
Constructor and Description |
---|
OverflowChecker(SMTSort intsort) |
Modifier and Type | Method and Description |
---|---|
private boolean |
acceptableTerm(SMTTermMultOp tm,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars,
java.util.List<SMTTermVariable> bind) |
SMTTerm |
addGuardIfNecessary(SMTTerm t)
Adds a guard for the given term if that term may overflow.
|
private SMTTerm |
addGuardIfNecessary(SMTTerm t,
java.util.Set<SMTTermVariable> quantifiedVars)
Constructs a guarded term, if overflows are possible, otherwise returns the original term.
|
private void |
classifySubs(java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTerm> subs,
java.util.Set<SMTTerm> universalSubs,
java.util.Set<SMTTerm> existentialSubs) |
private boolean |
containsVars(SMTTerm term) |
private SMTTerm |
createGuard(java.util.Set<SMTTerm> terms) |
private SMTTerm |
createGuardForAdd(SMTTermMultOp t) |
private SMTTerm |
createGuardForMul(SMTTermMultOp t) |
java.util.List<SMTTerm> |
createGuards(java.util.Set<SMTTerm> terms)
Creates guards for the given terms
|
private SMTTerm |
doubleBitsize(SMTTerm t) |
private void |
getSubTerms(SMTTerm t,
java.util.Set<SMTTerm> result) |
private void |
getVariables(SMTTerm term,
java.util.Set<SMTTerm> vars) |
private SMTTerm |
increaseBitsize(SMTTerm t) |
private boolean |
isAddOp(SMTTermMultOp.Op op) |
private boolean |
isArithmeticOperator(SMTTermMultOp.Op op) |
private boolean |
isComparisonOp(SMTTermMultOp.Op op) |
private boolean |
isMulOp(SMTTermMultOp.Op op) |
private boolean |
isUniversalSub(SMTTerm t,
java.util.Set<SMTTermVariable> universalVars) |
private int |
max() |
private int |
min() |
void |
processTerm(SMTTerm t)
Recursively adds overflow guards for non ground terms if necessary.
|
private void |
processTerm(SMTTerm t,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars) |
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.
|
private SMTSort intsort
public OverflowChecker(SMTSort intsort)
private int max()
private int min()
private SMTTerm createGuardForAdd(SMTTermMultOp t)
private SMTTerm createGuardForMul(SMTTermMultOp t)
public java.util.List<SMTTerm> createGuards(java.util.Set<SMTTerm> terms)
terms
- - the terms that must be guarded against integer overflowsprivate boolean isArithmeticOperator(SMTTermMultOp.Op op)
private boolean isAddOp(SMTTermMultOp.Op op)
private boolean isMulOp(SMTTermMultOp.Op op)
private boolean isComparisonOp(SMTTermMultOp.Op op)
public SMTTerm addGuardIfNecessary(SMTTerm t)
t
- private SMTTerm addGuardIfNecessary(SMTTerm t, java.util.Set<SMTTermVariable> quantifiedVars)
t
- quantifiedVars
- public void processTerm(SMTTerm t)
t
- private void processTerm(SMTTerm t, java.util.Set<SMTTermVariable> universalVars, java.util.Set<SMTTermVariable> existentialVars)
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 quantifierpublic void searchArithGroundTerms(java.util.Set<SMTTerm> terms, SMTTerm sub)
terms
- sub
- private boolean acceptableTerm(SMTTermMultOp tm, java.util.Set<SMTTermVariable> universalVars, java.util.Set<SMTTermVariable> existentialVars, java.util.List<SMTTermVariable> bind)
private boolean containsVars(SMTTerm term)
private void classifySubs(java.util.Set<SMTTermVariable> universalVars, java.util.Set<SMTTerm> subs, java.util.Set<SMTTerm> universalSubs, java.util.Set<SMTTerm> existentialSubs)
universalVars
- subs
- universalSubs
- existentialSubs
- private boolean isUniversalSub(SMTTerm t, java.util.Set<SMTTermVariable> universalVars)