case class EqModelElement(eqs: EquationConj, _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
- EqModelElement
- Serializable
- Product
- Equals
- ModelElement
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Instance Constructors
- new EqModelElement(eqs: EquationConj, _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]
- 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
- val eqs: EquationConj
- 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
- EqModelElement → 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)