//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2021, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::_part_attributes.asciidoc[]

:leveloffset: -2

[[multivalue-practical-usage]]
== 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:

[cols="1,2", options="header"]
|===
| 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.
