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. class DivisibilityTask extends FormulaTask

    Permalink
  9. 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.

  10. class EagerTaskAutomaton extends AnyRef

    Permalink
  11. 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

  12. class ExQuantifierTask extends QuantifierTask

    Permalink
  13. 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.

  14. class Goal extends ProofTree

    Permalink
  15. class LazyMatchTask extends PrioritisedTask

    Permalink
  16. class NegLitClauseTask extends FormulaTask

    Permalink
  17. 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.

  18. abstract class QuantifierTask extends FormulaTask

    Permalink
  19. 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

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

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

  22. class TaskInfoCollector extends HeapCollector[Task, TaskInfoCollector]

    Permalink
  23. 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. 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

  24. class UpdateConstantFreedomTask extends PrioritisedTask

    Permalink
  25. 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 DivisibilityTask

    Permalink
  9. object EagerMatchTask extends EagerTask with Product with Serializable

    Permalink
  10. object EagerTaskAutomaton

    Permalink
  11. 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.

  12. object ExQuantifierTask

    Permalink
  13. object FactsNormalisationTask extends EagerTask with Product with Serializable

    Permalink
  14. object FormulaTask

    Permalink
  15. object Goal

    Permalink
  16. object LazyMatchTask

    Permalink
  17. object NegLitClauseTask

    Permalink
  18. object OmegaTask extends EagerTask with Product with Serializable

    Permalink

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

  19. object QuantifierTask

    Permalink
  20. object RegularityBlockedTask

    Permalink
  21. object SymbolWeights

    Permalink
  22. object TaskInfoCollector

    Permalink
  23. object TaskManager

    Permalink
  24. object UpdateTasksTask extends EagerTask with Product with Serializable

    Permalink

    Meta-Task for updating all tasks of a goal

  25. object WrappedFormulaTask extends Serializable

    Permalink

Ungrouped