Trait

util.sat

CnfLike

Related Doc: package sat

Permalink

trait CnfLike extends AnyRef

An interface for building formulas in conjunctive normal form.

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

Type Members

  1. final case class Clause(lits: List[Int]) extends Product with Serializable

    Permalink

    A clause.

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. final def addClause(lits: Int*)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a collection of literals as a clause to the solver.

    Adds a collection of literals as a clause to the solver.

    returns

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

  5. def addClauseImplem(lits: List[Int]): Unit

    Permalink

    Method to use to effectively add a clause to the underlying Solver implementation.

  6. final def addClauseList(lits: List[Int])(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Adds a list of literals as a clause to the solver.

    Adds a list of literals as a clause to the solver.

    returns

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

  7. final def addHeaderComment(comment: String): Unit

    Permalink

    Add a header comment in the formula.

  8. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  9. final def clauses: Iterator[(Clause, Option[Int])]

    Permalink

    returns

    an iterator on the clauses currently in the solver.

  10. def clone(): AnyRef

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

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

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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. def freeze(lit: Int): CnfLike.this.type

    Permalink

    Freeze the variable underlying the literal.

  15. final def freshVar(howmany: Int): Int

    Permalink

    Reserve

    Reserve

    howmany

    variables to express the problem, reserving dimacs variables identifiers in [1, howmany]. Next fresh variables identifiers will start at

    howmany+1

    howmany }}} Next fresh variables identifiers will start at

    howmany+1
    howmany

    number of variables to create

    returns

    The total variables used in the solver.

  16. final def freshVar: Int

    Permalink

    Creates a fresh variable in the solver.

    Creates a fresh variable in the solver.

    returns

    the number of variables created in the solver so far, equal to the fresh variable identifier.

  17. def freshVarImplem(superRes: Int): Int

    Permalink

    Method to implement to effectively create a fresh var in the underlying representation.

  18. def freshVarImplem(superRes: Int, howmany: Int): Int

    Permalink

    Method to implement to effectively create a fresh var in the underlying representation.

  19. final def getClass(): Class[_]

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

    Permalink
    Definition Classes
    AnyRef → Any
  21. final def headerComments: Iterator[String]

    Permalink

    returns

    Iterator over all header comments, in insertion order.

  22. def isFrozen(lit: Int): Boolean

    Permalink

    True iff the variable is frozen.

  23. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  24. final def mkSwitchLit(switch: Option[Int], switchable: Boolean): Option[Int]

    Permalink

    Returns a switching literal: if switch is Some( s ), returns this Some( s ), else if switchable is true, returns a Some( newSwitch ) else returns None.

  25. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  26. final def nofClauses: Int

    Permalink

    returns

    the number of clauses of the formula.

  27. final def nofVars: Int

    Permalink

    returns

    the number of variables created using freshVar

  28. final def notify(): Unit

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

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

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

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

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped