NonLoggingLogger
Related Doc:
package ComputationLogger
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 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.
Instantiate a universally quantified formula with ground terms
Instantiate a universally quantified formula with ground terms
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.