Trait/Object

ap.theories.strings

StringTheory

Related Docs: object StringTheory | package strings

Permalink

trait StringTheory extends Theory

Generic class describing string theories.

Linear Supertypes
Theory, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. StringTheory
  2. Theory
  3. AnyRef
  4. 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 RichWord extends AnyRef

    Permalink

    Helper class providing string infix operators

Abstract Value Members

  1. abstract val CharSort: Sort

    Permalink

    Sort representing characters

  2. abstract val RegexSort: Sort

    Permalink

    Sort representing regular expressions

  3. abstract val StringSort: Sort

    Permalink

    Sort representing strings

  4. abstract val _str_++: Predicate

    Permalink

    The predicate corresponding to str_++

    The predicate corresponding to str_++

  5. abstract val _str_cons: Predicate

    Permalink

    The predicate corresponding to str_cons

    The predicate corresponding to str_cons

  6. abstract val _str_empty: Predicate

    Permalink

    The predicate corresponding to str_empty

    The predicate corresponding to str_empty

  7. abstract val alphabetSize: Int

    Permalink
  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

  10. abstract val char_is_digit: Predicate

    Permalink
  11. abstract val extraOps: Map[String, Either[IFunction, Predicate]]

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

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

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

    Permalink

    Convert an integer term to a character term

  16. 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
  17. 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
  18. abstract val predicates: Seq[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    Theory
  19. abstract val re_*: IFunction

    Permalink
  20. abstract val re_+: IFunction

    Permalink
  21. abstract val re_++: IFunction

    Permalink
  22. abstract val re_all: IFunction

    Permalink
  23. abstract val re_allchar: IFunction

    Permalink
  24. abstract val re_charrange: IFunction

    Permalink
  25. abstract val re_comp: IFunction

    Permalink
  26. abstract val re_eps: IFunction

    Permalink
  27. abstract val re_from_str: IFunction

    Permalink
  28. abstract val re_inter: IFunction

    Permalink
  29. abstract val re_loop: IFunction

    Permalink
  30. abstract val re_none: IFunction

    Permalink
  31. abstract val re_opt: IFunction

    Permalink
  32. abstract val re_range: IFunction

    Permalink
  33. abstract val re_union: IFunction

    Permalink
  34. abstract val str: IFunction

    Permalink
  35. abstract val str_++: IFunction

    Permalink
  36. abstract val str_<=: Predicate

    Permalink
  37. abstract val str_at: IFunction

    Permalink
  38. abstract val str_char: IFunction

    Permalink
  39. abstract val str_cons: IFunction

    Permalink
  40. abstract val str_contains: Predicate

    Permalink
  41. abstract val str_empty: IFunction

    Permalink
  42. abstract val str_from_code: IFunction

    Permalink
  43. abstract val str_head: IFunction

    Permalink
  44. abstract val str_head_code: IFunction

    Permalink
  45. abstract val str_in_re: Predicate

    Permalink
  46. abstract val str_indexof: IFunction

    Permalink
  47. abstract val str_len: IFunction

    Permalink
  48. abstract val str_prefixof: Predicate

    Permalink
  49. abstract val str_replace: IFunction

    Permalink
  50. abstract val str_replaceall: IFunction

    Permalink
  51. abstract val str_replaceallre: IFunction

    Permalink
  52. abstract val str_replacere: IFunction

    Permalink
  53. abstract val str_substr: IFunction

    Permalink
  54. abstract val str_suffixof: Predicate

    Permalink
  55. abstract val str_tail: IFunction

    Permalink
  56. abstract val str_to_code: IFunction

    Permalink
  57. abstract val str_to_re: IFunction

    Permalink
  58. 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
  59. 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. final def asInstanceOf[T0]: T0

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

    Permalink

    Translate a numeric value from a model to a string.

  6. val asStringPartial: Decoder[Option[String]]

    Permalink

    Translate a numeric value from a model to a string.

  7. def clone(): AnyRef

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  11. 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
  12. 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
  13. 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
  14. def finalize(): Unit

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

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

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  24. 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
  25. 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
  26. 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
  27. implicit def string2Term(str: String): ITerm

    Permalink

    Convert a string to a term

  28. final def synchronized[T0](arg0: ⇒ T0): T0

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

    Permalink

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

  30. def toString(): String

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

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

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

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

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped