object Sort
- Alphabetic
- By Inheritance
- Sort
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val AnySort: ProxySort
A placeholder sort that is used in places where the sort has not been inferred yet.
- lazy val Bool: ADTProxySort
The sort of Booleans.
The sort of Booleans. Booleans are encoded as an ADT with two nullary constructors
true(mapped to the integer0),false(mapped to the integer1).- See also
ap.theories.ADT.BoolADT
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def createInfUninterpretedSort(name: String): InfUninterpretedSort
Create a new uninterpreted sort of infinite cardinality.
- def createUninterpretedSort(name: String): UninterpretedSort
Create a new uninterpreted sort of finite or infinite cardinality.
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def individualsVectors(sorts: List[Sort]): Stream[List[ITerm]]
Generate a stream of vectors of individuals in the given sort vector.
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def sortOf(t: ITerm): Sort
Determine the sort of the given term.
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- object :::
Extractor to identify terms with associated sort.
Extractor to identify terms with associated sort. This can be used for checks like
t match { case t ::: Sort.Bool => XXX }. - object AnyBool
Extractor to recognise sorts that represent the Booleans.
- object Integer extends Sort
The sort of integers, which is also the default sort whenever no sort is specified.
- object MultipleValueBool extends ProxySort
The sort of integers reinterpreted as Booleans.
The sort of integers reinterpreted as Booleans. Integer
0true, every non-zero number asfalse. For symbolic representation the same terms as in sortBoolare used.- See also
ap.theories.ADT.BoolADT
Bool
- object Nat extends ProxySort
The sort of natural numbers.
- object NonNumeric
Extractor to recognise non-numeric sorts.
- object NonNumericTerm
- object Numeric
Extractor to recognise sorts that are subsets of the integers.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)