Rationals

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

object FracTerm

Extractor for fractions, where numerator and denominator are expressions from the underlying ring.

object Fraction

Object to construct and identify fractions, consisting of a numerator and a denominator.

object FractionSort extends ProxySort with TheorySort

object IncompletenessChecker extends ContextAwareVisitor[Unit, Unit]

The theory is not complete for the full first-order case; check whether the denom function occurs in the scope of a quantifier.

val RatDivZero: IFunction

Uninterpreted function representing the SMT-LIB rational division by zero.

val RatDivZeroTheory: DivZero

object RingCastTerm

Extractor for ring elements embedded into the ring of fractions.

val addition: IFunction

Function to represent sums of terms.

def additiveGroup: Group with Abelian with SymbolicTimes

Addition gives rise to an Abelian group

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

def clone(): AnyRef

val denom: IFunction

Function used internally to represent the unique denominator for all fractions

val denomT: ITerm

val dependencies: List[nia.GroebnerMultiplication.type]

Optionally, other theories that this theory depends on.

def div(s: ITerm, t: ITerm): ITerm

Division operation

def divByDenom(t: ITerm): (ITerm, IdealInt)

Divide each term of a sum by the denom() term, rewriting accordingly.

def divWithSpecialZero(s: ITerm, t: ITerm): ITerm

Division, assuming SMT-LIB semantics for division by zero.

val division: IFunction

Function to represent division.

val dom: Sort

Domain of the ring

def encodeExpr(t: IExpression, subres: Seq[IExpression], usedDenom: Array[Boolean]): IExpression

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 extraPredicates: List[Predicate]

val frac: IFunction

Function to represent fractions, where numerator and denominator are expressions from the underlying ring

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

val fromRing: IFunction

Function to embed ring elements in the ring of fractions.

val funPredMap: Map[IFunction, Predicate]

val functionPredicateMapping: List[(IFunction, 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[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.

def geq(s: ITerm, t: ITerm): IFormula

Greater-than-or-equal operator

final def getClass(): Class[_]

def gt(s: ITerm, t: ITerm): IFormula

Greater-than operator

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 ignoringQuantifiers[A](comp: ⇒ A): A

Hack to enable other theories to use rationals even in axioms with quantifiers.

def individualsStream: Option[Stream[ITerm]]

Optionally, a stream of the constructor terms for this domain can be defined (e.g., the fractions with co-prime numerator and denominator).

def int2ring(s: ITerm): ITerm

Conversion of an integer term to a ring term

def inverse(s: ITerm): ITerm

final def isInstanceOf[T0]: Boolean

def isInt(s: ITerm): IFormula

Test whether a rational is integer.

def isNonZeroRingTerm(t: ITerm): 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.

def leq(s: ITerm, t: ITerm): IFormula

Less-than-or-equal operator

lazy val lessThan: Predicate

Less-than predicate.

lazy val lessThanOrEqual: Predicate

Less-than-or-equal predicate.

def lt(s: ITerm, t: ITerm): IFormula

Less-than operator

def minus(s: ITerm): ITerm

Additive inverses

def minus(s: ITerm, t: ITerm): ITerm

Difference between two terms

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 mul(s: ITerm, t: ITerm): ITerm

Ring multiplication

val multWithFraction: IFunction

Function to represent a product of a fraction, represented using numerator and denominator, with a fraction term.

val multWithRing: IFunction

Function to represent a product of a ring term with a fraction term.

val multiplication: IFunction

Function to represent products of terms.

def multiplicativeGroup: Group with Abelian

Non-zero elements now give rise to an Abelian group

def multiplicativeMonoid: Monoid with Abelian

Multiplication gives rise to an Abelian monoid

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

val one: ITerm

The one element of this ring

val plugin: None.type

Optionally, a plug-in implementing reasoning in this theory

def plus(s: ITerm, t: ITerm): ITerm

Ring addition

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, signature: Signature): Conjunction

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

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, signature: Signature): Conjunction

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

def product(terms: ITerm*): ITerm

N-ary sums

val reducerPlugin: ReducerPluginFactory

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

def ring2int(s: ITerm): ITerm

Conversion of a rational term to an integer term, the floor operator.

def simplifiers: List[(IExpression) ⇒ IExpression]

def simplifyFraction(n: ITerm, d: ITerm): (ITerm, ITerm)

Method that can be overwritten in sub-classes to term concrete fractions into canonical form.

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.

def summation(terms: ITerm*): ITerm

N-ary sums

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

def termNeedsRewr(t: ITerm): Boolean

def times(num: ITerm, s: ITerm): ITerm

num * s, where num must be an integer term.

def times(num: IdealInt, s: ITerm): ITerm

num * s

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

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

final def wait(arg0: Long): Unit

final def wait(): Unit

val zero: ITerm

The zero element of this ring

def finalize(): Unit