goal

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

   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

    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.