Package de.uzl.its.swat.symbolic.value.primitive.numeric

Class NumericalValue<T extends org.sosy_lab.java_smt.api.Formula,K>

java.lang.Object

de.uzl.its.swat.symbolic.value.Value<T,K>

de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue<T,K>

Type Parameters:

T - The type of Formula used by this Value

K - The class wrapper around the primitive datatype this value represents

Direct Known Subclasses:

BooleanValue, ByteValue, CharValue, DoubleValue, FloatValue, IntValue, LongValue, ShortValue

public abstract class NumericalValue<T extends org.sosy_lab.java_smt.api.Formula,K>
extends Value<T,K>

Field Summary

Fields

Modifier and Type	Field	Description
protected org.sosy_lab.java_smt.api.IntegerFormulaManager	imgr	Java-smt formula manager for handling integral formulas

Fields inherited from class de.uzl.its.swat.symbolic.value.Value

concrete, context, formula, inc, name, symbol

Constructor Summary

Constructors

Constructor	Description
NumericalValue()

Method Summary

Modifier and Type	Method	Description
String	genericToString(String type)
protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	wrapByte(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)	Models short overflow in constraints
protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	wrapCharacter(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)	Models short overflow in constraints
protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	wrapInteger(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)	Models int overflow in constraints
protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	wrapLong(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)	Models long overflow in constraints
protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	wrapShort(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)	Models short overflow in constraints

Methods inherited from class de.uzl.its.swat.symbolic.value.Value

asBooleanValue, asByteValue, asCharValue, asDoubleValue, asFloatValue, asIntValue, asLongValue, asNumericalValue, asObjectValue, asShortValue, asStringValue, getBounds, getConcrete, getConcreteEncoded, getName, getType, initSymbolic, initSymbolic, MAKE_SYMBOLIC, MAKE_SYMBOLIC, MAKE_SYMBOLIC, reset, toString

Methods inherited from class java.lang.Object

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

Field Details

imgr

protected org.sosy_lab.java_smt.api.IntegerFormulaManager imgr

Java-smt formula manager for handling integral formulas

Constructor Details

NumericalValue

public NumericalValue()

Method Details

wrapInteger

protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula wrapInteger(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)

Models int overflow in constraints

Parameters:

i - The formula to wrap

Returns:

The wrapped formula

wrapLong

protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula wrapLong(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)

Models long overflow in constraints

Parameters:

i - The formula to wrapLong

Returns:

The wrapped formula

wrapShort

protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula wrapShort(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)

Models short overflow in constraints

Parameters:

i - The formula to wrap

Returns:

The wrapped formula

wrapByte

protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula wrapByte(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)

Models short overflow in constraints

Parameters:

i - The formula to wrap

Returns:

The wrapped formula

wrapCharacter

protected org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula wrapCharacter(org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula i)

Models short overflow in constraints

Parameters:

i - The formula to wrap

Returns:

The wrapped formula

genericToString

public String genericToString(String type)