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
    Definition Classes
    StringTheory
  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 alphabetSize: Int

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

    Permalink
    Definition Classes
    Any
  15. 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
    StringTheory
  16. 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
    StringTheory
  17. 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
  18. val axioms: Formula

    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
  19. 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
  20. 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
  21. val char_is_digit: MonoSortedPredicate

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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  23. 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
  24. final def eq(arg0: AnyRef): Boolean

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

    Permalink
    Definition Classes
    AnyRef → Any
  26. 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
  27. 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
  28. 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
  29. val extraOps: Map[String, Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  30. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  31. val funPredMap: Map[IFunction, Predicate]

    Permalink
  32. val funPredicates: Seq[Predicate]

    Permalink
  33. 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
  34. 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
  35. val functions: List[MonoSortedIFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    SeqStringTheoryTheory
  36. 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
    StringTheoryTheory
  37. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  38. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  39. 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
  40. 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
  41. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  42. 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
  43. final def ne(arg0: AnyRef): Boolean

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

    Permalink
    Definition Classes
    AnyRef
  45. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  46. 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
  47. def predefFunctions: List[MonoSortedIFunction]

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

    Permalink
    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  49. 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
  50. val predicates: List[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    SeqStringTheoryTheory
  51. 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
  52. val re_*: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  53. val re_+: MonoSortedIFunction

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  55. val re_all: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  56. val re_allchar: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  57. val re_charrange: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  58. val re_comp: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  59. val re_eps: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  60. val re_from_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  61. val re_inter: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  62. val re_loop: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  63. val re_none: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  64. val re_opt: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  65. val re_range: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  66. val re_union: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  67. 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
  68. val seqADT: ADT

    Permalink
  69. 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
  70. val str: MonoSortedIFunction

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

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  73. val str_at: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  74. val str_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  75. val str_cons: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  76. val str_contains: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  77. val str_empty: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  78. val str_from_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  79. val str_head: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  80. val str_head_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  81. val str_in_re: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  82. val str_indexof: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  83. val str_len: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  84. val str_prefixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  85. val str_replace: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  86. val str_replaceall: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  87. val str_replaceallre: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  88. val str_replacere: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  89. val str_substr: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  90. val str_suffixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  91. val str_tail: MonoSortedIFunction

    Permalink
    Definition Classes
    SeqStringTheoryStringTheory
  92. val str_to_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  93. val str_to_re: MonoSortedIFunction

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

    Permalink

    Convert a string to a term

    Convert a string to a term

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

    Permalink
    Definition Classes
    AnyRef
  96. 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
  97. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  98. 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
  99. 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
  100. val upperBound: IdealInt

    Permalink
  101. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  102. final def wait(arg0: Long, arg1: Int): Unit

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

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

Inherited from AbstractStringTheory

Inherited from StringTheory

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped