Package

ap.proof

theoryPlugins

Permalink

package theoryPlugins

Visibility
  1. Public
  2. All

Type Members

  1. class EagerPluginTask extends PluginTask with EagerTask

    Permalink
  2. class IntermediatePluginTask extends PluginTask with PrioritisedTask

    Permalink
  3. trait Plugin extends TheoryProcedure

    Permalink

    Interface for theory plugins that can be added to the EagerTaskManager.

    Interface for theory plugins that can be added to the EagerTaskManager. At the moment, such plugins can mainly observe which formulae are asserted on a branch, and then generate/instantiate further axioms to add theory knowledge.

    Plugin objects have to be immutable.

  4. class PluginSequence extends Plugin

    Permalink

    Execution of a sequence of plugins.

  5. abstract class PluginTask extends Task

    Permalink

    Task integrating a Plugin (or TheoryProcedure) into a prover

    Task integrating a Plugin (or TheoryProcedure) into a prover

  6. class PrioritisedPluginTask extends PluginTask with PrioritisedTask

    Permalink
  7. trait TheoryProcedure extends AnyRef

    Permalink

    General interface for a theory-specific procedure that can be applied by a prover to reason about interpreted symbols.

Value Members

  1. object IntermediatePluginTask

    Permalink
  2. object Plugin

    Permalink
  3. object PluginSequence

    Permalink
  4. object PluginTask

    Permalink

Ungrouped