de.uka.ilkd.key.smt

Class OverflowChecker

java.lang.Object

de.uka.ilkd.key.smt.OverflowChecker

public class OverflowChecker
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private SMTSort	intsort

Constructor Summary

Constructors

Constructor and Description
OverflowChecker(SMTSort intsort)

Method Summary

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.

Methods inherited from class java.lang.Object

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

Field Detail

intsort

private SMTSort intsort

Constructor Detail

OverflowChecker

public OverflowChecker(SMTSort intsort)

Method Detail

max

private int max()

min

private int min()

increaseBitsize

private SMTTerm increaseBitsize(SMTTerm t)

doubleBitsize

private SMTTerm doubleBitsize(SMTTerm t)

createGuardForAdd

private SMTTerm createGuardForAdd(SMTTermMultOp t)

createGuardForMul

private SMTTerm createGuardForMul(SMTTermMultOp t)

getSubTerms

private void getSubTerms(SMTTerm t,
                         java.util.Set<SMTTerm> result)

createGuard

private SMTTerm createGuard(java.util.Set<SMTTerm> terms)

createGuards

public java.util.List<SMTTerm> createGuards(java.util.Set<SMTTerm> terms)

Creates guards for the given terms

Parameters:

terms - - the terms that must be guarded against integer overflows

Returns:

a list of generated guards

isArithmeticOperator

private boolean isArithmeticOperator(SMTTermMultOp.Op op)

isAddOp

private boolean isAddOp(SMTTermMultOp.Op op)

isMulOp

private boolean isMulOp(SMTTermMultOp.Op op)

isComparisonOp

private boolean isComparisonOp(SMTTermMultOp.Op op)

addGuardIfNecessary

public SMTTerm addGuardIfNecessary(SMTTerm t)

Adds a guard for the given term if that term may overflow.

Parameters:

t -

Returns:

addGuardIfNecessary

private SMTTerm addGuardIfNecessary(SMTTerm t,
                                    java.util.Set<SMTTermVariable> quantifiedVars)

Constructs a guarded term, if overflows are possible, otherwise returns the original term.

Parameters:

t -

quantifiedVars -

Returns:

processTerm

public void processTerm(SMTTerm t)

Recursively adds overflow guards for non ground terms if necessary.

Parameters:

t -

processTerm

private void processTerm(SMTTerm t,
                         java.util.Set<SMTTermVariable> universalVars,
                         java.util.Set<SMTTermVariable> existentialVars)

searchArithTerms

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)

Searches for non ground terms in sub, and stores them in terms. Begin with empty lists.

Parameters:

terms - list where the terms are stored

sub - the term to be searched

universalVars - universal variables

existentialVars - existential variables

bind - variables bounded by the current quantifier

searchArithGroundTerms

public void searchArithGroundTerms(java.util.Set<SMTTerm> terms,
                                   SMTTerm sub)

Searches for arithmetical ground terms in sub and stores them in terms

Parameters:

terms -

sub -

acceptableTerm

private boolean acceptableTerm(SMTTermMultOp tm,
                               java.util.Set<SMTTermVariable> universalVars,
                               java.util.Set<SMTTermVariable> existentialVars,
                               java.util.List<SMTTermVariable> bind)

getVariables

private void getVariables(SMTTerm term,
                          java.util.Set<SMTTerm> vars)

containsVars

private boolean containsVars(SMTTerm term)

classifySubs

private void classifySubs(java.util.Set<SMTTermVariable> universalVars,
                          java.util.Set<SMTTerm> subs,
                          java.util.Set<SMTTerm> universalSubs,
                          java.util.Set<SMTTerm> existentialSubs)

Parameters:

universalVars -

subs -

universalSubs -

existentialSubs -

isUniversalSub

private boolean isUniversalSub(SMTTerm t,
                               java.util.Set<SMTTermVariable> universalVars)