theoryPlugins

Type Members

1. class EagerPluginTask extends PluginTask with EagerTask

   

2. class IntermediatePluginTask extends PluginTask with PrioritisedTask

   

3. trait Plugin extends TheoryProcedure

   

   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

   

   Execution of a sequence of plugins.

5. abstract class PluginTask extends Task

   

   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

   

7. trait TheoryProcedure extends AnyRef

   

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