NIASplitter

Instance Constructors

new NIASplitter(gbCache: GBCache)

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[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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: Any): 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[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
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()
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 consideredPredicates and in atoms constructed using predicates not in theoryPredicates.
Find constants that occur both in atoms constructed using predicates from consideredPredicates and in atoms constructed using predicates not in theoryPredicates. 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()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
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( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Doc: package nia

class NIASplitter extends TheoryProcedure

Instance Constructors

new NIASplitter(gbCache: GBCache)

Type Members

class RichActionSeq extends AnyRef

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def binarySplit(intervalSet: IntervalSet, targetSet: Seq[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]

def clone(): AnyRef

def discreteSplit(intervalSet: IntervalSet, targetSet: Seq[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def gapSplit(intervalSet: IntervalSet, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]

final def getClass(): Class[_]

def goalState(goal: Goal): proof.theoryPlugins.Plugin.GoalState.Value

def handleGoal(goal: Goal): Seq[Action]

def hashCode(): Int

def infinitySplit(intervalSet: IntervalSet, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]

def interfaceConstants(goal: Goal, consideredPredicates: Set[Predicate], theoryPredicates: Set[Predicate]): Set[ConstantTerm]

def interfaceConstants(goal: Goal, theoryPredicates: Set[Predicate]): Set[ConstantTerm]

final def isInstanceOf[T0]: Boolean

def linearizers(predicates: List[Atom], intervalSet: IntervalSet)(implicit order: TermOrder): Set[ConstantTerm]

final def ne(arg0: AnyRef): Boolean

def negeqSplit(intervalSet: IntervalSet, negeqs: NegEquationConj, targetSet: Set[ConstantTerm])(implicit order: TermOrder): Iterator[(Seq[ArithConj], String, BitSet, Seq[Action], Boolean)]

final def notify(): Unit

final def notifyAll(): Unit

implicit def richActionSeq(acts: Seq[Action]): RichActionSeq

def splitTermAt(x: ConstantTerm, mid: IdealInt, swap: Boolean = false)(implicit order: TermOrder): Seq[Action]

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

def updateProcedure(goal: Goal, factCollector: (Conjunction) ⇒ Unit): Option[Seq[(TheoryProcedure, Int)]]

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from TheoryProcedure

Inherited from AnyRef

Inherited from Any

Ungrouped