class NonLoggingLogger extends ComputationLogger
- Alphabetic
- By Inheritance
- NonLoggingLogger
- ComputationLogger
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new NonLoggingLogger()
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
- NonLoggingLogger → 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 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
- NonLoggingLogger → 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
- NonLoggingLogger → 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
- NonLoggingLogger → 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
- NonLoggingLogger → ComputationLogger
- 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 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
- NonLoggingLogger → ComputationLogger
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val isLogging: Boolean
- Definition Classes
- NonLoggingLogger → ComputationLogger
- 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
- 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
- NonLoggingLogger → 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
- NonLoggingLogger → 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
- NonLoggingLogger → 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
- NonLoggingLogger → ComputationLogger
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- 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
- NonLoggingLogger → 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
- NonLoggingLogger → 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)