case class InNegEqModelElement(ac: ArithConj, _cs: Set[ConstantTerm]) extends ModelElement with Product with Serializable
Class for creating models (assignments of
integer literals to constants) of Formula, for certain
special cases. This class is used in EliminateFactsTask
Linear Supertypes
Ordering
- Alphabetic
 - By Inheritance
 
Inherited
- InNegEqModelElement
 - Serializable
 - Product
 - Equals
 - ModelElement
 - AnyRef
 - Any
 
- Hide All
 - Show All
 
Visibility
- Public
 - Protected
 
Instance Constructors
-  new InNegEqModelElement(ac: ArithConj, _cs: Set[ConstantTerm])
 
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
 
 -  val _cs: Set[ConstantTerm]
 -  val ac: ArithConj
 -   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()
 
 -    val cs: Set[ConstantTerm]
- Definition Classes
 - ModelElement
 
 -   final  def eq(arg0: AnyRef): Boolean
- Definition Classes
 - AnyRef
 
 -    def extendModel(model: HashMap[ConstantTerm, IdealInt], predModel: HashMap[Atom, Boolean], order: TermOrder): Unit
Extend the given model, in such a way that the conditions of this model element are satisfied.
Extend the given model, in such a way that the conditions of this model element are satisfied.
- Definition Classes
 - InNegEqModelElement → ModelElement
 
 -   final  def getClass(): Class[_ <: AnyRef]
- Definition Classes
 - AnyRef → Any
 - Annotations
 - @HotSpotIntrinsicCandidate() @native()
 
 -   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()
 
 -    val preds: Set[Predicate]
- Definition Classes
 - ModelElement
 
 -    def productElementNames: Iterator[String]
- Definition Classes
 - Product
 
 -   final  def synchronized[T0](arg0: => T0): T0
- Definition Classes
 - AnyRef
 
 -   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)