Class/Object

ap.theories.strings

AbstractStringTheoryWithSort

Related Docs: object AbstractStringTheoryWithSort | package strings

Permalink

abstract class AbstractStringTheoryWithSort extends AbstractStringTheory

Abstract class defining relevant string operations as sorted functions/predicates, as well as an infinite string sort together with constructor and selector operations.

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

Instance Constructors

  1. new AbstractStringTheoryWithSort()

    Permalink

Type Members

  1. class IllegalRegexException extends Exception

    Permalink
    Definition Classes
    AbstractStringTheory
  2. 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
  3. class RichWord extends AnyRef

    Permalink

    Helper class providing string infix operators

    Helper class providing string infix operators

    Definition Classes
    StringTheory
  4. class WordExtractor extends AnyRef

    Permalink
    Definition Classes
    AbstractStringTheory

Abstract Value Members

  1. abstract val CharSort: Sort

    Permalink

    Sort representing characters

    Sort representing characters

    Definition Classes
    StringTheory
  2. abstract val RegexSort: Sort

    Permalink

    Sort representing regular expressions

    Sort representing regular expressions

    Definition Classes
    StringTheory
  3. abstract val _str_++: Predicate

    Permalink

    The predicate corresponding to str_++

    The predicate corresponding to str_++

    Definition Classes
    StringTheory
  4. abstract val _str_cons: Predicate

    Permalink

    The predicate corresponding to str_cons

    The predicate corresponding to str_cons

    Definition Classes
    StringTheory
  5. abstract val _str_empty: Predicate

    Permalink

    The predicate corresponding to str_empty

    The predicate corresponding to str_empty

    Definition Classes
    StringTheory
  6. abstract val alphabetSize: Int

    Permalink
    Definition Classes
    StringTheory
  7. abstract 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
  8. abstract 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
  9. abstract 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
    Theory
  10. abstract def char2Int(t: ITerm): ITerm

    Permalink

    Convert a character term to an integer term

    Convert a character term to an integer term

    Definition Classes
    StringTheory
  11. abstract val extraIndexedOps: Map[(String, Int), Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    StringTheory
  12. abstract val extraOps: Map[String, Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    StringTheory
  13. abstract val functionPredicateMapping: Seq[(IFunction, 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
    Theory
  14. abstract 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
    Theory
  15. abstract val functions: Seq[IFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    Theory
  16. abstract def int2Char(t: ITerm): ITerm

    Permalink

    Convert an integer term to a character term

    Convert an integer term to a character term

    Definition Classes
    StringTheory
  17. abstract def plugin: Option[Plugin]

    Permalink

    Optionally, a plug-in implementing reasoning in this theory

    Optionally, a plug-in implementing reasoning in this theory

    Definition Classes
    Theory
  18. abstract 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
    Theory
  19. abstract val predicates: Seq[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    Theory
  20. abstract val totalityAxioms: Formula

    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
    Theory
  21. abstract 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
    Theory

Concrete 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. 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
  5. object RegexExtractor

    Permalink
    Definition Classes
    AbstractStringTheory
  6. val StringSort: AbstractStringSort

    Permalink

    Sort representing strings

    Sort representing strings

    Definition Classes
    AbstractStringTheoryWithSortStringTheory
  7. object WordExtractor

    Permalink
    Definition Classes
    AbstractStringTheory
  8. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  9. 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
  10. 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
  11. val char_is_digit: MonoSortedPredicate

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  16. 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
  17. 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
  18. 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
  19. 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
    Theory
  20. final def getClass(): Class[_]

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  22. 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
  23. 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
    Theory
  24. 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
  25. val int_to_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  26. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  27. 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
    Theory
  28. 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
  29. final def ne(arg0: AnyRef): Boolean

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

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  32. 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
  33. 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
  34. def predefFunctions: List[MonoSortedIFunction]

    Permalink
    Attributes
    protected
    Definition Classes
    AbstractStringTheoryWithSortAbstractStringTheory
  35. def predefPredicates: List[MonoSortedPredicate]

    Permalink
    Attributes
    protected
    Definition Classes
    AbstractStringTheory
  36. 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
    Theory
  37. val re_*: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  38. val re_+: MonoSortedIFunction

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  40. val re_all: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  41. val re_allchar: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  42. val re_charrange: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  43. val re_comp: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  44. val re_diff: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  45. val re_eps: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  46. val re_from_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  47. val re_inter: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  48. val re_loop: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  49. val re_none: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  50. val re_opt: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  51. val re_range: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  52. val re_union: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  53. 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
  54. 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
  55. val str_++: MonoSortedIFunction

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  57. val str_at: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  58. val str_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  59. val str_cons: MonoSortedIFunction

    Permalink
  60. val str_contains: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  61. val str_empty: MonoSortedIFunction

    Permalink
  62. val str_from_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  63. val str_from_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  64. val str_head: MonoSortedIFunction

    Permalink
  65. val str_head_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  66. val str_in_re: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  67. val str_indexof: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  68. val str_len: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  69. val str_prefixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  70. val str_replace: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  71. val str_replaceall: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  72. val str_replaceallre: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  73. val str_replacere: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  74. val str_substr: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  75. val str_suffixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  76. val str_tail: MonoSortedIFunction

    Permalink
  77. val str_to_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  78. val str_to_int: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  79. val str_to_re: MonoSortedIFunction

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

    Permalink

    Convert a string to a term

    Convert a string to a term

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  84. final def wait(arg0: Long, arg1: Int): Unit

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  86. 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