Object/Trait

ap.proof.theoryPlugins

Plugin

Related Docs: trait Plugin | package theoryPlugins

Permalink

object Plugin

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Plugin
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. sealed abstract class Action extends AnyRef

    Permalink
  2. case class AddAxiom(assumptions: Seq[Formula], axiom: Conjunction, theory: Theory) extends Action with Product with Serializable

    Permalink

    Add an explicit theory axiom.

    Add an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom and assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.

  3. case class AddFormula(formula: Conjunction) extends Action with Product with Serializable

    Permalink

    Add a formula to the handled proof goal.

    Add a formula to the handled proof goal. This action does not support generation of proof certificates.

  4. case class AddReducableModelElement(facts: Conjunction, constants: Set[ConstantTerm], reducerSettings: ReducerSettings) extends Action with Product with Serializable

    Permalink

    Record that values of the given constants can be reconstructed from the provided facts.

  5. case class AxiomSplit(assumptions: Seq[Formula], cases: Seq[(Conjunction, Seq[Action])], theory: Theory) extends Action with Product with Serializable

    Permalink

    Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom.

    Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom, but already assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.

  6. case class CloseByAxiom(assumptions: Seq[Formula], theory: Theory) extends Action with Product with Serializable

    Permalink

    Close the goal by invoking an explicit theory axiom.

    Close the goal by invoking an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom and assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.

  7. case class RemoveFacts(facts: Conjunction) extends Action with Product with Serializable

    Permalink

    Remove some facts from the handled proof goal.

  8. case class ScheduleTask(proc: TheoryProcedure, priority: Int) extends Action with Product with Serializable

    Permalink

    Schedule a task to be applied later on the goal.

  9. case class SplitDisequality(equality: LinearCombination, leftActions: Seq[Action], rightActions: Seq[Action]) extends Action with Product with Serializable

    Permalink

    Split a disequality fact into two inequalities.

  10. case class SplitGoal(cases: Seq[Seq[Action]]) extends Action with Product with Serializable

    Permalink

    Split a proof goal into multiple sub-goals.

    Split a proof goal into multiple sub-goals. This action does not support generation of proof certificates.

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. val AC: AC_PLUGIN.type

    Permalink
    Attributes
    protected[ap.proof.theoryPlugins]
  5. object GoalState extends Enumeration

    Permalink
  6. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  7. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  8. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  12. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  13. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  14. def isRelevantAxiomAction(action: Action, order: TermOrder): Boolean

    Permalink

    A simple relevance filter to get rid of axioms that follow trivially from built-in arithmetic rules.

    A simple relevance filter to get rid of axioms that follow trivially from built-in arithmetic rules. Such irrelevant axioms should not be added, since they might interfere with the built-in simplification rules, and sometimes lead to illformed proofs.

  15. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  16. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  17. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  18. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  19. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  20. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  21. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped