Packages

class PredConj extends Formula with SortedWithOrder[PredConj]

A class for representing a conjunction of positive and negative predicate literals

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. PredConj
  2. SortedWithOrder
  3. Sorted
  4. Formula
  5. TerFor
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def --(that: PredConj): PredConj
  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  7. lazy val constants: Set[ConstantTerm]
    Definition Classes
    PredConjSortedWithOrderTerFor
  8. def diff(oldConj: PredConj)(implicit fullOrder: TermOrder): (PredConj, PredConj)

    Find the subset of literals in this conjunction that also occur in oldConj, as well as the subset of literals that do not occur in oldConj.

  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(that: Any): Boolean
    Definition Classes
    PredConj → AnyRef → Any
  11. def filter(pred: (Atom) => Boolean): PredConj
  12. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  13. lazy val groundAtoms: Set[Atom]
    Definition Classes
    PredConjFormula
  14. def hashCode(): Int
    Definition Classes
    PredConj → AnyRef → Any
  15. def implies(that: PredConj): Boolean
  16. def isFalse: Boolean

    Return true if this formula is obviously always false.

    Return true if this formula is obviously always false. The only allowed case at this point is that the conjunction contains exactly two literals, the same atom positively and negatively

    Definition Classes
    PredConjFormula
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. def isLiteral: Boolean
  19. def isSortedBy(otherOrder: TermOrder): Boolean
    Definition Classes
    SortedWithOrderSorted
  20. def isTrue: Boolean

    Return true if this formula is obviously always true

    Return true if this formula is obviously always true

    Definition Classes
    PredConjFormula
  21. def iterator: Iterator[PredConj]
  22. def lookupFunctionResult(atom: Atom): Option[LinearCombination]

    Check whether there is a positive literal with the given predicate, and starting with the given arguments, and return the last argument.

  23. def lookupFunctionResult(pred: Predicate, arguments: Seq[LinearCombination]): Option[LinearCombination]

    Check whether there is a positive literal with the given predicate, and starting with the given arguments, and return the last argument.

  24. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  25. def negate: PredConj

    Create the negation of exactly one literal

  26. val negativeLits: IndexedSeq[Atom]
  27. lazy val negativeLitsAsSet: Set[Atom]
  28. def negativeLitsWithPred(pred: Predicate): IndexedSeq[Atom]
  29. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  30. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  31. val order: TermOrder
    Definition Classes
    PredConjSortedWithOrder
  32. def partition(pred: (Atom) => Boolean): (PredConj, PredConj)
  33. val positiveLits: IndexedSeq[Atom]
  34. lazy val positiveLitsAsSet: Set[Atom]
  35. def positiveLitsWithPred(pred: Predicate): IndexedSeq[Atom]
  36. lazy val predicates: Set[Predicate]
    Definition Classes
    PredConjSortedWithOrderTerFor
  37. def size: Int
  38. def sortBy(newOrder: TermOrder): PredConj

    Re-sort an object with a new TermOrder.

    Re-sort an object with a new TermOrder. It is guaranteed that the result isSortedBy(order)

    Definition Classes
    PredConjSorted
  39. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  40. def toString(): String
    Definition Classes
    PredConj → AnyRef → Any
  41. def unary_!: PredConj
  42. def updateLits(newPosLits: IndexedSeq[Atom], newNegLits: IndexedSeq[Atom])(implicit newOrder: TermOrder): PredConj
  43. def updateLits(newPosLits: IndexedSeq[Atom], newNegLits: IndexedSeq[Atom], logger: ComputationLogger)(implicit newOrder: TermOrder): PredConj

    Update the literals of this conjunction; if nothing has changed, the old object is returned

  44. def updateLitsSubset(newPosLits: IndexedSeq[Atom], newNegLits: IndexedSeq[Atom], newOrder: TermOrder): PredConj

    Update the atoms of this conjunction under the assumption that the new atoms form a subset of the old atoms

  45. lazy val variables: Set[VariableTerm]
    Definition Classes
    PredConjTerFor
  46. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  47. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  48. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from SortedWithOrder[PredConj]

Inherited from Sorted[PredConj]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped