object ModPlugin extends Plugin
- Alphabetic
- By Inheritance
- ModPlugin
- Plugin
- TheoryProcedure
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- class RichActionSeq extends AnyRef
- Definition Classes
- TheoryProcedure
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def computeModel(goal: Goal): Seq[Action]
Apply this procedure to the given goal in model-generation mode.
Apply this procedure to the given goal in model-generation mode. In this mode, we have already established that a problem is satisfiable, but still need to compute a full/concrete model.
- Definition Classes
- Plugin
- def enumIntValuesOf(t: Term, order: TermOrder): Formula
Generate an assertion that will cause all values of the given term to be enumerated explicitly.
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def goalState(goal: Goal): proof.theoryPlugins.Plugin.GoalState.Value
From a theory procedure, determine in which state a given goal is.
From a theory procedure, determine in which state a given goal is.
- Definition Classes
- TheoryProcedure
- def handleGoal(goal: Goal): Seq[Action]
Apply this plugin to the given goal.
Apply this plugin to the given goal.
- Definition Classes
- ModPlugin → Plugin → TheoryProcedure
- def hasImpliedIneqConstraints(c: ConstantTerm, lower: IdealInt, upper: IdealInt, ineqs: InEqConj): Boolean
Check whether all inequalities present for the given constants are already implied by the type
Check whether all inequalities present for the given constants are already implied by the type
- Attributes
- protected[bitvectors]
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def interfaceConstants(goal: Goal, consideredPredicates: Set[Predicate], theoryPredicates: Set[Predicate]): Set[ConstantTerm]
Find constants that occur both in atoms constructed using predicates from
consideredPredicatesand in atoms constructed using predicates not intheoryPredicates.Find constants that occur both in atoms constructed using predicates from
consideredPredicatesand in atoms constructed using predicates not intheoryPredicates. Arithmetic facts (equations, disequations, inequalities) in a goal are not considered, but arithmetic clauses are included.- Definition Classes
- TheoryProcedure
- def interfaceConstants(goal: Goal, theoryPredicates: Set[Predicate]): Set[ConstantTerm]
Find constants that occur both in atoms constructed using theory predicates and in atoms constructed using non-theory predicates.
Find constants that occur both in atoms constructed using theory predicates and in atoms constructed using non-theory predicates. Arithmetic facts (equations, disequations, inequalities) in a goal are not considered, but arithmetic clauses are included.
- Definition Classes
- TheoryProcedure
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- implicit def richActionSeq(acts: Seq[Action]): RichActionSeq
An implicit function to simplify cascading of possible actions.
An implicit function to simplify cascading of possible actions.
- Attributes
- protected
- Definition Classes
- TheoryProcedure
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- ModPlugin → AnyRef → Any
- def updateProcedure(goal: Goal, factCollector: (Conjunction) => Unit): Option[Seq[(TheoryProcedure, Int)]]
Optionally update the task with possibly new information from the goal.
Optionally update the task with possibly new information from the goal.
- Definition Classes
- TheoryProcedure
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)