Trait

util.sat

FormulaLike

Related Doc: package sat

Permalink

trait FormulaLike extends CnfLike with CircuitLike with PseudoBooleanLike with OptimizeLike

Created by rdelmas on 21/06/16.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. FormulaLike
  2. OptimizeLike
  3. PseudoBooleanLike
  4. CircuitLike
  5. CnfLike
  6. AnyRef
  7. 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.

    Conjunction.

    Definition Classes
    CircuitLike
  2. 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 }}}

    Definition Classes
    PseudoBooleanLike
  3. 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 }}}

    Definition Classes
    PseudoBooleanLike
  4. final case class Clause(lits: List[Int]) extends Product with Serializable

    Permalink

    A clause.

    A clause.

    Definition Classes
    CnfLike
  5. sealed trait Criterion extends AnyRef

    Permalink

    Abstract trait for optimization criteria.

    Abstract trait for optimization criteria.

    Definition Classes
    OptimizeLike
  6. sealed trait Gate extends AnyRef

    Permalink

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

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

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

    Permalink

    Equivalence.

    Equivalence.

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

    Permalink

    Implication.

    Implication.

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

    Permalink

    If-then-else.

    If-then-else.

    Definition Classes
    CircuitLike
  10. case class Maximize(lits: List[Int], weights: List[Int], k: Int = 0) extends (OptimizeLike.this)#Criterion with Product with Serializable

    Permalink

    A linear criterion to be maximized.

    A linear criterion to be maximized.

    Definition Classes
    OptimizeLike
  11. case class Minimize(lits: List[Int], weights: List[Int], k: Int = 0) extends (OptimizeLike.this)#Criterion with Product with Serializable

    Permalink

    A linear criterion to be minimized.

    A linear criterion to be minimized.

    Definition Classes
    OptimizeLike
  12. final case class Not(lit: Int) extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Negation.

    Negation.

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

    Permalink

    Disjunction.

    Disjunction.

    Definition Classes
    CircuitLike
  14. sealed trait PseudoBoolCst extends AnyRef

    Permalink
    Definition Classes
    PseudoBooleanLike
  15. sealed trait RelOp extends AnyRef

    Permalink

    Abstract type for relational operators used in cardinality constraints.

    Abstract type for relational operators used in cardinality constraints.

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

    Permalink

    Equivalence.

    Equivalence.

    Definition Classes
    CircuitLike

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
    Definition Classes
    PseudoBooleanLike
  5. object AtMost extends (PseudoBooleanLike.this)#RelOp with Product with Serializable

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

    Permalink
    Definition Classes
    PseudoBooleanLike
  7. object Input extends (CircuitLike.this)#Gate with Product with Serializable

    Permalink

    Represents an input gate of the circuit.

    Represents an input gate of the circuit.

    Definition Classes
    CircuitLike
  8. 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.

    Definition Classes
    PseudoBooleanLike
  9. 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.

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

    Permalink

    Definition Classes
    PseudoBooleanLike
  11. final def addCard(c: 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.

    Definition Classes
    PseudoBooleanLike
  12. def addCardImplem(c: Card): Unit

    Permalink

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

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

    Definition Classes
    PseudoBooleanLike
  13. 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.

    Definition Classes
    CnfLike
  14. def addClauseImplem(lits: List[Int]): Unit

    Permalink

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

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

    Definition Classes
    CnfLike
  15. 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.

    Definition Classes
    CnfLike
  16. final def addCriterion(c: Criterion): Unit

    Permalink

    Adds an optimization criterion to the formula.

    Adds an optimization criterion to the formula.

    Definition Classes
    OptimizeLike
  17. 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.

    Definition Classes
    PseudoBooleanLike
  18. final def addHeaderComment(comment: String): Unit

    Permalink

    Add a header comment in the formula.

    Add a header comment in the formula.

    Definition Classes
    CnfLike
  19. final def addPbCst(c: ClassicPBCst)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink
    Definition Classes
    PseudoBooleanLike
  20. final def asInstanceOf[T0]: T0

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

    Permalink

    Asserts that a certain literal must be true.

    Asserts that a certain literal must be true.

    Definition Classes
    CircuitLike
  22. 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

    Definition Classes
    CircuitLike
  23. final def assertions: Iterator[(Int, Option[Int])]

    Permalink

    returns

    An itetator on the gate variables of the formula.

    Definition Classes
    CircuitLike
  24. final def cards: Iterator[(PseudoBoolCst, Option[Int])]

    Permalink

    returns

    an iterator on the cardinality constraints currently in the solver.

    Definition Classes
    PseudoBooleanLike
  25. final def clauses: Iterator[(Clause, Option[Int])]

    Permalink

    returns

    an iterator on the clauses currently in the solver.

    Definition Classes
    CnfLike
  26. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def criteria: Iterator[Criterion]

    Permalink

    returns

    An iterator on criteria of the formula.

    Definition Classes
    OptimizeLike
  28. final def declareInput(lit: Int)(switch: Option[Int] = None, switchable: Boolean = false): Option[Int]

    Permalink

    Declares a literal as an output of the circuit.

    Declares a literal as an output of the circuit.

    Definition Classes
    CircuitLike
  29. final def declareOutput(lit: Int): Unit

    Permalink

    Declares a literal as an output of the circuit.

    Declares a literal as an output of the circuit.

    Definition Classes
    CircuitLike
  30. 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.

    Definition Classes
    CircuitLike
  31. 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.

    Definition Classes
    CircuitLike
  32. 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.

    Definition Classes
    CircuitLike
  33. 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.

    Definition Classes
    CircuitLike
  34. 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.

    Definition Classes
    CircuitLike
  35. 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.

    Definition Classes
    CircuitLike
  36. 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.

    Definition Classes
    CircuitLike
  37. final def eq(arg0: AnyRef): Boolean

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

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

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

    Permalink

    Freeze the variable underlying the literal.

    Freeze the variable underlying the literal.

    Definition Classes
    CnfLike
  41. 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.

    Definition Classes
    CnfLike
  42. 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.

    Definition Classes
    CnfLike
  43. def freshVarImplem(superRes: Int): Int

    Permalink

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

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

    Definition Classes
    CnfLike
  44. def freshVarImplem(superRes: Int, howmany: Int): Int

    Permalink

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

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

    Definition Classes
    CnfLike
  45. final def gates: Map[Int, (Gate, Option[Int])]

    Permalink

    returns

    A gate Map indexed by literals.

    Definition Classes
    CircuitLike
  46. final def gatesIterator: Iterator[(Int, (Gate, Option[Int]))]

    Permalink

    returns

    An itetator on gate literal definitions.

    Definition Classes
    CircuitLike
  47. final def getClass(): Class[_]

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

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

    Permalink

    returns

    Iterator over all header comments, in insertion order.

    Definition Classes
    CnfLike
  50. final def inputs: Iterator[Int]

    Permalink

    returns

    An itetator on the gate variables of the formula.

    Definition Classes
    CircuitLike
  51. final def isFree(lit: Int): Boolean

    Permalink

    returns

    True iff the literal is not a gate.

    Definition Classes
    CircuitLike
  52. def isFrozen(lit: Int): Boolean

    Permalink

    True iff the variable is frozen.

    True iff the variable is frozen.

    Definition Classes
    CnfLike
  53. final def isGate(lit: Int): Boolean

    Permalink

    returns

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

    Definition Classes
    CircuitLike
  54. final def isInput(lit: Int): Boolean

    Permalink

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

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

    Definition Classes
    CircuitLike
  55. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  56. 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.

    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.

    Definition Classes
    CnfLike
  57. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  58. final def nofAssertions: Int

    Permalink

    returns

    the number of gates of the formula.

    Definition Classes
    CircuitLike
  59. final def nofClauses: Int

    Permalink

    returns

    the number of clauses of the formula.

    Definition Classes
    CnfLike
  60. final def nofCriteria: Int

    Permalink

    returns

    the number of criteria of the formula.

    Definition Classes
    OptimizeLike
  61. final def nofGates: Int

    Permalink

    returns

    The number of gates of the formula.

    Definition Classes
    CircuitLike
  62. final def nofInputs: Int

    Permalink

    returns

    the number of gates of the formula.

    Definition Classes
    CircuitLike
  63. final def nofOutputs: Int

    Permalink

    returns

    the number of gates of the formula.

    Definition Classes
    CircuitLike
  64. final def nofPBCst: Int

    Permalink

    returns

    the number of cardinality constraints of the formula.

    Definition Classes
    PseudoBooleanLike
  65. final def nofVars: Int

    Permalink

    returns

    the number of variables created using freshVar

    Definition Classes
    CnfLike
  66. final def notify(): Unit

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

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

    Permalink

    returns

    An iterator on the gate variables of the formula.

    Definition Classes
    CircuitLike
  69. final def synchronized[T0](arg0: ⇒ T0): T0

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

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

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

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

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

Inherited from OptimizeLike

Inherited from PseudoBooleanLike

Inherited from CircuitLike

Inherited from CnfLike

Inherited from AnyRef

Inherited from Any

Ungrouped