SeqStringTheory

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

val CharSort: ModSort

Sort representing characters

object ConcreteRegex

Extractor to identify regular expressions that are completely defined, i.e., in which no sub-terms are left symbolic.

object RegexExtractor

val RegexSort: InfUninterpretedSort

Sort representing regular expressions

val StringSort: ADTProxySort

Sort representing strings

object WordExtractor

val _str_++: Predicate

The predicate corresponding to str_++

val _str_cons: Predicate

The predicate corresponding to str_cons

val _str_empty: Predicate

The predicate corresponding to str_empty

val allAxioms: IFormula

val alphabetSize: Int

final def asInstanceOf[T0]: T0

val asString: Decoder[String]

Translate a numeric value from a model to a string.

val asStringPartial: Decoder[Option[String]]

Translate a numeric value from a model to a string.

def assignStringValues(facts: Conjunction, assignment: Map[Term, Seq[Int]], order: TermOrder): Conjunction

Augment goal facts with the given assignment of strings to terms.

val axioms: Conjunction

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

val axioms1: Formula

def breakCyclicEquations(goal: Goal): Option[Seq[Action]]

Check for cyclic word equations induced by str_++ or str_cons, and break those.

def char2Int(t: ITerm): ITerm

Convert a character term to an integer term

val char_is_digit: MonoSortedPredicate

def clone(): AnyRef

val dependencies: Iterable[Theory]

Optionally, other theories that this theory depends on.

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def evalFun(f: IFunApp): Option[ITerm]

Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

def evalPred(p: IAtom): Option[Boolean]

Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

def extend(order: TermOrder): TermOrder

Add the symbols defined by this theory to the order

val extraIndexedOps: Map[(String, Int), Either[IFunction, Predicate]]

val extraOps: Map[String, Either[IFunction, Predicate]]

val funPredMap: Map[IFunction, Predicate]

val funPredicates: Seq[Predicate]

val functionPredicateMapping: List[(MonoSortedIFunction, Predicate)]

Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

val functionalPredicates: Set[Predicate]

Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

val functions: List[MonoSortedIFunction]

Interpreted functions of the theory

def generateDecoderData(model: Conjunction): Option[TheoryDecoderData]

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.

final def getClass(): Class[_]

def hashCode(): Int

def iPostprocess(f: IFormula, signature: Signature): IFormula

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

def iPreprocess(f: IFormula, signature: Signature): (IFormula, Signature)

Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

def int2Char(t: ITerm): ITerm

Convert an integer term to a character term

def int2String(t: ITerm): ITerm

Convert an integer term to a singleton string

val intToStrAxioms: IFormula

val int_to_str: MonoSortedIFunction

val int_to_str_help: MonoSortedIFunction

final def isInstanceOf[T0]: Boolean

def isSoundForSat(theories: Seq[Theory], config: Theory.SatSoundnessConfig.Value): Boolean

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.

val modelGenPredicates: Set[Predicate]

Optionally, a set of predicates used by the theory to tell the PresburgerModelFinder about terms that will be handled exclusively by this theory.

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

val order: TermOrder

def plugin: Some[Plugin]

Optionally, a plug-in implementing reasoning in this theory

def postSimplifiers: Seq[(IExpression) ⇒ IExpression]

Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier.

def postprocess(f: Conjunction, order: TermOrder): Conjunction

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

def predefFunctions: List[MonoSortedIFunction]

def predefPredicates: List[MonoSortedPredicate]

val predicateMatchConfig: PredicateMatchConfig

Information how interpreted predicates should be handled for e-matching.

val predicates: List[Predicate]

Interpreted predicates of the theory

def preprocess(f: Conjunction, order: TermOrder): Conjunction

Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

val reDerivativeAxioms: IFormula

val reDerivativeAxioms2: Formula

val reMatchingAxioms: IFormula

val reMatchingAxioms2: Formula

val reNullableAxioms: IFormula

val reSimpAxioms: IFormula

val re_*: MonoSortedIFunction

val re_+: MonoSortedIFunction

val re_++: MonoSortedIFunction

val re_all: MonoSortedIFunction

val re_allchar: MonoSortedIFunction

val re_charrange: MonoSortedIFunction

val re_comp: MonoSortedIFunction

val re_derivative_help: MonoSortedIFunction

val re_diff: MonoSortedIFunction

val re_eps: MonoSortedIFunction

val re_from_str: MonoSortedIFunction

val re_inter: MonoSortedIFunction

val re_loop: MonoSortedIFunction

val re_matches_str_help: MonoSortedIFunction

val re_none: MonoSortedIFunction

val re_nullable_help: MonoSortedIFunction

val re_opt: MonoSortedIFunction

val re_range: MonoSortedIFunction

val re_union: MonoSortedIFunction

val reducerPlugin: ReducerPluginFactory

Optionally, a plugin for the reducer applied to formulas both before and during proving.

val seqADT: ADT

val singleInstantiationPredicates: Set[Predicate]

When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

val strAtAxioms: IFormula

val strIndexofAxioms: IFormula

val strReplaceAxioms: IFormula

val strSubstrAxioms: IFormula

val strToIntAxioms: IFormula

val str_++: MonoSortedIFunction

val str_<=: MonoSortedPredicate

val str_at: MonoSortedIFunction

val str_char: MonoSortedIFunction

val str_cons: MonoSortedIFunction

val str_contains: MonoSortedPredicate

val str_empty: MonoSortedIFunction

val str_from_char: MonoSortedIFunction

val str_from_code: MonoSortedIFunction

val str_head: MonoSortedIFunction

val str_head_code: MonoSortedIFunction

val str_in_re: MonoSortedPredicate

val str_indexof: MonoSortedIFunction

val str_indexof_help: MonoSortedIFunction

val str_len: MonoSortedIFunction

val str_prefixof: MonoSortedPredicate

val str_replace: MonoSortedIFunction

val str_replaceall: MonoSortedIFunction

val str_replaceallre: MonoSortedIFunction

val str_replacere: MonoSortedIFunction

val str_substr: MonoSortedIFunction

val str_suffixof: MonoSortedPredicate

val str_tail: MonoSortedIFunction

val str_to_code: MonoSortedIFunction

val str_to_int: MonoSortedIFunction

val str_to_int_help: MonoSortedIFunction

val str_to_re: MonoSortedIFunction

implicit def string2Term(str: String): ITerm

Convert a string to a term

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

implicit def term2RichWord(t: ITerm): RichWord

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

def toString(): String

val totalityAxioms: Conjunction

Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

val triggerRelevantFunctions: Set[IFunction]

A list of functions that should be considered in automatic trigger generation

val upperBound: IdealInt

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit