Class

ap.theories.strings

AbstractStringTheory

Related Doc: package strings

Permalink

abstract class AbstractStringTheory extends StringTheory

Abstract class defining relevant string operations as sorted functions/predicates

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

Instance Constructors

  1. new AbstractStringTheory()

    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
  3. class RegexExtractor extends AnyRef

    Permalink

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

  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

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 StringSort: Sort

    Permalink

    Sort representing strings

    Sort representing strings

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

    Permalink

    The predicate corresponding to str_++

    The predicate corresponding to str_++

    Definition Classes
    StringTheory
  5. abstract val _str_cons: Predicate

    Permalink

    The predicate corresponding to str_cons

    The predicate corresponding to str_cons

    Definition Classes
    StringTheory
  6. abstract val _str_empty: Predicate

    Permalink

    The predicate corresponding to str_empty

    The predicate corresponding to str_empty

    Definition Classes
    StringTheory
  7. abstract val alphabetSize: Int

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

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

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

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

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    Theory
  18. abstract val str_cons: IFunction

    Permalink
    Definition Classes
    StringTheory
  19. abstract val str_empty: IFunction

    Permalink
    Definition Classes
    StringTheory
  20. abstract val str_head: IFunction

    Permalink
    Definition Classes
    StringTheory
  21. abstract val str_tail: IFunction

    Permalink
    Definition Classes
    StringTheory
  22. 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
  23. 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.

  5. object RegexExtractor

    Permalink
  6. object WordExtractor

    Permalink
  7. final def asInstanceOf[T0]: T0

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

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

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

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

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

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

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

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

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

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

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

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

    Permalink
    Attributes
    protected
  31. def predefPredicates: List[MonoSortedPredicate]

    Permalink
    Attributes
    protected
  32. 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
  33. val re_*: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  34. val re_+: MonoSortedIFunction

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  36. val re_all: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  37. val re_allchar: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  38. val re_charrange: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  39. val re_comp: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  40. val re_eps: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  41. val re_from_str: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  42. val re_inter: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  43. val re_loop: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  44. val re_none: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  45. val re_opt: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  46. val re_range: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  47. val re_union: MonoSortedIFunction

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

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

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

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  53. val str_at: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  54. val str_char: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  55. val str_contains: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  56. val str_from_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  57. val str_head_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  58. val str_in_re: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  59. val str_indexof: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  60. val str_len: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  61. val str_prefixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  62. val str_replace: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  63. val str_replaceall: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  64. val str_replaceallre: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  65. val str_replacere: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  66. val str_substr: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  67. val str_suffixof: MonoSortedPredicate

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  68. val str_to_code: MonoSortedIFunction

    Permalink
    Definition Classes
    AbstractStringTheoryStringTheory
  69. val str_to_re: MonoSortedIFunction

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

    Permalink

    Convert a string to a term

    Convert a string to a term

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

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

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

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

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

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

Inherited from StringTheory

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped