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 for representing formulae whose application is currently blocked. Such formulae are only stored for the time being, until possibly at some later point they can be used (or discarded).
Task responsible for strengthening the inequalities lc + b1 >= 0
and -lc - b2 >= 0
to lc + b1 >= 1
and
-lc - b2 >= 1
, introducing one splinter
Task responsible for strengthening the inequalities lc + b1 >= 0
and -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.
Trait for representing proof tasks that want to be applied as soon as some
condition holds. The prioritisation of such task is right now hardcoded in
TaskManager
.
A class for tracking the application of tasks and recommending the
intermediate application of EagerTask
s.
A class for tracking the application of tasks and recommending the
intermediate application of EagerTask
s. This class is
implemented as a finite automaton to give recommendations based on the
history of task applications
The representation of formulas in a proof goal that are more complex than simple facts.
The representation of formulas in a proof goal that are more complex than simple facts. Such formulas are considered to have positive polarity, i.e., as conjunctions in the succedent of a goal. This class is both responsible for storing such formulas and for eventually processing the formulas, e.g. by splitting up the formulas/proof goal.
Trait for tasks that are
given a priority
, based on the age (to ensure fairness)
and on other criteria to work at different tasks in a meaningful order.
Trait for tasks that are
given a priority
, based on the age (to ensure fairness)
and on other criteria to work at different tasks in a meaningful order.
Tasks with smaller priority
are supposed to be handled first.
Proof tasks of this kind cannot fail, i.e., the result of apply
is simply ProofTree
.
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
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 to assign weights (integers) to constant and predicate symbols. Such weights are used to decide which atoms to split over first
Trait for the future tasks that are stored in a proof goal.
Trait for the future tasks that are stored in a proof goal. Tasks are considered as mappings from proof goals to proof trees, given a factory that is able to construct proof trees and update goals.
An immutable class (priority queue) for handling a set of tasks in a proof goal.
An immutable class (priority queue) for handling a set of tasks in a proof goal. Currently, this is implemented using a sorted set, but it would be better to use a real immutable queue (leftist heap?).
TODO: So far, no real subsumption checks are performed
Wrapper class for formula tasks.
Wrapper class for formula tasks. This is used to handle (theory) propagation when extracting certificates: in this case, all simplifications and reductions have to be done using the basic calculus rules. Reduction of formulae is still used to identify formulae that can be simplified a lot, so that priorities can be chosed in a meaningful way.
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
Class to approximate whether two terms have to be considered as potential aliases, i.e., may have the same value. Two criteria are taken into account for this: arithmetic facts that are available in a proof goal, and constant freedom. The class does caching to speed up queries.