case class ElimPredModelElement(_preds: Set[Predicate]) extends ModelElement with Product with Serializable
Class for storing information about eliminated predicates, without giving a precise description how their value can be reconstructed. This is currently used for "abbreviations", which are eliminated from proof branches when it becomes clear that they will never be expanded.
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- ElimPredModelElement
- Serializable
- Product
- Equals
- ModelElement
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
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 _preds: Set[Predicate]
- 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(constModel: 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
- ElimPredModelElement → 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)