ADT

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def SMTDeclarationSideEffects: Seq[Theory]

A list of (other) theories that are implicitly declared as a side-effect of declaring this theory.

object SortNum

Extractor to recognise sorts belonging to this ADT.

final def asInstanceOf[T0]: T0

val axioms: Formula

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 cardinalities: Seq[Option[IdealInt]]

The number of elements per sort, or None for infinite sorts.

def clone(): AnyRef

val constructorPreds: IndexedSeq[Predicate]

val constructors: IndexedSeq[MonoSortedIFunction]

The constructors of the ADT

val ctorId2PerSortId: IndexedSeq[Int]

val ctorIdPreds: IndexedSeq[Predicate]

val ctorIds: IndexedSeq[MonoSortedIFunction]

Function symbols representing the index of the head symbol of a constructor term

def ctorIdsPerSort: IndexedSeq[IndexedSeq[Int]]

List the constructors belonging to each sort; the constructors are identified with the position of a constructor in the sequence ctorSignatures.

def ctorTermSize(f: ITerm): Option[Int]

Compute the size (number of constructor occurrences) of a constructor term; return None if parts of the term are symbolic, and the size cannot be determined.

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 evaluatingSimplifier(t: IExpression): IExpression

A simplification function that applies the methods evalFun and evalPred to some given expression (but not recursively).

def extend(order: TermOrder): TermOrder

Add the symbols defined by this theory to the order

def fun2SMTString(f: IFunction): Option[String]

Translate a function belonging to this theory to an SMT-LIB identifier.

val functionPredicateMapping: Seq[(IFunction, Predicate)]

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

val functionTranslation: Map[IFunction, Predicate]

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: Seq[IFunction]

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 getCtorPerSort(sortNum: Int, ctorNum: Int): MonoSortedIFunction

Get the constructor number ctorNum of sort sortNum.

def hasCtor(t: ITerm, id: Int): IFormula

Query the constructor type of a term; the given id is the position of a constructor in the sequence ctorSignatures.

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.

val isEnum: IndexedSeq[Boolean]

Enum sorts, i.e., sorts with only nullary constructors.

final def isInstanceOf[T0]: Boolean

lazy val isRecursive: IndexedSeq[Boolean]

Recursive sorts, i.e., sorts that can appear (directly or indirectly) as sort of subterms of its own terms.

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

lazy val parikhSizeConstraints: IndexedSeq[Conjunction]

def plugin: Option[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 pred2SMTString(p: Predicate): Option[String]

Translate a predicate belonging to this theory to an SMT-LIB identifier.

val predicateMatchConfig: PredicateMatchConfig

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

val predicates: Seq[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.

def printSMTDeclaration: Unit

Print an SMT-LIB declaration of this theory; do not output anything if the theory does not need to be declared.

val reducerPlugin: ReducerPluginFactory

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

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

Rewrite a formula prior to solving; e.g., add selector and tester constraints

val selectorPreds: IndexedSeq[Seq[Predicate]]

val selectors: IndexedSeq[Seq[MonoSortedIFunction]]

The selectors of the 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.

lazy val sizeLowerBound: IndexedSeq[IdealInt]

def sort2SMTType(s: Sort): Option[SMTType]

Translate a sort belonging to this theory to an SMT type.

def sortOfCtor(ctorNum: Int): Int

The sort sorts(n) belonging to the constructor constructors(ctorNum).

lazy val sortSCCs: IndexedSeq[Seq[Int]]

The strongly connected components among the ADTs sorts.

val sorts: IndexedSeq[ADTProxySort]

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

val termDepth: IndexedSeq[MonoSortedIFunction]

Function symbols representing (relative) depth of constructor terms.

val termDepthPreds: IndexedSeq[Predicate]

val termSize: IndexedSeq[MonoSortedIFunction]

Function symbols representing absolute size of constructor terms.

val termSizePreds: IndexedSeq[Predicate]

def toString(): String

val totalityAxioms: Conjunction

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

lazy val transitiveDependencies: Iterable[Theory]

Dependencies closed under transitivity, i.e., also including the dependencies of dependencies.

val triggerRelevantFunctions: Set[IFunction]

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

lazy val uniqueTermSize: IndexedSeq[Option[IdealInt]]

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

final def wait(arg0: Long): Unit

final def wait(): Unit

val witnesses: Seq[ITerm]

def finalize(): Unit