MulTheory

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

abstract val functionPredicateMapping: Seq[(IFunction, Predicate)]

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

abstract val functionalPredicates: Set[Predicate]

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

abstract val functions: Seq[IFunction]

Interpreted functions of the theory

abstract val mul: IFunction

Symbol representing proper (non-linear) multiplication

abstract def plugin: Option[Plugin]

Optionally, a plug-in implementing reasoning in this theory

abstract val predicateMatchConfig: PredicateMatchConfig

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

abstract val predicates: Seq[Predicate]

Interpreted predicates of the theory

abstract val totalityAxioms: Formula

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

abstract val triggerRelevantFunctions: Set[IFunction]

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

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def clone(): AnyRef

def convert(expr: IFormula): IFormula

Convert the given expression to this multiplication theory

def convert(expr: ITerm): ITerm

Convert the given expression to this multiplication theory

def convert(expr: IExpression): IExpression

Convert the given expression to this multiplication theory

implicit def convert2RichMulTerm(term: ITerm): RichMulTerm

val dependencies: Iterable[Theory]

Optionally, other theories that this theory depends on.

def eDiv(numTerm: ITerm, denomTerm: ITerm): ITerm

Euclidian division

def eDivWithSpecialZero(num: ITerm, denom: ITerm): ITerm

Euclidian division, assuming the SMT-LIB semantics for division by zero.

def eMod(numTerm: ITerm, denomTerm: ITerm): ITerm

Euclidian remainder

def eModWithSpecialZero(num: ITerm, denom: ITerm): ITerm

Euclidian remaining, assuming the SMT-LIB semantics for remainder by zero.

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

def fDiv(numTerm: ITerm, denomTerm: ITerm): ITerm

Floor division

def fMod(numTerm: ITerm, denomTerm: ITerm): ITerm

Floor remainder

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.

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.

def mult(t1: ITerm, t2: ITerm): ITerm

Multiply two terms, using the mul function if necessary; if any of the two terms is constant, normal Presburger multiplication will be used.

def multSimplify(t1: ITerm, t2: ITerm): ITerm

Multiply two terms, using the mul function if necessary; if any of the two terms is constant, normal Presburger multiplication will be used, and simple terms will directly be simplified.

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

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 pow(basis: ITerm, expTerm: ITerm): ITerm

Exponentiation, with non-negative exponent

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 reducerPlugin: ReducerPluginFactory

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

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.

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

def tDiv(numTerm: ITerm, denomTerm: ITerm): ITerm

Truncation division

def tMod(numTerm: ITerm, denomTerm: ITerm): ITerm

Truncation remainder

def toString(): String

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit