Practical usage

After this short and possibly mind-blowing introduction on decision diagrams in particular in the multi-valued variation, below some practical information on using the common.multivaluetrees library.

Variables

As you typically work with variables in several use-kinds, like i and i+ in the explanation above, this has to be defined first. The core functionality provided for that is in common.multivaluetrees.VarInfoBuilder. The class is generic over the type of variables. As a convenience, the common.multivaluetrees.SimpleVarInfoBuilder class has been created using common.multivaluetrees.SimpleVarVariable variables (with a name, a lower bound, and a number of valid values).

After creating an instance providing the number of use-kinds that you have, add the variables as you like. The order of adding is also the order of the variable nodes in the tree from the root towards the bottom ONE or ZERO terminator nodes. The elementary function is addVariable(<variable>, <use-kind>) which adds a node level for variable <variable> and usage index <use-kind> (running from 0 to the number of use-kinds excluding the upper bound).

As you usually want to have all use-kinds for a variable, and often want them on consecutive node levels in the tree, addVariable(<variable>) adds all use-kinds in one call. For a list of variables, addVariablesGroupOnVariables(<list-variables>) does the same for each variable in the list. First N use-kinds for the first variable, then N use-kinds for the second variable, and so on. If you want the same use-kinds near each other instead, addVariablesGroupOnUseKind(<list-variables>) exists.

Each call adds one or more VarInfo instances to the builder. A VarInfo instance is the equivalent of e.g. i and i+ above. The VarInfoBuilder instance also stores the relation between variables and their VarInfo instances. With a variable you can ask it for all related VarInfo instances (or just one instance), with a VarInfo instance you can ask for the associated variable.

Trees and relations

The VarInfo instances from the builder are used to construct multi-value nodes, and eventually trees of such nodes. This is done in the common.multivaluetrees.Tree class, the work horse in multi-value diagram computations. Constructing it is a simple Tree t = new Tree(); which gives you an empty tree.

Constructed relations in t are represented by common.multivaluetrees.Node objects. These objects should be considered to be read-only. They can be stored anywhere in the application. Modifying a Node object is not possible, but you can create a new (updated) object and store that.

You can read the information inside a Node. The only somewhat useful operation that you can perform on Node n is n.dumpGraphLines("a-description-of-n"); which dumps a human-readable representation of the relation expressed in the node. You may however also want to check out t.dumpGraph(Node n) which should provide better output.

The Tree t object is where nodes are created and stored. It provides the following features:

Feature Description

Node Tree.ZERO

Constant expressing the false relation.

Node Tree.ONE

Constant expressing the true relation.

Node t.buildEqualityValue(VarInfo varInfo, int value)

Construct the elementary var == value relation, see also below.

Node t.conjunct(Node a, Node b)

Construct a conjunction (‘and’ operator) of relations a and b.

Node t.multiConjunct(Node…​ nodes)

Construct a conjunction (‘and’ operator) of one or more relations.

Node t.disjunct(Node a, Node b)

Construct a disjunction (‘or’ operator) of relations a and b.

Node t.multiDisjunct(Node…​ nodes)

Construct a disjunction (‘or’ operator) of one or more relations.

Node t.invert(Node n)

Construct an inverted relation (‘not’ operator) of relation n.

Node t.replace(Node n, VarInfo oldVar, VarInfo newVar)

Construct a new relation from relation n, where the equality over oldVar is replaced by the equality over newVar, see also below.

Node t.abstract(Node n, VarInfo[] abstractions)

Abstracts from the supplied variables. The variable is replaced by a disjunction of its children.

String t.dumpGraph(Node n)

Output a human readable description of relation n.

  • The fool-proof way to build a relation from the ground up is to use Node t.buildEqualityValue(VarInfo varInfo, int value), combined with Node t.conjunct(Node a, Node b) (‘and’ operator) and Node t.disjunct(Node a, Node b) (‘or’ operator) calls.

    There is also Node t.buildEqualityIndex(VarInfo varInfo, int index) and Node t.buildEqualityIndex(VarInfo varInfo, int index, Node sub). These calls are more efficient, but ignore the lower bound (internally, the variable range is shifted to make the lower bound equal to 0), and the latter function assumes you build the relation bottom up (VarInfo instances of last to first calls in the VarInfoBuilder).

  • The Node t.replace(Node n, VarInfo oldVar, VarInfo newVar) is simple and has few requirements, but it is not very efficient variable replacement. For mass-replacement, Node t.adjacentReplacements(Node n, VariableReplacement[] replacements) is better where the variable replacement instances are constructed with VariableReplacement(VarInfo oldVar, VarInfo newVar). The oldVar and newVar variables should be on adjacent levels in the tree, and replacements must be ordered top-down.

  • A somewhat exotic method is Node t.assign(Node n, VarInfo varInfo, int index). It selects the relation where the varInfo variable has the index value (with shifted lower bound), and eliminates that variable as well.