trait BranchInferenceCollector extends ComputationLogger
- Alphabetic
- By Inheritance
- BranchInferenceCollector
- 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
Turn two complementary inequalities into an equation
- Definition Classes
- ComputationLogger
- abstract 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. - 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
- 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
- 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.- Definition Classes
- ComputationLogger
- 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.Given the two formulae
t >= 0andt != 0(or, similarly,t >= 0and-t != 0), infer the inequalityt-1 >= 0.- Definition Classes
- ComputationLogger
- 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.
- abstract def getCollection: BranchInferenceCollection
- 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
- 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.newConstantsare the constants introduced to instantiate the quantifiers, starting with the innermost instantiated quantifier. - abstract val isLogging: Boolean
- Definition Classes
- ComputationLogger
- abstract def newCertFormula(f: CertFormula): Unit
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
- abstract def newFormula(f: Conjunction): Unit
Inform the collector that a new formula has occurred on the branch (important for alpha-rules)
- 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
- 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
- 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
- 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
- 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
- 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
- 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
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()
- 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
otherComputationConvenient interface for
otherComputation- Definition Classes
- ComputationLogger
- 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)