kodkod.engine.bool

Class BooleanValue

java.lang.Object

kodkod.engine.bool.BooleanValue

All Implemented Interfaces:

Comparable<BooleanValue>

Direct Known Subclasses:

BooleanAccumulator, BooleanConstant, BooleanFormula

public abstract class BooleanValue
extends Object
implements Comparable<BooleanValue>

Represents a boolean value, which may be a formula or a constant. Boolean formulas are produced by circuit factories. Each value is associated with an integer label; the labels are unique within a given factory. A boolean value with a negative label -|l| represents the negation of the value with the positive label |l|. Non-constant values are not shared among factories.

Author:

Emina Torlak

Specfields:

op: Operator

label: [-Integer.MAX_VALUE, Integer.MAX_VALUE]

Invariants:

no c: BooleanValue - this | some components.c & components.this && c.label = this.label

Method Summary

Modifier and Type	Method and Description
int	compareTo(BooleanValue other) Boolean components are ordered according to their labels.
abstract int	label() Returns the label for this value.
abstract Operator	op() Returns the operator representing the function computed by this gate.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

compareTo

public final int compareTo(BooleanValue other)

Boolean components are ordered according to their labels. Note that the ordering is well defined on components produced by the same factory. Specifically, this comparison function is consistent with equals for the components produced by the same factory, but may not be for the components produced by different factories.

Specified by:

compareTo in interface Comparable<BooleanValue>

Returns:

0 if the label of this and other are the same, a negative integer if the label of this is smaller than the label of other; and a positive integer otherwise.

label

public abstract int label()

Returns the label for this value.

Returns:

this.label

op

public abstract Operator op()

Returns the operator representing the function computed by this gate.

Returns:

this.op