Module dev.civl.sarl

Package dev.civl.sarl.IF.type

Interface SymbolicUninterpretedType

All Superinterfaces:

SymbolicObject, SymbolicType

public interface SymbolicUninterpretedType
extends SymbolicType

This class represents uninterpreted types. Objects of an uninterpreted type cannot participate any operations except for EQUALS, NOT_EQUALS and APPLY.

An uninterpreted type is defined by a name. Two uninterpreted types who have the same name are identical, otherwise, they are different types. Objects of different uninterpreted types cannot be compared.

An concrete expression of an uninterpreted type is indexed by a concrete integral key. Two objects of the same uninterpreted type are identical if and only if they have the exact same key.

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.sarl.IF.object.SymbolicObject

SymbolicObject.SymbolicObjectKind

Nested classes/interfaces inherited from interface dev.civl.sarl.IF.type.SymbolicType

SymbolicType.SymbolicTypeKind

Method Summary

Modifier and Type	Method	Description
StringObject	name()
Function<SymbolicExpression,IntObject>	soleSelector()

Methods inherited from interface dev.civl.sarl.IF.object.SymbolicObject

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

Methods inherited from interface dev.civl.sarl.IF.type.SymbolicType

isBoolean, isChar, isHerbrand, isIdeal, isInteger, isNumeric, isReal, typeKind

Method Details

name

StringObject name()

Returns:

the name of this uninterpreted type.

soleSelector

Function<SymbolicExpression,IntObject> soleSelector()

Returns:

an operator which is an instance of

invalid reference

Function<T,R>

. The key of an symbolic expression of an uninterpreted type can be obtained by applying the operator to the symbolic expression.