# BranchInferenceCollector

### Related Doc: package certificates

#### trait BranchInferenceCollector extends ComputationLogger

Linear Supertypes
ComputationLogger, AnyRef, Any
Known Subclasses
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. BranchInferenceCollector
2. ComputationLogger
3. AnyRef
4. 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

Turn two complementary inequalities into an equation

Definition Classes
ComputationLogger
2. #### abstract def columnReduce(oldSymbol: ConstantTerm, newSymbol: ConstantTerm, newSymbolDef: LinearCombination, subst: Boolean, newOrder: TermOrder): Unit

Inference corresponding to an application of the `col-red` or `col-red-subst` rule.

Inference corresponding to an application of the `col-red` or `col-red-subst` rule. This will simply introduce a new constant `newSymbol` that is defined as the term `newSymbolDef`.

This method is not added in the `ComputationLogger`, because it is never used in the ter/for datastructures.

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

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

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

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

Definition Classes
ComputationLogger
7. #### abstract def divRight(divisibility: Conjunction, result: Conjunction, order: TermOrder): Unit

An inference that turns a universally quantified divisibility constraint into an existentially quantified disjunction of equations.

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

Instantiate a universally quantified formula with ground terms

Definition Classes
ComputationLogger
10. #### abstract def instantiateQuantifier(quantifiedFormula: Conjunction, newConstants: Seq[ConstantTerm], result: Conjunction, order: TermOrder): Unit

Inference corresponding to applications of the rules `all-left`, `ex-left`, etc.

Inference corresponding to applications of the rules `all-left`, `ex-left`, etc. A uniform prefix of quantifiers (only forall or only exists) is instantiated with a single inference. `newConstants` are the constants introduced to instantiate the quantifiers, starting with the innermost instantiated quantifier.

11. #### abstract val isLogging: Boolean

Definition Classes
ComputationLogger
12. #### abstract def newCertFormula(f: CertFormula): Unit

Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

13. #### abstract def newFormula(f: Conjunction): Unit

Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

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

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

Definition Classes
ComputationLogger
15. #### 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`).

Definition Classes
ComputationLogger
16. #### 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`).

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

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

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

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

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
ComputationLogger

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

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

Convenient interface for `combineInequalities`

Convenient interface for `combineInequalities`

Definition Classes
ComputationLogger
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`

Definition Classes
ComputationLogger
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( ... )