Class

util.sat

DualRailEncoder

Related Doc: package sat

Permalink

case class DualRailEncoder(source: FormulaLike, target: FormulaLike) extends Product with Serializable

Implements the dual-rail transformation at clause level. Does not split variables that are frozen in the source formula, and freezes them in the target formula.

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DualRailEncoder
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new DualRailEncoder(source: FormulaLike, target: FormulaLike)

    Permalink

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. def apply(lit: Int): Int

    Permalink

    Returns the dual rail encoded variable.

  5. def apply(lits: List[Int]): List[(Int, Int)]

    Permalink

    Generates dual-rail variables for a list of literals (allows to control which indices ranges will be occupied by dual rail lits).

    Generates dual-rail variables for a list of literals (allows to control which indices ranges will be occupied by dual rail lits). Must be called before encode() to guarantee intended control over the dual-rail literal indices. Literals not encoded a priori using this method will be enoded on the fly as discovered during the clause-level processing of encode().

    lits

    the list of literals to encode

    returns

    the list of dual-rail literals resulting from the translation

  6. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  7. def bothLits(lit: Int): (Int, Int)

    Permalink

    Return both dual-rail encoded literals in (l_x, l_not_x).

  8. def cacheMap: Map[Int, Int]

    Permalink

    Returns the current translation cache as an immutable map.

  9. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  10. def encode(): Unit

    Permalink

    Encodes source formula to target formula using dual-rail encoding.

    Encodes source formula to target formula using dual-rail encoding.

    Literals not encoded a priori using the apply(List[Int]) will be encoded on the fly as discovered during clause traversal, and hence no guarantees can be given about the index range they will occupy nor on their ordering.

  11. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  12. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  13. def funcMap: Map[Int, (Int, Int)]

    Permalink

    Returns the current translation cache as an immutable map.

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

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

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

    Permalink
    Definition Classes
    AnyRef
  17. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
  19. def selFromSign(selector: Int, ifPos: Int, ifNeg: Int): Int

    Permalink

    Returns ifPos if selector > 0 and isNeg otherwise.

  20. val source: FormulaLike

    Permalink
  21. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  22. val target: FormulaLike

    Permalink
  23. def toPosNeg(lit: Int): (Int, Int)

    Permalink

    Given a literal, returns a pair (pos, neg) where: - pos is the positive version of the literal.

    Given a literal, returns a pair (pos, neg) where: - pos is the positive version of the literal. - neg the negative version of the literal.

  24. final def wait(): Unit

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

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

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

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped