 # ComputationLogger

### Related Docs: object ComputationLogger | package terfor

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

Linear Supertypes
AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ComputationLogger
2. AnyRef
3. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### Abstract Value Members

1. #### abstract def antiSymmetry(leftInEq: LinearCombination, rightInEq: LinearCombination, order: TermOrder): Unit

Turn two complementary inequalities into an equation

2. #### 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

3. #### 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

4. #### 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 `ineqs` might be stored and evaluated much later, or not at all if the represented inference turns out to be unnecessary.

5. #### abstract def directStrengthen(inequality: LinearCombination, equation: LinearCombination, result: LinearCombination, order: TermOrder): Unit

Given the two formulae `t >= 0` and `t != 0` (or, similarly, `t >= 0` and `-t != 0`), infer the inequality `t-1 >= 0`.

Given the two formulae `t >= 0` and `t != 0` (or, similarly, `t >= 0` and `-t != 0`), infer the inequality `t-1 >= 0`.

6. #### 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

8. #### 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.

9. #### 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`).

Inference corresponding to a series of applications of the reduce rule to a an inequality (reduction of positive equalities is described using `CombineEquationsInference`).

10. #### 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`).

Inference corresponding to a series of applications of the reduce rule to a negated equation (reduction of positive equalities is described using `CombineEquationsInference`).

11. #### 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

12. #### 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.

13. #### 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

1. #### final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
2. #### final def ##(): Int

Definition Classes
AnyRef → Any
3. #### final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
4. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
5. #### val ceScope: LogScope[(Seq[(IdealInt, LinearCombination)], TermOrder), (LinearCombination, LinearCombination)]

Convenient interface for `combineEquations`

Convenient interface for `combineEquations`

6. #### val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]

Convenient interface for `combineInequalities`

Convenient interface for `combineInequalities`

7. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
8. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
9. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
10. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
11. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
12. #### def hashCode(): Int

Definition Classes
AnyRef → Any
13. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
14. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
15. #### final def notify(): Unit

Definition Classes
AnyRef
16. #### final def notifyAll(): Unit

Definition Classes
AnyRef
17. #### val otherCompScope: LogScope[(Seq[Formula], TermOrder, AnyRef), Formula]

Convenient interface for `otherComputation`

Convenient interface for `otherComputation`

18. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
19. #### def toString(): String

Definition Classes
AnyRef → Any
20. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
21. #### final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
22. #### final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )