class LoggingBranchInferenceCollector extends BranchInferenceCollector
Mutable datastructure for collecting inferences during some computation. To avoid having to pass around collectors all over the place, a dynamic variable is used to realise context collectors.
- Alphabetic
- By Inheritance
- LoggingBranchInferenceCollector
- BranchInferenceCollector
- ComputationLogger
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
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
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val ceScope: LogScope[(Seq[(IdealInt, LinearCombination)], TermOrder), (LinearCombination, LinearCombination)]
Convenient interface for
combineEquationsConvenient interface for
combineEquations- Definition Classes
- ComputationLogger
- val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]
Convenient interface for
combineInequalitiesConvenient interface for
combineInequalities- Definition Classes
- ComputationLogger
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def columnReduce(oldSymbol: ConstantTerm, newSymbol: ConstantTerm, newSymbolDef: LinearCombination, subst: Boolean, newOrder: TermOrder): Unit
Inference corresponding to an application of the
col-redorcol-red-substrule.Inference corresponding to an application of the
col-redorcol-red-substrule. This will simply introduce a new constantnewSymbolthat is defined as the termnewSymbolDef.This method is not added in the
ComputationLogger, because it is never used in the ter/for datastructures.- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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.- Definition Classes
- LoggingBranchInferenceCollector → ComputationLogger
- 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.Given the two formulae
t >= 0andt != 0(or, similarly,t >= 0and-t != 0), infer the inequalityt-1 >= 0.- Definition Classes
- LoggingBranchInferenceCollector → ComputationLogger
- 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.
An inference that turns a universally quantified divisibility constraint into an existentially quantified disjunction of equations.
- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- 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 getCollection: BranchInferenceCollection
- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- var inferences: List[BranchInference]
- 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.newConstantsare the constants introduced to instantiate the quantifiers, starting with the innermost instantiated quantifier.- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val isLogging: Boolean
- Definition Classes
- LoggingBranchInferenceCollector → ComputationLogger
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def newCertFormula(f: CertFormula): Unit
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- def newFormula(f: Conjunction): Unit
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
- Definition Classes
- LoggingBranchInferenceCollector → BranchInferenceCollector
- 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
otherComputationConvenient interface for
otherComputation- Definition Classes
- ComputationLogger
- def otherComputation(assumptions: Seq[Formula], result: Formula, order: TermOrder, theoryAnyRef: 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- LoggingBranchInferenceCollector → AnyRef → Any
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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
- LoggingBranchInferenceCollector → ComputationLogger
- 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)