ModSort

Value Members

1. final def !=(arg0: Any): Boolean

   

   Definition Classes

   AnyRef → Any

2. final def ##(): Int

   

   Definition Classes

   AnyRef → Any

3. final def ==(arg0: Any): Boolean

   

   Definition Classes

   AnyRef → Any

4. def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

   

   Higher-order syntax for universal quantifiers.

   Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c, d, e) => phi(a, b, c, d, e)).

   Definition Classes

   Sort

5. def all(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

   

   Higher-order syntax for universal quantifiers.

   Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c, d) => phi(a, b, c, d)).

   Definition Classes

   Sort

6. def all(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

   

   Higher-order syntax for universal quantifiers.

   Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c) => phi(a, b, c)).

   Definition Classes

   Sort

7. def all(f: (ITerm, ITerm) ⇒ IFormula): IFormula

   

   Higher-order syntax for universal quantifiers.

   Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b) => phi(a, b)).

   Definition Classes

   Sort

8. def all(f: (ITerm) ⇒ IFormula): IFormula

   

   Higher-order syntax for universal quantifiers.

   Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all(a => phi(a)).

   Definition Classes

   Sort

9. def all(f: IFormula): ISortedQuantified

   

   Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

   Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

   Definition Classes

   Sort

10. final def asInstanceOf[T0]: T0

    

    Definition Classes

    Any

11. val asTerm: Decoder[Option[ITerm]]

    

    Extract a term representation of some value in the sort.

    Extract a term representation of some value in the sort.

    Definition Classes

    Sort

12. def augmentModelTermSet(model: Conjunction, assignment: Map[(IdealInt, Sort), ITerm], allTerms: Set[(IdealInt, Sort)], definedTerms: Set[(IdealInt, Sort)]): Unit

    

    Extract constructor terms from a model.

    Extract constructor terms from a model. Such terms will always be encoded as integers, and integers can have different meaning depending on the considered sort. Each sort can add the terms representing a model to the assignment map. Alternatively, a sort can add indexes to the definedTerms set to indicate a particular index is defined by a model, but the corresponding constructor term is not available yet because it refers to other terms that are not yet available.

    Definition Classes

    ProxySort → Sort

13. def boundVariable(index: Int): IVariable

    

    The variable with given de Bruijn index and this sort.

    The variable with given de Bruijn index and this sort.

    Definition Classes

    Sort

14. val cardinality: Option[IdealInt]

    

    The cardinality of sorts with fixed-size, finite domain.

    The cardinality of sorts with fixed-size, finite domain.

    Definition Classes

    ProxySort → Sort

15. def clone(): AnyRef

    

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

16. def decodeToTerm(d: IdealInt, assignment: Map[(IdealInt, Sort), ITerm]): Option[ITerm]

    

    Extract a term representation of some value in the sort.

    Extract a term representation of some value in the sort. This method can be overwritten in sub-classes to decode in a sort-specific way

    Definition Classes

    ModSort → ProxySort → Sort

17. def eps(f: (ITerm) ⇒ IFormula): ISortedEpsilon

    

    Higher-order syntax for epsilon-expressions.

    Higher-order syntax for epsilon-expressions. This makes it possible to write things like Sort.eps(a => phi(a)).

    Definition Classes

    Sort

18. def eps(f: IFormula): ISortedEpsilon

    

    Generate an epsilon-expression.

    Generate an epsilon-expression.

    Definition Classes

    Sort

19. final def eq(arg0: AnyRef): Boolean

    

    Definition Classes

    AnyRef

20. def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c, d, e) => phi(a, b, c, d, e)).

    Definition Classes

    Sort

21. def ex(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c, d) => phi(a, b, c, d)).

    Definition Classes

    Sort

22. def ex(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c) => phi(a, b, c)).

    Definition Classes

    Sort

23. def ex(f: (ITerm, ITerm) ⇒ IFormula): IFormula

    

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b) => phi(a, b)).

    Definition Classes

    Sort

24. def ex(f: (ITerm) ⇒ IFormula): IFormula

    

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex(a => phi(a)).

    Definition Classes

    Sort

25. def ex(f: IFormula): ISortedQuantified

    

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Definition Classes

    Sort

26. def finalize(): Unit

    

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

27. final def getClass(): Class[_]

    

    Definition Classes

    AnyRef → Any

28. def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]

    

    Attributes

    protected

    Definition Classes

    Sort

29. val individuals: Stream[ITerm]

    

    Terms representing elements of the sort.

    Terms representing elements of the sort.

    Definition Classes

    ModSort → ProxySort → Sort

30. final def isInstanceOf[T0]: Boolean

    

    Definition Classes

    Any

31. val lower: IdealInt

    

32. def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

    

    Constraints defining the range of the sort.

    Constraints defining the range of the sort.

    Definition Classes

    ProxySort → Sort

33. val modulus: IdealInt

    

34. val name: String

    

    Definition Classes

    ModSort → ProxySort → Sort

35. final def ne(arg0: AnyRef): Boolean

    

    Definition Classes

    AnyRef

36. def newConstant(name: String): ConstantTerm

    

    Allocation of a new constant with this sort.

    Allocation of a new constant with this sort.

    Definition Classes

    Sort

37. final def notify(): Unit

    

    Definition Classes

    AnyRef

38. final def notifyAll(): Unit

    

    Definition Classes

    AnyRef

39. final def synchronized[T0](arg0: ⇒ T0): T0

    

    Definition Classes

    AnyRef

40. def toString(): String

    

    Definition Classes

    Sort → AnyRef → Any

41. val upper: IdealInt

    

42. final def wait(): Unit

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

43. final def wait(arg0: Long, arg1: Int): Unit

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

44. final def wait(arg0: Long): Unit

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

45. def witness: Option[ITerm]

    

    A witness term proving that the sort is inhabited.

    A witness term proving that the sort is inhabited.

    Definition Classes

    Sort