# NonLoggingLogger

### Related Doc: package ComputationLogger

#### class NonLoggingLogger extends ComputationLogger

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

### 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. #### def antiSymmetry(leftInEq: LinearCombination, rightInEq: LinearCombination, order: TermOrder): Unit

Turn two complementary inequalities into an equation

Turn two complementary inequalities into an equation

Definition Classes
NonLoggingLoggerComputationLogger
5. #### final def asInstanceOf[T0]: T0

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

Convenient interface for `combineEquations`

Convenient interface for `combineEquations`

Definition Classes
ComputationLogger
7. #### val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]

Convenient interface for `combineInequalities`

Convenient interface for `combineInequalities`

Definition Classes
ComputationLogger
8. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
9. #### 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

Definition Classes
NonLoggingLoggerComputationLogger
10. #### 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

Definition Classes
NonLoggingLoggerComputationLogger
11. #### 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.

Definition Classes
NonLoggingLoggerComputationLogger
12. #### 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`.

Definition Classes
NonLoggingLoggerComputationLogger
13. #### final def eq(arg0: AnyRef): Boolean

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

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

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

Definition Classes
AnyRef → Any
17. #### def groundInstantiateQuantifier(quantifiedFormula: Conjunction, instanceTerms: Seq[LinearCombination], instance: Conjunction, dischargedAtoms: PredConj, result: Conjunction, order: TermOrder): Unit

Instantiate a universally quantified formula with ground terms

Instantiate a universally quantified formula with ground terms

Definition Classes
NonLoggingLoggerComputationLogger
18. #### def hashCode(): Int

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

Definition Classes
Any
20. #### val isLogging: Boolean

Definition Classes
NonLoggingLoggerComputationLogger
21. #### final def ne(arg0: AnyRef): Boolean

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

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

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

Convenient interface for `otherComputation`

Convenient interface for `otherComputation`

Definition Classes
ComputationLogger
25. #### 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.

Some other computation, that might in particular be performed by theory plug-ins.

Definition Classes
NonLoggingLoggerComputationLogger
26. #### 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`).

Definition Classes
NonLoggingLoggerComputationLogger
27. #### 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`).

Definition Classes
NonLoggingLoggerComputationLogger
28. #### 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

Definition Classes
NonLoggingLoggerComputationLogger
29. #### final def synchronized[T0](arg0: ⇒ T0): T0

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

Definition Classes
AnyRef → Any
31. #### 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.

Apply the functional consistency axiom to derive that the results of two function applications (encoded as predicate atoms) must be the same.

Definition Classes
NonLoggingLoggerComputationLogger
32. #### 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

Unify two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise

Definition Classes
NonLoggingLoggerComputationLogger
33. #### final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )