Manipulation APIs

Manipulation APIs

This page documents the field-aware operations in the low-level org.ants.jndd.diagram.NDD API. NDD node IDs are integers; initialize the engine, declare every field, and call generateFields() before using any operation.

NDD.initNDD(100_000, 10_000, 100_000, 10_000);
int src = NDD.declareField(32);
int dst = NDD.declareField(32);
NDD.generateFields();

Unless noted otherwise, every operation returns an NDD node ID that is not permanently protected. Call NDD.ref(result) if the result must survive later allocations or garbage collection, and balance it with NDD.deref(result) when it is no longer needed.

Overview

Need	API	Field-aware behavior
Canonical construction	mk(field, edges), addAtField(field, edges)	Builds or reuses a node whose outgoing edges are labeled by field predicates.
Boolean operations	and, or, not, diff, imp	Combines complete NDDs.
Generic Boolean operation	apply(operation, left, right)	Supports AND, OR, XOR, NAND, NOR, BIIMP, IMP, and DIFF.
Care-set simplification	simplify(function, careSet)	Preserves function on the care set and returns FALSE outside it.
Cofactor	restrict(root, field, value)	Fixes one field and removes it from the returned NDD.
Counting and witnesses	satCount, anySat, allSat	Counts or enumerates complete assignments over declared fields.
Quantification	exist(root, fields...)	Projects out one or more complete fields.
Replacement	substitute(root, sourceField, targetField)	Replaces the source field with the target field.

Construction and Boolean Operations

mk is the NDD equivalent of an ROBDD unique-table constructor. Instead of a single variable and two successors, it receives a field and a target-to-label map. Equal nodes are canonicalized by the node table.

Map<Integer, Integer> edges = new HashMap<>();
edges.put(NDD.getTrue(), someFieldLabel);
int node = NDD.addAtField(src, edges);

Most callers should use the supplied encoders or literal nodes instead:

int sourceHighBit = NDD.getVar(src, 0);
int destinationHighBit = NDD.getVar(dst, 0);
int allowed = NDD.and(sourceHighBit, destinationHighBit);

int different = NDD.apply(NDD.BinaryOperation.XOR, sourceHighBit, destinationHighBit);
int implication = NDD.apply(NDD.BinaryOperation.IMP, sourceHighBit, destinationHighBit);

simplify(function, careSet) is deliberately conservative: it returns function AND careSet. It therefore agrees with function on every cared-for assignment and is FALSE elsewhere. NDD's canonical representation already removes structurally redundant nodes; this API does not claim to compute a minimum-size don't-care cover.

Restriction (Cofactor)

restrict fixes a field to one value and existentially removes that field from the result. This is the field-level counterpart of BDD restrict/cofactor.

For Boolean and complemented-BDD labels, use either an unsigned long for fields up to 63 bits or an MSB-first bit vector of exactly the field width:

// Assume tcp was declared before generateFields().

int onlyPort443 = NDD.restrict(policy, tcp, 443L);
int sameResult = NDD.restrict(policy, tcp,
    new int[]{0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1, 1, 1, 0, 1, 1});

Bit index 0 is the most significant bit, matching getVar(field, index) and encodePrefix.

For FINITE_DOMAIN_ZDD, restrict(root, field, value) accepts a domain-value index rather than a binary integer. The bit-vector overload is intentionally unavailable in that mode.

Satisfying Assignments

double numberOfPackets = NDD.satCount(policy);

int[][] witness = NDD.anySat(policy);
if (witness != null) {
    // BOOLEAN_BDD / COMPLEMENTED_BDD: witness[field][bit] is 0 or 1.
}

long visited = NDD.allSat(policy, assignment -> {
    inspect(assignment);
    return true;  // return false to stop early
});

anySat returns null for FALSE. In Boolean and complemented-BDD modes, each assignment[field] contains the complete MSB-first bit vector for that field. In finite-domain ZDD mode it contains one selected domain-value index.

allSat enumerates concrete, complete assignments and passes a defensive copy to the callback. It can be exponential in the number of free field values; use anySat for one witness or stop early by returning false from the callback. Its return value is the number of assignments delivered to the callback.

Existential Quantification

Quantification is at field granularity. The one-field and multi-field overloads use the same semantics:

int withoutSource = NDD.exist(reachability, src);
int headerIndependent = NDD.exist(reachability, src, dst);

The result no longer constrains the projected field(s). satCount still counts assignments in the original declared field universe, so a projected field contributes all of its possible values to the count.

Universal quantification can be expressed using the usual dual: not(exist(not(root), field)).

Field Substitution and Replacement

substitute(root, sourceField, targetField) returns the function formed by replacing every occurrence of sourceField with targetField. The two fields must have identical widths (or identical finite-domain sizes).

// Turns a predicate over src into the corresponding predicate over dst.
int destinationPredicate = NDD.substitute(sourcePredicate, src, dst);

// Equivalent alias when the intent is a rename.
int renamed = NDD.replaceField(sourcePredicate, src, dst);

The implementation constructs equality between the fields, conjoins it with the input, and existentially quantifies the source field. This preserves correct semantics even when the target field already occurs in root.

Backend Notes

apply, simplify, exist, anySat, allSat, and substitute work with every supported label mode. restrict accepts binary bit vectors only for BOOLEAN_BDD and COMPLEMENTED_BDD; in FINITE_DOMAIN_ZDD it uses a domain-value index.

For basic setup and encoding helpers, return to Usage. For sizing and field-layout guidance, see Parameters.