Trait

util.sat

CircuitLike

Related Doc: package sat

Permalink

trait CircuitLike extends AnyRef

An interface for building circuit-like formulas on top of CNF formulas.

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

Type Members

  1. final case class And(lits: List[Int]) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Conjunction.

  2. sealed trait Gate extends AnyRef

    Permalink

    Abstract type for logical gates used when constructing a CNF formula.

  3. final case class Iff(kid1: Int, kid2: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Equivalence.

  4. final case class Implies(kid1: Int, kid2: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Implication.

  5. final case class Ite(kid1: Int, kid2: Int, kid3: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    If-then-else.

  6. final case class Not(lit: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Negation.

  7. final case class Or(lits: List[Int]) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Disjunction.

  8. final case class Xor(kid1: Int, kid2: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Equivalence.

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 Input extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Represents an input gate of the circuit.

  5. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  6. final def assert(lit: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Asserts that a certain literal must be true.

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

    Permalink

    Asserts that a collection of literals are all equal, implemented using a loop of implications.

    Asserts that a collection of literals are all equal, implemented using a loop of implications.

    l1 = l2 = ... = ln := l1 -> l2 & ... & ln -> l1
    lits

    list of literals of size >= 2

    switch

    optional switch literal

    switchable

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

    returns

    The optional switching literal

  8. final def assertions: Iterator[(Int, Option[Int])]

    Permalink

    returns

    An itetator on the gate variables of the formula.

  9. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  10. final def declareInput(lit: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Declares a literal as an output of the circuit.

  11. final def declareOutput(lit: Int): Unit

    Permalink

    Declares a literal as an output of the circuit.

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

    Permalink

    Encodes the equation

    Encodes the equation

    x = And(a1, ... ,an)

    as clauses:

    (  x, ~a1, ... , ~an)
    ( ~x,  a1 )
    ...
    ( ~x,  an )
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  13. final def defineIff(x: Int, p: Int, q: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Iff(p, q)

    as clauses:

    ( ~x, ~p,  q )
    ( ~x,  p, ~q )
    (  x, ~p, ~q )
    (  x,  p,  q )
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  14. final def defineImplies(x: Int, p: Int, q: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Implies(p, q)

    as clauses:

    (~x, ~p, q )
    ( x,  p )
    ( x, ~q )
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  15. final def defineIte(x: Int, s: Int, t: Int, f: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Ite(s, t, f)

    as clauses:

    (  x, ~s, ~t )
    ( ~x, ~s,  t )
    (  x,  s, ~f )
    ( ~x,  s,  f )
    (  x, ~t, ~f )
    ( ~x,  f,  t )
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  16. final def defineNot(x: Int, p: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Not(p)

    as clauses:

    (~x, ~p)
    (x, p)
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  17. final def defineOr(x: Int, lits: List[Int])(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Or(a1, ... , an)

    as clauses:

    ( ~x,  a1, ... , an)
    (  x, ~a1)
    ...
    (  x, ~an)
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

  18. final def defineXor(x: Int, p: Int, q: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Encodes the equation

    Encodes the equation

    x = Xor(p, q)

    as clauses:

    ( ~x,  p,  q )
    ( ~x, ~p, ~q )
    (  x,  p, ~q )
    (  x, ~p,  q )
    switch

    optional switch literal

    switchable

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

    returns

    if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.

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

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

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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  22. final def gates: Map[Int, ((CircuitLike.this)#Gate, Option[Int])]

    Permalink

    returns

    A gate Map indexed by literals.

  23. final def gatesIterator: Iterator[(Int, ((CircuitLike.this)#Gate, Option[Int]))]

    Permalink

    returns

    An itetator on gate literal definitions.

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  26. final def inputs: Iterator[Int]

    Permalink

    returns

    An itetator on the gate variables of the formula.

  27. final def isFree(lit: Int): Boolean

    Permalink

    returns

    True iff the literal is not a gate.

  28. final def isGate(lit: Int): Boolean

    Permalink

    returns

    True iff the literal or its complement is defined as a gate.

  29. final def isInput(lit: Int): Boolean

    Permalink

    True iff the literal was previously declared as a circuit input.

  30. final def isInstanceOf[T0]: Boolean

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

    Permalink
    Definition Classes
    AnyRef
  32. final def nofAssertions: Int

    Permalink

    returns

    the number of gates of the formula.

  33. final def nofGates: Int

    Permalink

    returns

    The number of gates of the formula.

  34. final def nofInputs: Int

    Permalink

    returns

    the number of gates of the formula.

  35. final def nofOutputs: Int

    Permalink

    returns

    the number of gates of the formula.

  36. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
  38. final def outputs: Iterator[Int]

    Permalink

    returns

    An iterator on the gate variables of the formula.

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

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

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

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped