Class to approximate whether two terms have to be considered as potential aliases, i.e., may have the same value.
Task for representing formulae whose application is currently blocked.
Task responsible for strengthening the inequalities
lc + b1 >= 0
-lc - b2 >= 0 to
lc + b1 >= 1 and
-lc - b2 >= 1, introducing one splinter
Trait for representing proof tasks that want to be applied as soon as some condition holds.
A class for tracking the application of tasks and recommending the
intermediate application of
The representation of formulas in a proof goal that are more complex than simple facts.
Trait for tasks that are
priority, based on the age (to ensure fairness)
and on other criteria to work at different tasks in a meaningful order.
Formulae of the shape
t1 = 0 & ... & tn = 0 & !(s1 = 0 & ... & sm = 0)
that are blocked because the equations
t1 = 0 & ... & tn = 0 & s1 = 0 & ... & sm = 0
would reduce the facts of a goal to a mere subset
Trait to assign weights (integers) to constant and predicate symbols.
Trait for the future tasks that are stored in a proof goal.
An immutable class (priority queue) for handling a set of tasks in a proof goal.
Wrapper class for formula tasks.
Task for removing facts that are no longer needed (like equations that have been applied to all other formulas), or that can be discharged directly by moving them into the contraint.
Task for eliminating inequalities using the equivalence from the Omega-test
Meta-Task for updating all tasks of a goal