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. 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

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 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
  8. 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
  9. abstract val extraOps: Map[String, Either[IFunction, Predicate]]

    Permalink
    Definition Classes
    StringTheory
  10. 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
  11. 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
  12. abstract val functions: Seq[IFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    Theory
  13. 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
  14. 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
  15. 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
  16. abstract val predicates: Seq[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    Theory
  17. 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
  18. 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. 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
  10. 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
  11. 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
  12. 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
  13. val char_is_digit: MonoSortedPredicate

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  18. 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
  19. 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
  20. 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
  21. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  22. 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
  23. final def getClass(): Class[_]

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  31. def predefFunctions: List[MonoSortedIFunction]

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

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  35. val re_+: MonoSortedIFunction

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  37. val re_all: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  38. val re_allchar: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  39. val re_charrange: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  40. val re_comp: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  41. val re_eps: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  42. val re_from_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  43. val re_inter: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  44. val re_loop: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  45. val re_none: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  46. val re_opt: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  47. val re_range: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  48. val re_union: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  49. 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
  50. 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
  51. val str: MonoSortedIFunction

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

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  54. val str_at: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  55. val str_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  56. val str_cons: MonoSortedIFunction

    Permalink
  57. val str_contains: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  58. val str_empty: MonoSortedIFunction

    Permalink
  59. val str_from_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  60. val str_head: MonoSortedIFunction

    Permalink
  61. val str_head_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  62. val str_in_re: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  63. val str_indexof: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  64. val str_len: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  65. val str_prefixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  66. val str_replace: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  67. val str_replaceall: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  68. val str_replaceallre: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  69. val str_replacere: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  70. val str_substr: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  71. val str_suffixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  72. val str_tail: MonoSortedIFunction

    Permalink
  73. val str_to_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  74. val str_to_re: MonoSortedIFunction

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

    Permalink

    Convert a string to a term

    Convert a string to a term

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  79. final def wait(): Unit

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

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