class NIASplitter extends TheoryProcedure
Splitter handles the splitting when no new information can be deduced
- Alphabetic
- By Inheritance
- NIASplitter
- 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 binarySplit(intervalSet: IntervalSet, targetSet: Seq[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]
Splitting of intervals in the middle
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def discreteSplit(intervalSet: IntervalSet, targetSet: Seq[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]
Finds a possible split of x in [a, b] into the individual cases x = a, x = a + 1, ..., x = b
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def gapSplit(intervalSet: IntervalSet, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]
Utilizes any gaps in an interval (i.e.
Utilizes any gaps in an interval (i.e. x = [lb, -a] U [a, ub]) and branches into two (i.e. x <= -a V x >= a)
- 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 procedure to the given goal.
Apply this procedure to the given goal.
- Definition Classes
- NIASplitter → TheoryProcedure
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def infinitySplit(intervalSet: IntervalSet, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]
Splits intervals that ranges from -Inf to +Inf on zero
- 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
- def linearizers(predicates: List[Atom], intervalSet: IntervalSet)(implicit order: TermOrder): Set[ConstantTerm]
Here follow the different splitting strategies.
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def negeqSplit(intervalSet: IntervalSet, negeqs: NegEquationConj, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]
Takes negative equations (i.e.
Takes negative equations (i.e. x+y+... != 0) and splits them around zero
- 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
- def splitTermAt(x: ConstantTerm, mid: IdealInt, swap: Boolean = false)(implicit order: TermOrder): Seq[Action]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- NIASplitter → 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)