Type Members

1.  class AddFactsTask extends FormulaTask
2.  class AliasAnalyser extends AliasChecker

   Class to approximate whether two terms have to be considered as potential aliases, i.e., may have the same value.

   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.

3.  class AllQuantifierTask extends QuantifierTask
4.  class BetaFormulaTask extends FormulaTask
5.  abstract class BlockedFormulaTask extends FormulaTask

   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).

6.  class BoundStrengthenTask extends PrioritisedTask

   Task responsible for strengthening the inequalities lc + b1 >= 0 and -lc - b2 >= 0 to lc + b1 >= 1 and -lc - b2 >= 1, introducing one splinter

7.  case class CompoundFormulas(qfClauses: NegatedConjunctions, eagerQuantifiedClauses: IterativeClauseMatcher, lazyQuantifiedClauses: IterativeClauseMatcher) extends Sorted[CompoundFormulas] with Product with Serializable
8.  abstract class CountingTaskAggregator[Key] extends TaskAggregator

   Aggregator that counts the number of occurrences of certain objects in a prioritised task (e.g., the number of constant symbol occurrences).

9.  class DivisibilityTask extends FormulaTask
10.  trait EagerTask extends Task

    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.

11.  class EagerTaskAutomaton extends AnyRef
12.  abstract class EagerTaskManager extends AnyRef

    A class for tracking the application of tasks and recommending the intermediate application of EagerTasks.

    A class for tracking the application of tasks and recommending the intermediate application of EagerTasks. This class is implemented as a finite automaton to give recommendations based on the history of task applications

13.  class ExQuantifierTask extends QuantifierTask
14.  abstract class FormulaTask extends PrioritisedTask

    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.

15.  class Goal extends ProofTree
16.  class LazyMatchTask extends PrioritisedTask
17.  class NegLitClauseTask extends FormulaTask
18.  abstract class PairCountingTaskAggregator[Key1, Key2] extends TaskAggregator

    Aggregator that counts the number of occurrences of two kinds of objects in a prioritised task.

19.  trait PrioritisedTask extends Task

    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.

20.  abstract class QuantifierTask extends FormulaTask
21.  class RegularityBlockedTask extends BlockedFormulaTask

    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

22.  trait SymbolWeights extends AnyRef

    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

23.  trait Task extends AnyRef

    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.

24.  trait TaskAggregator extends AnyRef

    Class to compute summary information about the prioritised tasks in a goal.

25.  class TaskManager extends AnyRef

    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. This is implemented using a leftist heap.

    TODO: So far, no subsumption checks are performed

26.  class UpdateConstantFreedomTask extends PrioritisedTask
27.  class VectorTaskAggregator extends TaskAggregator

    A task aggregator that combines several sub-aggregators.

28.  case class WrappedFormulaTask(realTask: FormulaTask, simplifiedTasks: Seq[FormulaTask]) extends FormulaTask with Product with Serializable

    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.