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

Class BooleanValue

java.lang.Object

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

de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue

public class BooleanValue
extends NumericalValue<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Wrapper to represent boolean values on the symbolic stack. Can contain concrete and symbolic information.

Field Summary

Fields inherited from class de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue

imgr

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

concrete, context, formula, inc, name, symbol

Constructor Summary

Constructors

Constructor	Description
BooleanValue(org.sosy_lab.java_smt.api.SolverContext context, boolean concrete)	Creates a new BooleanValue that has no prior symbolic information and only contains a specific value
BooleanValue(org.sosy_lab.java_smt.api.SolverContext context, boolean concrete, org.sosy_lab.java_smt.api.BooleanFormula formula)	Creates a new BooleanValue that has prior symbolic information and contains a specific value

Method Summary

Modifier and Type	Method	Description
BooleanValue	asBooleanValue()
IntValue	asIntValue()
NumericalValue<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>	asNumericalValue()
StringValue	asStringValue()
org.sosy_lab.java_smt.api.BooleanFormula	getBounds(boolean upper)	Creates a formula that asserts that this symbolic value is withing the bounds of this type
String	getConcreteEncoded()
String	MAKE_SYMBOLIC()	Turns this BooleanValue into a symbolic variable
String	MAKE_SYMBOLIC(long idx)	Turns this IntValue into a symbolic variable
String	MAKE_SYMBOLIC(String namePrefix)	Turns this BooleanValue into a symbolic variable
String	toString()	Returns the string representation of the value used to visualize the stack.

Methods inherited from class de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue

genericToString, wrapByte, wrapCharacter, wrapInteger, wrapLong, wrapShort

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

asByteValue, asCharValue, asDoubleValue, asFloatValue, asLongValue, asObjectValue, asShortValue, getConcrete, getName, getType, initSymbolic, initSymbolic, reset

Methods inherited from class java.lang.Object

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

Constructor Details

BooleanValue

public BooleanValue(org.sosy_lab.java_smt.api.SolverContext context,
 boolean concrete)

Creates a new BooleanValue that has no prior symbolic information and only contains a specific value

Parameters:

context - The SolverContext

concrete - The concrete boolean value

BooleanValue

public BooleanValue(org.sosy_lab.java_smt.api.SolverContext context,
 boolean concrete,
 org.sosy_lab.java_smt.api.BooleanFormula formula)

Creates a new BooleanValue that has prior symbolic information and contains a specific value

Parameters:

context - The SolverContext

concrete - The concrete boolean value

formula - The symbolic formula representing prior symbolic information about this boolean

Method Details

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(String namePrefix)

Turns this BooleanValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Parameters:

namePrefix -

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC()

Turns this BooleanValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(long idx)

Turns this IntValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Parameters:

idx -

Returns:

The numerical identifier of this symbolic variable

asNumericalValue

public NumericalValue<org.sosy_lab.java_smt.api.BooleanFormula,Boolean> asNumericalValue()

Overrides:

asNumericalValue in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

getBounds

public org.sosy_lab.java_smt.api.BooleanFormula getBounds(boolean upper)

Creates a formula that asserts that this symbolic value is withing the bounds of this type

Overrides:

getBounds in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Parameters:

upper - If the upper or lower bound should be created

Returns:

The BooleanFormula that represents the bounds check

asIntValue

public IntValue asIntValue()

Overrides:

asIntValue in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

asBooleanValue

public BooleanValue asBooleanValue()

Overrides:

asBooleanValue in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

asStringValue

public StringValue asStringValue()

Overrides:

asStringValue in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

getConcreteEncoded

public String getConcreteEncoded()

Overrides:

getConcreteEncoded in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

toString

public String toString()

Returns the string representation of the value used to visualize the stack. The representation is not complete.

Overrides:

toString in class Value<org.sosy_lab.java_smt.api.BooleanFormula,Boolean>

Returns:

the string representation of the value.