trait ComputationLogger extends AnyRef
Trait that can be used to track the computation taking place in systems of equations, inequalities, etc. This is used to produce proofs.
- Alphabetic
- By Inheritance
- ComputationLogger
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Abstract Value Members
- abstract def antiSymmetry(leftInEq: LinearCombination, rightInEq: LinearCombination, order: TermOrder): Unit
Turn two complementary inequalities into an equation
- abstract def combineEquations(equations: Seq[(IdealInt, LinearCombination)], result: LinearCombination, resultAfterRounding: LinearCombination, order: TermOrder): Unit
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a number of positive equations.
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a number of positive equations. The given terms (apart from
result) shall be primitive, with a positive leading coefficient - abstract def combineInequalities(leftCoeff: IdealInt, leftInEq: LinearCombination, rightCoeff: IdealInt, rightInEq: LinearCombination, result: LinearCombination, resultAfterRounding: LinearCombination, order: TermOrder): Unit
Fourier-Motzkin Inference.
Fourier-Motzkin Inference. The given terms shall be primitive, and the result will be implicitly rounded
- abstract def combineInequalitiesLazy(ineqs: Iterator[(IdealInt, LinearCombination)], resultAfterRounding: LinearCombination, order: TermOrder): Unit
Compute the sum of multiple inequalities, and round the result afterwards.
Compute the sum of multiple inequalities, and round the result afterwards. The argument
ineqsmight be stored and evaluated much later, or not at all if the represented inference turns out to be unnecessary. - abstract def directStrengthen(inequality: LinearCombination, equation: LinearCombination, result: LinearCombination, order: TermOrder): Unit
Given the two formulae
t >= 0andt != 0(or, similarly,t >= 0and-t != 0), infer the inequalityt-1 >= 0. - abstract def groundInstantiateQuantifier(quantifiedFormula: Conjunction, instanceTerms: Seq[LinearCombination], instance: Conjunction, dischargedAtoms: PredConj, result: Conjunction, order: TermOrder): Unit
Instantiate a universally quantified formula with ground terms
- abstract val isLogging: Boolean
- abstract def otherComputation(assumptions: Seq[Formula], result: Formula, order: TermOrder, theory: AnyRef): Unit
Some other computation, that might in particular be performed by theory plug-ins.
- abstract def reduceInequality(equations: Seq[(IdealInt, LinearCombination)], targetLit: LinearCombination, order: TermOrder): Unit
Inference corresponding to a series of applications of the reduce rule to a an inequality (reduction of positive equalities is described using
CombineEquationsInference). - abstract def reduceNegEquation(equations: Seq[(IdealInt, LinearCombination)], targetLit: LinearCombination, order: TermOrder): Unit
Inference corresponding to a series of applications of the reduce rule to a negated equation (reduction of positive equalities is described using
CombineEquationsInference). - abstract def reducePredFormula(equations: Seq[Seq[(IdealInt, LinearCombination)]], targetLit: Atom, negated: Boolean, result: Atom, order: TermOrder): Unit
Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal.
Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal. This is essentially the same as the
reduceArithFormula, only that all of the arguments can be reduced simultaneously - abstract def unifyFunctionApps(leftApp: Atom, rightApp: Atom, resultEq: LinearCombination, order: TermOrder): Unit
Apply the functional consistency axiom to derive that the results of two function applications (encoded as predicate atoms) must be the same.
- abstract def unifyPredicates(leftAtom: Atom, rightAtom: Atom, result: EquationConj, order: TermOrder): Unit
Unify two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val ceScope: LogScope[(Seq[(IdealInt, LinearCombination)], TermOrder), (LinearCombination, LinearCombination)]
Convenient interface for
combineEquations - val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]
Convenient interface for
combineInequalities - def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val otherCompScope: LogScope[(Seq[Formula], TermOrder, AnyRef), Formula]
Convenient interface for
otherComputation - final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)