Trait

util.sat

PseudoBooleanLike

Related Doc: package sat

Permalink

trait PseudoBooleanLike extends AnyRef

An interface for building pseudo-boolean problems on top of CNF formulas.

Self Type
PseudoBooleanLike with CnfLike with CircuitLike
Linear Supertypes
AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. PseudoBooleanLike
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. final case class Card(lits: List[Int], relOp: (PseudoBooleanLike.this)#RelOp, k: Int) extends (PseudoBooleanLike.this)#PseudoBoolCst with Product with Serializable

    Permalink

    A cardinality constraint of the form

    A cardinality constraint of the form

    sum(lits) relop k

    . sum(lits) relop k }}}

  2. final case class ClassicPBCst(lits: List[Int], relOp: (PseudoBooleanLike.this)#RelOp, k: Int, weights: Map[Int, Int]) extends (PseudoBooleanLike.this)#PseudoBoolCst with Product with Serializable

    Permalink

    A classic PB constraint f the form

    A classic PB constraint f the form

    sum(weights(lit)*lit) relop k

    . sum(weights(lit)*lit) relop k }}}

  3. sealed trait PseudoBoolCst extends AnyRef

    Permalink
  4. sealed trait RelOp extends AnyRef

    Permalink

    Abstract type for relational operators used in cardinality constraints.

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. object AtLeast extends (PseudoBooleanLike.this)#RelOp with Product with Serializable

    Permalink
  5. object AtMost extends (PseudoBooleanLike.this)#RelOp with Product with Serializable

    Permalink
  6. object Exactly extends (PseudoBooleanLike.this)#RelOp with Product with Serializable

    Permalink
  7. final def addAtLeastK(lits: List[Int], k: Int)(implicit switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a cardinality constraint

    Adds a cardinality constraint

    sum(lits) >= k

    .

    sum(lits) >= k }}}

    switchable

    optionally add a masking literal that allows to switch the clause on and off

    returns

    if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.

  8. final def addAtMostK(lits: List[Int], k: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a cardinality constraint

    Adds a cardinality constraint

    sum(lits) <= k

    .

    sum(lits) <= k }}}

    switchable

    optionally add a masking literal that allows to switch the clause on and off

    returns

    if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.

  9. final def addAtMostKGate(lits: List[Int], k: Int)(implicit switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

  10. final def addCard(c: (PseudoBooleanLike.this)#Card)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a cardinality constraint with specified relop and constant to the solver.

    Adds a cardinality constraint with specified relop and constant to the solver.

    switch

    optional switch literal

    switchable

    if true and if switch is None, creates a fresh switch literal that allows to switch the constraint on and off

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.

  11. def addCardImplem(c: (PseudoBooleanLike.this)#Card): Unit

    Permalink

    Method to use to effectively add a cardinality constraint to the underlying Solver implementation.

  12. final def addExactlyK(lits: List[Int], k: Int)(implicit switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a cardinality constraint

    Adds a cardinality constraint

    sum(lits) <= k

    .

    sum(lits) <= k }}}

    switchable

    optionally add a masking literal that allows to switch the clause on and off

    returns

    if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.

  13. final def addPbCst(c: (PseudoBooleanLike.this)#ClassicPBCst)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink
  14. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  15. final def cards: Iterator[((PseudoBooleanLike.this)#PseudoBoolCst, Option[Int])]

    Permalink

    returns

    an iterator on the cardinality constraints currently in the solver.

  16. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  17. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  18. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  19. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  20. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  21. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  22. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  23. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  24. final def nofPBCst: Int

    Permalink

    returns

    the number of cardinality constraints of the formula.

  25. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  26. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  27. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  28. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  29. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped