Package

ap.proof

goal

Permalink

package goal

Visibility
  1. Public
  2. All

Type Members

  1. class AddFactsTask extends FormulaTask

    Permalink
  2. class AliasAnalyser extends AliasChecker

    Permalink

    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

    Permalink
  4. class BetaFormulaTask extends FormulaTask

    Permalink
  5. abstract class BlockedFormulaTask extends FormulaTask

    Permalink

    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

    Permalink

    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

    Permalink
  8. abstract class CountingTaskAggregator[Key] extends TaskAggregator

    Permalink

    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

    Permalink
  10. trait EagerTask extends Task

    Permalink

    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

    Permalink
  12. abstract class EagerTaskManager extends AnyRef

    Permalink

    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

    Permalink
  14. abstract class FormulaTask extends PrioritisedTask

    Permalink

    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

    Permalink
  16. class LazyMatchTask extends PrioritisedTask

    Permalink
  17. class NegLitClauseTask extends FormulaTask

    Permalink
  18. abstract class PairCountingTaskAggregator[Key1, Key2] extends TaskAggregator

    Permalink

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

  19. trait PrioritisedTask extends Task

    Permalink

    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

    Permalink
  21. class RegularityBlockedTask extends BlockedFormulaTask

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

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

  25. class TaskManager extends AnyRef

    Permalink

    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

    Permalink
  27. class VectorTaskAggregator extends TaskAggregator

    Permalink

    A task aggregator that combines several sub-aggregators.

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

    Permalink

    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.

Value Members

  1. object AddFactsTask

    Permalink
  2. object AliasAnalyser

    Permalink
  3. object AllQuantifierTask

    Permalink
  4. object BetaFormulaTask

    Permalink
  5. object BlockedFormulaTask

    Permalink
  6. object BoundStrengthenTask

    Permalink
  7. object CompoundFormulas extends Serializable

    Permalink
  8. object CountingTaskAggregator

    Permalink
  9. object DivisibilityTask

    Permalink
  10. object EagerMatchTask extends EagerTask with Product with Serializable

    Permalink
  11. object EagerTaskAutomaton

    Permalink
  12. object EliminateFactsTask extends EagerTask with Product with Serializable

    Permalink

    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.

  13. object ExQuantifierTask

    Permalink
  14. object FactsNormalisationTask extends EagerTask with Product with Serializable

    Permalink
  15. object FormulaTask

    Permalink
  16. object Goal

    Permalink
  17. object LazyMatchTask

    Permalink
  18. object MatchTasks

    Permalink
  19. object NegLitClauseTask

    Permalink
  20. object OmegaTask extends EagerTask with Product with Serializable

    Permalink

    Task for eliminating inequalities using the equivalence from the Omega-test

  21. object PairCountingTaskAggregator

    Permalink
  22. object QuantifierTask

    Permalink
  23. object RegularityBlockedTask

    Permalink
  24. object SymbolWeights

    Permalink
  25. object TaskAggregator

    Permalink
  26. object TaskManager

    Permalink
  27. object UpdateTasksTask extends EagerTask with Product with Serializable

    Permalink

    Meta-Task for updating all tasks of a goal

  28. object WrappedFormulaTask extends Serializable

    Permalink

Ungrouped