LoggingBranchInferenceCollector
Related Docs:
object LoggingBranchInferenceCollector
| package certificates
Turn two complementary inequalities into an equation
Turn two complementary inequalities into an equation
Convenient interface for combineEquations
Convenient interface for combineEquations
Convenient interface for combineInequalities
Convenient interface for combineInequalities
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.
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
Fourier-Motzkin Inference.
Fourier-Motzkin Inference. The given terms shall be primitive, and the result will be implicitly rounded
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.
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.
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.
Instantiate a universally quantified formula with ground terms
Instantiate a universally quantified formula with ground terms
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.
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)
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)
Convenient interface for otherComputation
Convenient interface for otherComputation
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.
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).
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).
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
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.
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
(Since version ) see corresponding Javadoc for more information.
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.