Class/Object

ap.theories.strings

SeqStringTheory

Related Docs: object SeqStringTheory | package strings

Permalink

class SeqStringTheory extends AbstractStringTheory

String theory implemented using a list ADT.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SeqStringTheory
  2. AbstractStringTheory
  3. StringTheory
  4. Theory
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class DecoderData(m: Map[IdealInt, Seq[IdealInt]]) extends TheoryDecoderData with Product with Serializable

    Permalink
  2. class IllegalRegexException extends Exception

    Permalink
    Definition Classes
    AbstractStringTheory
  3. class RegexExtractor extends AnyRef

    Permalink

    Translator from atoms representing regexes in a goal to the corresponding term.

    Translator from atoms representing regexes in a goal to the corresponding term.

    Definition Classes
    AbstractStringTheory
  4. class RichWord extends AnyRef

    Permalink

    Helper class providing string infix operators

    Helper class providing string infix operators

    Definition Classes
    StringTheory
  5. class WordExtractor extends AnyRef

    Permalink
    Definition Classes
    AbstractStringTheory

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. val CharSort: ModSort

    Permalink

    Sort representing characters

    Sort representing characters

    Definition Classes
    SeqStringTheoryStringTheory
  5. object ConcreteRegex

    Permalink

    Extractor to identify regular expressions that are completely defined, i.e., in which no sub-terms are left symbolic.

    Extractor to identify regular expressions that are completely defined, i.e., in which no sub-terms are left symbolic.

    Definition Classes
    AbstractStringTheory
  6. object RegexExtractor

    Permalink
    Definition Classes
    AbstractStringTheory
  7. val RegexSort: InfUninterpretedSort

    Permalink

    Sort representing regular expressions

    Sort representing regular expressions

    Definition Classes
    SeqStringTheoryStringTheory
  8. val StringSort: ADTProxySort

    Permalink

    Sort representing strings

    Sort representing strings

    Definition Classes
    SeqStringTheoryStringTheory
  9. object WordExtractor

    Permalink
    Definition Classes
    AbstractStringTheory
  10. val _str_++: Predicate

    Permalink

    The predicate corresponding to str_++

    The predicate corresponding to str_++

    Definition Classes
    SeqStringTheoryStringTheory
  11. val _str_cons: Predicate

    Permalink

    The predicate corresponding to str_cons

    The predicate corresponding to str_cons

    Definition Classes
    SeqStringTheoryStringTheory
  12. val _str_empty: Predicate

    Permalink

    The predicate corresponding to str_empty

    The predicate corresponding to str_empty

    Definition Classes
    SeqStringTheoryStringTheory
  13. val allAxioms: IFormula

    Permalink
  14. val alphabetSize: Int

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  15. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  16. val asString: Decoder[String]

    Permalink

    Translate a numeric value from a model to a string.

    Translate a numeric value from a model to a string.

    Definition Classes
    SeqStringTheoryStringTheory
  17. val asStringPartial: Decoder[Option[String]]

    Permalink

    Translate a numeric value from a model to a string.

    Translate a numeric value from a model to a string.

    Definition Classes
    SeqStringTheoryStringTheory
  18. def assignStringValues(facts: Conjunction, assignment: Map[Term, Seq[Int]], order: TermOrder): Conjunction

    Permalink

    Augment goal facts with the given assignment of strings to terms.

    Augment goal facts with the given assignment of strings to terms. At the moment this assumes that all string terms are constants.

    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  19. val axioms: Conjunction

    Permalink

    Axioms defining the theory; such axioms are simply added as formulae to the problem to be proven, and thus handled using the standard reasoning techniques (including e-matching).

    Axioms defining the theory; such axioms are simply added as formulae to the problem to be proven, and thus handled using the standard reasoning techniques (including e-matching).

    Definition Classes
    SeqStringTheoryTheory
  20. val axioms1: Formula

    Permalink
  21. def breakCyclicEquations(goal: Goal): Option[Seq[Action]]

    Permalink

    Check for cyclic word equations induced by str_++ or str_cons, and break those.

    Check for cyclic word equations induced by str_++ or str_cons, and break those. e.g., equations x = yz & y = ax -> z = eps & a = eps & y = ax Tarjan's algorithm is used to find all strongly connected components

    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  22. def char2Int(t: ITerm): ITerm

    Permalink

    Convert a character term to an integer term

    Convert a character term to an integer term

    Definition Classes
    SeqStringTheoryStringTheory
  23. val char_is_digit: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  24. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )
  25. val dependencies: Iterable[Theory]

    Permalink

    Optionally, other theories that this theory depends on.

    Optionally, other theories that this theory depends on. Specified dependencies will be loaded before this theory, but the preprocessors of the dependencies will be called after the preprocessor of this theory.

    Definition Classes
    SeqStringTheoryTheory
  26. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  27. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  28. def evalFun(f: IFunApp): Option[ITerm]

    Permalink

    Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

    Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

    Definition Classes
    Theory
  29. def evalPred(p: IAtom): Option[Boolean]

    Permalink

    Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

    Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

    Definition Classes
    Theory
  30. def extend(order: TermOrder): TermOrder

    Permalink

    Add the symbols defined by this theory to the order

    Add the symbols defined by this theory to the order

    Definition Classes
    Theory
  31. val extraIndexedOps: Map[(String, Int), Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  32. val extraOps: Map[String, Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  33. val funPredMap: Map[IFunction, Predicate]

    Permalink
  34. val funPredicates: Seq[Predicate]

    Permalink
  35. val functionPredicateMapping: List[(MonoSortedIFunction, Predicate)]

    Permalink

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Definition Classes
    SeqStringTheoryTheory
  36. val functionalPredicates: Set[Predicate]

    Permalink

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Definition Classes
    SeqStringTheoryTheory
  37. val functions: List[MonoSortedIFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    SeqStringTheoryTheory
  38. def generateDecoderData(model: Conjunction): Option[TheoryDecoderData]

    Permalink

    If this theory defines any Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.

    If this theory defines any Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.

    Definition Classes
    SeqStringTheoryTheory
  39. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  40. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  41. def iPostprocess(f: IFormula, signature: Signature): IFormula

    Permalink

    Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

    Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination. This method will be applied to the formula after calling Internal2Inputabsy.

    Definition Classes
    Theory
  42. def iPreprocess(f: IFormula, signature: Signature): (IFormula, Signature)

    Permalink

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover. This method will be applied very early in the translation process.

    Definition Classes
    SeqStringTheoryTheory
  43. def int2Char(t: ITerm): ITerm

    Permalink

    Convert an integer term to a character term

    Convert an integer term to a character term

    Definition Classes
    SeqStringTheoryStringTheory
  44. def int2String(t: ITerm): ITerm

    Permalink

    Convert an integer term to a singleton string

    Convert an integer term to a singleton string

    Definition Classes
    StringTheory
  45. val intToStrAxioms: IFormula

    Permalink
  46. val int_to_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  47. val int_to_str_help: MonoSortedIFunction

    Permalink
  48. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  49. def isSoundForSat(theories: Seq[Theory], config: Theory.SatSoundnessConfig.Value): Boolean

    Permalink

    Check whether we can tell that the given combination of theories is sound for checking satisfiability of a problem, i.e., if proof construction ends up in a dead end, can it be concluded that a problem is satisfiable.

    Check whether we can tell that the given combination of theories is sound for checking satisfiability of a problem, i.e., if proof construction ends up in a dead end, can it be concluded that a problem is satisfiable.

    Definition Classes
    SeqStringTheoryTheory
  50. val modelGenPredicates: Set[Predicate]

    Permalink

    Optionally, a set of predicates used by the theory to tell the PresburgerModelFinder about terms that will be handled exclusively by this theory.

    Optionally, a set of predicates used by the theory to tell the PresburgerModelFinder about terms that will be handled exclusively by this theory. If a proof goal in model generation mode contains an atom p(x), for p in this set, then the PresburgerModelFinder will ignore x when assigning concrete values to symbols.

    Definition Classes
    Theory
  51. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  52. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  53. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  54. val order: TermOrder

    Permalink
  55. def plugin: Some[Plugin]

    Permalink

    Optionally, a plug-in implementing reasoning in this theory

    Optionally, a plug-in implementing reasoning in this theory

    Definition Classes
    SeqStringTheoryTheory
  56. def postSimplifiers: Seq[(IExpression) ⇒ IExpression]

    Permalink

    Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier.

    Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier. Such simplifiers are invoked by with ap.parser.Simplifier.

    Definition Classes
    Theory
  57. def postprocess(f: Conjunction, order: TermOrder): Conjunction

    Permalink

    Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

    Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination. This method will be applied to the raw formulas, before calling Internal2Inputabsy.

    Definition Classes
    Theory
  58. def predefFunctions: List[MonoSortedIFunction]

    Permalink
    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  59. def predefPredicates: List[MonoSortedPredicate]

    Permalink
    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  60. val predicateMatchConfig: PredicateMatchConfig

    Permalink

    Information how interpreted predicates should be handled for e-matching.

    Information how interpreted predicates should be handled for e-matching.

    Definition Classes
    SeqStringTheoryTheory
  61. val predicates: List[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    SeqStringTheoryTheory
  62. def preprocess(f: Conjunction, order: TermOrder): Conjunction

    Permalink

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Definition Classes
    SeqStringTheoryTheory
  63. val reDerivativeAxioms: IFormula

    Permalink
  64. val reDerivativeAxioms2: Formula

    Permalink
  65. val reMatchingAxioms: IFormula

    Permalink
  66. val reMatchingAxioms2: Formula

    Permalink
  67. val reNullableAxioms: IFormula

    Permalink
  68. val reSimpAxioms: IFormula

    Permalink
  69. val re_*: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  70. val re_+: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  71. val re_++: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  72. val re_all: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  73. val re_allchar: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  74. val re_charrange: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  75. val re_comp: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  76. val re_derivative_help: MonoSortedIFunction

    Permalink
  77. val re_diff: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  78. val re_eps: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  79. val re_from_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  80. val re_inter: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  81. val re_loop: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  82. val re_matches_str_help: MonoSortedIFunction

    Permalink
  83. val re_none: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  84. val re_nullable_help: MonoSortedIFunction

    Permalink
  85. val re_opt: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  86. val re_range: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  87. val re_union: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  88. val reducerPlugin: ReducerPluginFactory

    Permalink

    Optionally, a plugin for the reducer applied to formulas both before and during proving.

    Optionally, a plugin for the reducer applied to formulas both before and during proving.

    Definition Classes
    Theory
  89. val seqADT: ADT

    Permalink
  90. val singleInstantiationPredicates: Set[Predicate]

    Permalink

    When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

    When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

    Definition Classes
    Theory
  91. val strAtAxioms: IFormula

    Permalink
  92. val strIndexofAxioms: IFormula

    Permalink
  93. val strReplaceAxioms: IFormula

    Permalink
  94. val strSubstrAxioms: IFormula

    Permalink
  95. val strToIntAxioms: IFormula

    Permalink
  96. val str_++: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  97. val str_<=: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  98. val str_at: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  99. val str_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  100. val str_cons: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  101. val str_contains: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  102. val str_empty: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  103. val str_from_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  104. val str_from_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  105. val str_head: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  106. val str_head_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  107. val str_in_re: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  108. val str_indexof: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  109. val str_indexof_help: MonoSortedIFunction

    Permalink
  110. val str_len: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  111. val str_prefixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  112. val str_replace: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  113. val str_replaceall: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  114. val str_replaceallre: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  115. val str_replacere: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  116. val str_substr: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  117. val str_suffixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  118. val str_tail: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  119. val str_to_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  120. val str_to_int: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  121. val str_to_int_help: MonoSortedIFunction

    Permalink
  122. val str_to_re: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  123. implicit def string2Term(str: String): ITerm

    Permalink

    Convert a string to a term

    Convert a string to a term

    Definition Classes
    StringTheory
  124. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  125. implicit def term2RichWord(t: ITerm): RichWord

    Permalink

    Convert a term to a rich term, providing some infix operators

    Convert a term to a rich term, providing some infix operators

    Definition Classes
    StringTheory
  126. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  127. val totalityAxioms: Conjunction

    Permalink

    Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

    Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

    Definition Classes
    SeqStringTheoryTheory
  128. val triggerRelevantFunctions: Set[IFunction]

    Permalink

    A list of functions that should be considered in automatic trigger generation

    A list of functions that should be considered in automatic trigger generation

    Definition Classes
    SeqStringTheoryTheory
  129. val upperBound: IdealInt

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  131. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  132. final def wait(): Unit

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

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 AbstractStringTheory

Inherited from StringTheory

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped