Class

ap.theories.strings.AbstractStringTheoryWithSort

AbstractStringSort

Related Doc: package AbstractStringTheoryWithSort

Permalink

class AbstractStringSort extends ProxySort

Sort for strings that will reconstruct terms with the help of the str_empty and str_cons functions.

Linear Supertypes
ProxySort, Sort, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. AbstractStringSort
  2. ProxySort
  3. Sort
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new AbstractStringSort()

    Permalink

Value Members

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

    Permalink
    Definition Classes
    AnyRef → Any

  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any

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

    Permalink
    Definition Classes
    AnyRef → Any

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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink
    Definition Classes
    Any

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

    Permalink

    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, terms: Map[(IdealInt, Sort), ITerm], allTerms: Set[(IdealInt, Sort)], definedTerms: Set[(IdealInt, Sort)]): Unit

    Permalink

    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
    AbstractStringSort → ProxySort → Sort

  13. def boundVariable(index: Int): IVariable

    Permalink

    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]

    Permalink

    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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

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

    Permalink

    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
    AbstractStringSort → ProxySort → Sort

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

    Permalink

    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

    Permalink

    Generate an epsilon-expression.

    Generate an epsilon-expression.

    Definition Classes
    Sort

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

    Permalink
    Definition Classes
    AnyRef

  20. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

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

    Permalink

    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

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

    Permalink

    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

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

    Permalink

    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

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

    Permalink

    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

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

    Permalink

    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

  26. def ex(f: IFormula): ISortedQuantified

    Permalink

    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

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

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

    Permalink
    Attributes
    protected
    Definition Classes
    Sort

  29. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  30. lazy val individuals: Stream[ITerm]

    Permalink

    Terms representing elements of the sort.

    Terms representing elements of the sort.

    Definition Classes
    AbstractStringSort → ProxySort → Sort

  31. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

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

    Permalink

    Constraints defining the range of the sort.

    Constraints defining the range of the sort.

    Definition Classes
    ProxySort → Sort

  33. val name: String

    Permalink
    Definition Classes
    AbstractStringSort → ProxySort → Sort

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

    Permalink
    Definition Classes
    AnyRef

  35. def newConstant(name: String): ConstantTerm

    Permalink

    Allocation of a new constant with this sort.

    Allocation of a new constant with this sort.

    Definition Classes
    Sort

  36. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  37. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  38. def setTheory(_theory: AbstractStringTheoryWithSort): Unit

    Permalink
    Attributes
    protected[ap.theories.strings]

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

    Permalink
    Definition Classes
    AnyRef

  40. def toString(): String

    Permalink
    Definition Classes
    Sort → AnyRef → Any

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  43. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  44. def witness: Option[ITerm]

    Permalink

    A witness term proving that the sort is inhabited.

    A witness term proving that the sort is inhabited.

    Definition Classes
    Sort

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from ProxySort

Inherited from Sort

Inherited from AnyRef

Inherited from Any

Ungrouped