BooleanFactory (Kodkod API)

java.lang.Object
- kodkod.engine.bool.BooleanFactory

```
public abstract class BooleanFactory
extends Object
```
A factory for creating boolean values, matrices, and ints.

Author:

Emina Torlak

Specfields:

comparisonDepth: int // the depth to which circuits should be checked for equality

intEncoding: Options.IntEncoding // the encoding used for generating integers (integer(int)

bitwidth: int // the bitwidth used for integer computations

components: set BooleanValue

Invariants:

BooleanConstant in components

no f1, f2: BooleanFactory | f1 != f2 => f1.components & f2.components = BooleanConstant

let formulas = (components & BooleanFormula) - NotGate | min(formulas.label) = 1 && max(formulas.label) = #formulas

Method Summary

Methods
Modifier and Type	Method and Description
`BooleanValue`	`accumulate(BooleanAccumulator g)` Converts the given accumulator into an immutable boolean value and adds it to this.components.
`void`	`addVariables(int numVars)` Adds the specified number of fresh variables to `this.components`.
`BooleanValue`	`and(BooleanValue v0, BooleanValue v1)` Returns a boolean value whose meaning is the conjunction of the input components.
`int`	`bitwidth()` Returns the bitwidth used for integer representation.
`BooleanValue`	`carry(BooleanValue v0, BooleanValue v1, BooleanValue cin)` Returns a boolean value whose meaning is the carry out bit of a full binary adder.
`int`	`comparisonDepth()` Returns the depth (from the root) to which components are checked for semantic equality during gate construction.
`static BooleanFactory`	`constantFactory(Options options)` Returns a BooleanFactory with no variables; the returned factory can manipulate only constants.
`boolean`	`contains(BooleanValue v)` Returns true if v is in this.components.
`static BooleanFactory`	`factory(int numVars, Options options)` Returns a boolean factory, initialized to contain the given number of boolean variables.
`BooleanValue`	`iff(BooleanValue v0, BooleanValue v1)` Returns a boolean value whose meaning is [[v0]] <=> [[v1]].
`BooleanValue`	`implies(BooleanValue v0, BooleanValue v1)` Returns a boolean value whose meaning is [[v0]] => [[v1]].
`abstract Int`	`integer(int number)` Returns an Int that represents the given number using this.intEncoding.
`abstract Int`	`integer(int number, BooleanValue bit)` Returns an Int that represents 0 or the given number, depending on the value of the given bit.
`abstract Options.IntEncoding`	`intEncoding()` Returns the encoding used by this factory to represent integers.
`BooleanValue`	`ite(BooleanValue i, BooleanValue t, BooleanValue e)` Returns a boolean value whose meaning is [[i]] ? [[t]] : [[e]].
`BooleanMatrix`	`matrix(Dimensions d)` Returns a BooleanMatrix with the given dimensions and this as the factory for its non-FALSE components.
`BooleanMatrix`	`matrix(Dimensions d, IntSet allIndices, IntSet trueIndices)` Returns a BooleanMatrix `m` with the given dimensions, this as its factory, and the indices from the set `trueIndices` initialized to TRUE.
`int`	`maxFormula()` Returns the maximum label of a `formula` in `this.components`.
`int`	`maxVariable()` Returns the maximum label of a `variable` in `this.components`.
`BooleanValue`	`not(BooleanValue v)` Returns the negation of the given boolean value.
`int`	`numberOfVariables()` Returns the number of variables in this factory.
`BooleanValue`	`or(BooleanValue v0, BooleanValue v1)` Returns a boolean value whose meaning is the disjunction of the input components.
`void`	`setComparisonDepth(int newDepth)` Sets the comparison depth to the given value.
`BooleanValue`	`sum(BooleanValue v0, BooleanValue v1, BooleanValue cin)` Returns a boolean value whose meaning is the sum bit of a full binary adder.
`Int`	`sum(Collection<BooleanValue> bits)` Returns an Int that represents the sum of all values in the given collection.
`BooleanVariable`	`variable(int label)` Returns the variable with the given label.
`BooleanValue`	`xor(BooleanValue v0, BooleanValue v1)` Returns a boolean value whose meaning is [[v0]] ^ [[v1]].

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Method Detail
  - accumulate
```
public final BooleanValue accumulate(BooleanAccumulator g)
```
    Converts the given accumulator into an immutable boolean value and adds it to this.components. This method requires that all of g's inputs are in this.components. If g has no inputs, its operator's identity constant is returned. If g has one input, that input is returned. Otherwise, an immutable value that is semantically equivalent to g is returned. The behavior of this method is unspecified if the components of g are not components of this factory.
    
    Requires:
    
    g.components in this.components
    
    Ensures:
    
    this.components' = this.components + g'
    
    Returns:
    no g.inputs => g.op.identity(), one g.inputs => g.inputs, {g' : BooleanValue - BooleanAccumulator | [[g']] = [[g]] }
  - addVariables
```
public final void addVariables(int numVars)
```
    Adds the specified number of fresh variables to this.components.
    
    Requires:
    
    numVars >= 0
    
    Ensures:
    
    let diff = this.components' - this.components | diff in BooleanVariable && #diff = numVars && diff.label = { i: int | this.maxFormula() < i <= this.maxFormula() + numVars }
  - and
```
public final BooleanValue and(BooleanValue v0,
               BooleanValue v1)
```
    Returns a boolean value whose meaning is the conjunction of the input components. The behavior of this method is unspecified if v0 or v1 are not components of this factory.
    
    Requires:
    
    v0 + v1 in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    {v: BooleanValue | [[v]] = [[v0]] AND [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - bitwidth
```
public final int bitwidth()
```
    Returns the bitwidth used for integer representation.
    
    Returns:
    this.bitwidth
  - carry
```
public final BooleanValue carry(BooleanValue v0,
                 BooleanValue v1,
                 BooleanValue cin)
```
    Returns a boolean value whose meaning is the carry out bit of a full binary adder. The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
    
    Requires:
    
    v0 + v1 + cin in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = ([[v0]] and [[v1]]) or ([[cin]] and ([[v0]] xor [[v1]])) }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - comparisonDepth
```
public final int comparisonDepth()
```
    Returns the depth (from the root) to which components are checked for semantic equality during gate construction.
    
    Returns:
    this.comparisonDepth
  - constantFactory
```
public static BooleanFactory constantFactory(Options options)
```
    Returns a BooleanFactory with no variables; the returned factory can manipulate only constants.
    
    Returns:
    {f: BooleanFactory | f.components = BooleanConstant && f.comparisonDepth = options.sharing && f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding }
    
    Throws:
    
    NullPointerException - options = null
  - contains
```
public final boolean contains(BooleanValue v)
```
    Returns true if v is in this.components.
    
    Returns:
    v in this.components
    
    Throws:
    
    NullPointerException - v = null
  - factory
```
public static BooleanFactory factory(int numVars,
                     Options options)
```
    Returns a boolean factory, initialized to contain the given number of boolean variables.
    Gates are checked for semantic equality down to the depth given by options.sharing when checking for cached values. In general, setting the comparison depth to a higher value will result in more subcomponents being shared. However, it will also slow down gate construction.
    
    Integers are created/manipulated according to the specifications in the given Options object.
    
    Returns:
    {f: BooleanFactory | #(f.components & BooleanVariable) = numVars && BooleanConstant in f.components && f.components in BooleanVariable + BooleanConstant && f.comparisonDepth = options.sharing && f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding && (all i: [1..numVars] | one f.components.label & i }}
    
    Throws:
    
    IllegalArgumentException - numVars < 0 || numVars = Integer.MAX_VALUE
    
    NullPointerException - options = null
  - iff
```
public final BooleanValue iff(BooleanValue v0,
               BooleanValue v1)
```
    Returns a boolean value whose meaning is [[v0]] <=> [[v1]]. The behavior of this method is unspecified if v0 or v1 are not components of this factory.
    
    Requires:
    
    v0 + v1 in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = [[v0]] iff [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - implies
```
public final BooleanValue implies(BooleanValue v0,
                   BooleanValue v1)
```
    Returns a boolean value whose meaning is [[v0]] => [[v1]]. The behavior of this method is unspecified if v0 or v1 are not components of this factory.
    
    Requires:
    
    v0 + v1 in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = [[v0]] => [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - integer
```
public abstract Int integer(int number)
```
    Returns an Int that represents the given number using this.intEncoding.
    
    Returns:
    { i: Int | [[i]] = number && i.encoding && this.intEncoding && i.factory = this}
    
    Throws:
    
    IllegalArgumentException - the number cannot be represented using the specified encoding
  - integer
```
public abstract Int integer(int number,
          BooleanValue bit)
```
    Returns an Int that represents 0 or the given number, depending on the value of the given bit. The behavior of this method is unspecified if the bit is not a component of this factory.
    
    Returns:
    { i: Int | [[bit]] => [[i]] = number, [[i]] = 0 && i.encoding = this.intEncoding && i.factory = this}
  - intEncoding
```
public abstract Options.IntEncoding intEncoding()
```
    Returns the encoding used by this factory to represent integers.
    
    Returns:
    this.intEncoding
  - ite
```
public final BooleanValue ite(BooleanValue i,
               BooleanValue t,
               BooleanValue e)
```
    Returns a boolean value whose meaning is [[i]] ? [[t]] : [[e]]. The behavior of this method is unspecified if i, t, or e are not components of this factory.
    
    Requires:
    
    i + t + e in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = [[i]] ? [[t]] : [[e]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - matrix
```
public final BooleanMatrix matrix(Dimensions d)
```
    Returns a BooleanMatrix with the given dimensions and this as the factory for its non-FALSE components. The returned matrix can store any value from this.components at all indices between 0, inclusive, and d.capacity(), exclusive.
    
    Returns:
    { m: BooleanMatrix | m.factory = this && m.dimensions = d && m.elements = [0..d.capacity) -> one FALSE }
    
    Throws:
    
    NullPointerException - d = null
  - matrix
```
public final BooleanMatrix matrix(Dimensions d,
                   IntSet allIndices,
                   IntSet trueIndices)
```
    Returns a BooleanMatrix m with the given dimensions, this as its factory, and the indices from the set trueIndices initialized to TRUE. An IndexOutOfBoundsException may be thrown if BooleanMatrix.set(int, BooleanValue) is called on m with an index not contained in allIndices. If allIndices.equals(trueIndices), m may be a constant matrix; that is, an IllegalArgumentException may be thrown if BooleanMatrix.set(int, BooleanValue) is called on m with a non-constant value. Finally, if cloning trueIndices results in an immutable set, then m.set(int, BooleanValue) may throw an UnsupportedOperationException when called with a member of trueIndices.
    
    Requires:
    
    allIndices.containsAll(trueIndices)
    
    Returns:
    { m: BooleanMatrix | m.factory = this && m.dimensions = dims && m.elements = [0..d.capacity()-1] ->one FALSE ++ indices->TRUE }
    
    Throws:
    
    IllegalArgumentException - allIndices !in [0..d.capacity())
    
    IllegalArgumentException - one of the input sets is not cloneable
    
    NullPointerException - d = null || allIndices = null || trueIndices = null
  - maxFormula
```
public final int maxFormula()
```
    Returns the maximum label of a formula in this.components. Note that maxFormula() >= maxVariable() since variables themselves are formulas.
    
    Returns:
    max((this.components & BooleanFormula).label)
  - maxVariable
```
public final int maxVariable()
```
    Returns the maximum label of a variable in this.components.
    
    Returns:
    max((this.components & BooleanVariable).label)
  - not
```
public final BooleanValue not(BooleanValue v)
```
    Returns the negation of the given boolean value.
    
    Ensures:
    
    (components.v).components' = (components.v).components + n
    
    Returns:
    {n: BooleanValue | n.label = -v.label && [[n]] = ![[v]] }
    
    Throws:
    
    NullPointerException - v = null
  - numberOfVariables
```
public final int numberOfVariables()
```
    Returns the number of variables in this factory.
    
    Returns:
    #(this.components & BooleanVariable)
  - or
```
public final BooleanValue or(BooleanValue v0,
              BooleanValue v1)
```
    Returns a boolean value whose meaning is the disjunction of the input components. The behavior of this method is unspecified if v0 or v1 are not components of this factory.
    
    Requires:
    
    v0 + v1 in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    {v: BooleanValue | [[v]] = [[v0]] OR [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
    
    IllegalArgumentException - v0 + v1 !in this.components
  - setComparisonDepth
```
public final void setComparisonDepth(int newDepth)
```
    Sets the comparison depth to the given value. Setting the comparison depth to a high value will result in more subcomponents being shared. However, it will also slow down gate construction.
    
    Ensures:
    
    this.comparisonDepth' = newDepth
    
    Throws:
    
    IllegalArgumentException - newDepth < 1
  - sum
```
public final BooleanValue sum(BooleanValue v0,
               BooleanValue v1,
               BooleanValue cin)
```
    Returns a boolean value whose meaning is the sum bit of a full binary adder. The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
    
    Requires:
    
    v0 + v1 + cin in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = [[cin]] xor [[v0]] xor [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null
  - sum
```
public final Int sum(Collection<BooleanValue> bits)
```
    Returns an Int that represents the sum of all values in the given collection.
    
    Returns:
    an Int that represents the sum of all values in the given collection.
  - variable
```
public final BooleanVariable variable(int label)
```
    Returns the variable with the given label.
    
    Requires:
    
    0 < label <= numberOfVariables()
    
    Returns:
    (this.components & BooleanVariable).label
  - xor
```
public final BooleanValue xor(BooleanValue v0,
               BooleanValue v1)
```
    Returns a boolean value whose meaning is [[v0]] ^ [[v1]]. The behavior of this method is unspecified if v0 or v1 are not components of this factory.
    
    Requires:
    
    v0 + v1 in this.components
    
    Ensures:
    
    this.components' = this.components + v
    
    Returns:
    { v: BooleanValue | [[v]] = [[v0]] xor [[v1]] }
    
    Throws:
    
    NullPointerException - any of the arguments are null

Class BooleanFactory

Method Summary

Methods inherited from class java.lang.Object

Method Detail

accumulate

addVariables

and

bitwidth

carry

comparisonDepth

constantFactory

contains

factory

iff

implies

integer

integer

intEncoding

ite

matrix

matrix

maxFormula

maxVariable

not

numberOfVariables

or

setComparisonDepth

sum

sum

variable

xor