Package edu.udel.cis.vsl.sarl.IF.expr

Interface SymbolicConstant

All Superinterfaces:

SymbolicExpression, SymbolicObject

All Known Subinterfaces:

BooleanSymbolicConstant, NumericSymbolicConstant

All Known Implementing Classes:

CnfSymbolicConstant, CommonSymbolicConstant, HerbrandSymbolicConstant, IdealSymbolicConstant

public interface SymbolicConstant
extends SymbolicExpression

A "symbolic constant" is a symbol used in symbolic execution to represent an input value. It is "constant" in the sense that its value does not change in the course of an execution of the program. A symbolic constant is determined by two things: a name (which is a String), and a type (instance of SymbolicType). Two distinct symbolic constants may have the same name, but different types. Two symbolic constants are considered equal iff their names are equal and their types are equal.

Symbolic constants are SymbolicExpressions, which are SymbolicObjects, and like all symbolic objects are immutable.

Nested Class Summary

Nested classes/interfaces inherited from interface edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression

SymbolicExpression.SymbolicOperator

Nested classes/interfaces inherited from interface edu.udel.cis.vsl.sarl.IF.object.SymbolicObject

SymbolicObject.SymbolicObjectKind

Method Summary

Modifier and Type	Method	Description
StringObject	name()	Returns the name of this symbolic constant.
SymbolicType	type()	Returns the type of this symbolic constant.

Methods inherited from interface edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression

argument, atomString, getArguments, getFreeVars, isFalse, isNull, isNumeric, isOne, isTrue, isZero, numArguments, operator, printCompressedTree, size

Methods inherited from interface edu.udel.cis.vsl.sarl.IF.object.SymbolicObject

containsQuantifier, containsSubobject, equals, getOrder, hashCode, id, isCanonic, setInCanonic, setOrder, symbolicObjectKind, toString, toStringBuffer, toStringBufferLong

Method Details

name

StringObject name()

Returns the name of this symbolic constant. This is a StringObject, which wraps a String in a SymbolicObject package.

Returns:

the name of this symbolic constant

type

SymbolicType type()

Returns the type of this symbolic constant.

Specified by:

type in interface SymbolicExpression

Returns:

the type of this symbolic constant