uvllang

A toolkit for the Universal Variability Language (UVL). Supports conversion to CNF (DIMACS), SMT-LIB 2, and recovery of UVL models from DIMACS/SMT-LIB files.

uvl2cnf, uvl2smt, uvl2uvl, and any2uvl are native Zig binaries. The Python API (UVL(...)) defaults to the same Zig backend, and also supports seperate Lark and ANTLR4 backends (backend="lark"/"antlr"). The ANTLR4 grammar is derived from the official grammar

Installation

pip install uvllang

# With Lark parser support (backend="lark" in the Python API)
pip install uvllang[lark]

# With ANTLR parser support (backend="antlr" in the Python API)
pip install uvllang[antlr]

pip install uvllang ships prebuilt binaries; installing from a source checkout (pip install . or pip install -e .) compiles them via zig build automatically and puts uvl2cnf/uvl2uvl/uvl2smt/any2uvl on PATH -- the Zig toolchain just needs to be installed first. Running the binaries straight out of a checkout without installing anything needs a manual building and linking.

CLI tools

uvl2cnf: UVL to DIMACS CNF

A native binary (parser/zig-out/bin/uvl2cnf, built by zig build in parser/).

uvl2cnf model.uvl                      # writes model.dimacs
uvl2cnf model.uvl output.dimacs        # explicit output path
uvl2cnf model.uvl -v                   # also print feature/constraint/variable/clause counts
uvl2cnf --conversion model.uvl         # convert group cardinality + feature-local constraint attributes instead of dropping them
uvl2cnf --loud model.uvl               # fail instead of warning when a construct above the Boolean level would be dropped
uvl2cnf --simplify model.uvl           # run subsumption elimination + self-subsuming resolution over the output clause set
uvl2cnf --simplify --no-ssr model.uvl  # ...or subsumption elimination only

For Lark/ANTLR specifically (e.g. cross-checking against this backend), use the Python API instead: UVL(from_file="model.uvl", backend="lark").to_cnf().

Only the plain Boolean language level is supported for CNF conversion, identically across all three backends - see Non-Boolean constructs below for exactly what's affected and how --conversion/--loud change the behavior.

uvl2smt: UVL to SMT-LIB 2

A native binary (parser/zig-out/bin/uvl2smt), unlike uvl2cnf not restricted to the plain Boolean level: numeric comparisons, aggregate functions (sum/avg/len/floor/ceil, including the 2-argument scoped form sum(Feature, Attr)), and typed (String/Integer/Real) features are all represented. Feature-local constraint/constraints attributes are always included too (unconditionally, alongside the top-level constraints block).

uvl2smt model.uvl                 # writes model.smt2
uvl2smt model.uvl output.smt2
uvl2smt model.uvl -v              # also print feature/constraint counts and output size

Lark/ANTLR-backed SMT generation is available through UVL(backend="lark"/"antlr").to_smt().

uvl2uvl: UVL to UVL, redundant constraints removed

A native binary (parser/zig-out/bin/uvl2uvl) that writes a semantically equivalent UVL model back out, keeping the input's feature hierarchy exactly as-is while dropping any cross-tree constraint that's entirely subsumed by the hierarchy and the other constraints - every surviving constraint is emitted verbatim.

uvl2uvl model.uvl                 # writes model_reduced.uvl
uvl2uvl model.uvl output.uvl      # explicit output path
uvl2uvl model.uvl -v              # also print feature/constraint counts

any2uvl: DIMACS CNF or SMT-LIB 2 to UVL

A native binary (parser/zig-out/bin/any2uvl) that recovers a UVL feature model from either a DIMACS CNF file or an .smt2 file written by uvl2smt (input format is detected from content, only the SMT subset of UVL is supported). Hierarchy is reconstructed via a spanning-tree heuristic, remaining clauses (or any assert that isn't a pure Boolean formula over declared features in SMT) become cross-tree constraints. The output is always logically equivalent to the input regardless of hierarchy-recovery quality.

any2uvl model.dimacs              # writes model_recovered.uvl
any2uvl model.smt2 output.uvl     # SMT-LIB input works the same way
any2uvl --optimize model.dimacs   # run CTC-reduction optimiser after recovery
any2uvl --byname model.dimacs     # break hierarchy tie-breaks by feature name similarity
any2uvl -v model.dimacs           # also print input variable/clause counts and output constraint count

The --optimize pass groups features that share common implied parents and moves them into the hierarchy, reducing cross-tree constraints where valid.

--byname affects the initial spanning-tree construction: when two candidate parents are at equal depth, the one whose name is most similar to the child (by edit-distance ratio) wins. Combine with --optimize for best results.

For SMT-LIB input, a non-Boolean assert (an arithmetic constraint, an attribute-value binding) is preserved as a residual UVL constraint when it has a UVL constraint-syntax equivalent, the small slice that doesn't (ite, to_int, str.len - mainly uvl2smt's own aggregate-function expansions) is dropped with a warning rather than emitted as invalid UVL.

Python API

from uvllang import UVL

model = UVL(from_file = "model.uvl")

# CNF (uvl2cnf) - written straight to a DIMACS file
model.to_dimacs("output.dimacs")
cnf = model.to_cnf()  # or as a PySAT CNF object

# SMT-LIB 2 (uvl2smt) - returns text, or writes a file if given a path
smt = model.to_smt()
model.to_smt("output.smt2")

# DIMACS -> UVL recovery (any2uvl), as an alternate constructor: from a
# file path, or directly from a pysat.formula.CNF object
recovered = UVL(from_cnf=cnf)
recovered = UVL(from_cnf="model.dimacs", optimize=True, by_name=True)

Non-Boolean Constructs

CNF conversion (uvl2cnf, UVL.to_cnf()/to_dimacs()) typically only supports the plain Boolean language level, identically across all three backends. Everything above that level falls into one of three tiers:

• Tier 1
  • group cardinality ([i..j] groups)
  • feature-local {constraint ...}/{constraints [...]} attributes
  • feature cardinality (clone multiplicity) - not encoded; see Feature cardinality: why it's not converted
• Tier 2 - Not encodable constraints:
  • a constraint referencing a feature attribute (e.g. Feature.attr > 3)
  • a constraint containing a numeric comparison
• Tier 3 - Metadata:
  • typed (String/Integer/Real) features - the type itself is ignored for CNF purposes
  • value attributes on features - ignored for CNF purposes

uvl2cnf always warns about all three tiers and continues regardless of flags. UVL.to_cnf()/to_dimacs() raise NonBooleanConstructError by default for Tier 1 and Tier 2 (Tier 3 only ever warns), unless you pass drop_non_boolean=True to UVL(...). uvl2cnf --loud mirrors this exactly: it exits nonzero instead of only warning, under the same rules.

--conversion (CLI) / conversion=True (Python API, all three backends) applies the UVLParser paper's conversion strategies for group cardinality and feature-local constraint attributes instead of dropping them - encoding the cardinality bound as enumerated Boolean clauses, and extracting the feature-local constraints as ordinary top-level constraints. Feature cardinality still does, as it isn't converted. With conversion=True, those two categories no longer raise.

to_smt() has no such restriction and never raises - every construct above is representable in SMT-LIB 2.

Feature cardinality: Why it's not converted

The UVLParser paper's own prescribed strategy for feature cardinality "repeated subtrees for feature instances" requires cloning a whole subtree per instance and rewriting any cross-tree constraint that references a cloned feature to target a specific instance - the paper itself notes its interaction with cross-tree constraints "is not always clear". This is a substantially larger and riskier piece of work than the other two conversions, so it's documented here as explicitly omitted.

CNF Clause-Set Simplification

uvl2cnf --simplify / UVL.to_cnf(simplify=True) runs a global simplification pass over the generated clause set, to a fixpoint: subsumption elimination (a clause entirely implied by a shorter one already present is removed) and self-subsuming resolution / strengthening (a clause is rewritten to drop a literal made redundant by another clause). Both are exact logical-equivalence transformations and maintain the solution space. Pass --no-ssr / no_ssr=True alongside --simplify / simplify=True to keep subsumption elimination only.

Both transformations may remove or rewrite the plain 2-literal clause {-child, parent} a mandatory/optional relationship produces (e.g., if parent turns out to be forced true unconditionally by other clauses, that clause is subsumed by the unit clause {parent} and dropped - the implication still holds logically, just not as a literal clause anymore). any2uvl's hierarchy reconstruction finds parent/child edges by pattern-matching exactly that literal shape, so it silently loses the edge (turning it into an ordinary cross-tree constraint instead - the recovered model is still logically equivalent, just with a worse hierarchy).

UVL.to_cnf() defaults to the same unsimplified behavior as the CLI, so the Python API and uvl2cnf produce the same clause set for the same input unless the caller explicitly opts in on both sides.

Pyodide / WebAssembly

libuvlparser.so (the same C ABI the native Python API binds to via ctypes) can also be built for wasm32-emscripten and loaded inside Pyodide, whose ctypes.CDLL is patched to dlopen Emscripten side modules. uvllang/_zig.py needs no Pyodide-specific code for this - its path search and ctypes.CDLL(path) call are format-agnostic. The 4 CLI binaries aren't part of this build and neither are the other backends backend="lark"/"antlr" and their supporting Python packages. setup.py drops both post-build for a Pyodide wheel specifically, shrinking it to ~90KB compressed.

cd parser
zig build -Dpyodide=true \
  --sysroot "$(em-config CACHE)/sysroot" \
  -Demcc="$(dirname "$(command -v em-config)")/emcc" \
  -Doptimize=ReleaseSmall

Requires the emscripten toolchain from pyodide-build's xbuildenv (em-config/emcc on PATH; pyodide xbuildenv install-emscripten). Produces zig-out/lib/libuvlparser.so. setup.py's build step runs this automatically when PYODIDE=1 is set (the signal pyodide-build sets in its own build environment), in place of the native build.

The build is two steps (parser/build.zig's buildPyodideLib):

1. zig build-lib compiles the module graph to a wasm32-emscripten static archive linked against Emscripten libc, invoked as a plain subprocess (b.addLibrary can't drive a multi-module command line, and its Compile step treats wasm-ld's "-shared is unstable" warning as a fatal error).
2. emcc -sSIDE_MODULE=1 links that archive into the final .so.

Step 2 is what makes it a real Emscripten side module: malloc/free resolve to imports from the Pyodide main module, so allocation goes through the host's allocator. A self-contained wasm build instead carries its own allocator and grows the shared WebAssembly.Memory with a raw memory.grow, which detaches every typed-array view Emscripten and libffi hold and crashes the runtime on the first allocating call (the uvllang 0.4.0 bug).

Also needs one capi.zig workaround for a gap in Zig 0.16's wasm32-emscripten support (gated on builtin.target.cpu.arch.isWasm(), native build unaffected, see ziglang/zig#25856): Zig's default debug-I/O backend (std.Io.Threaded, the panic machinery linked into every build) depends on a getrandom binding std/posix.zig doesn't define for the .emscripten OS tag, so it's overridden with std.Io.failing. The wasm build also uses std.heap.c_allocator (native uses smp_allocator, which needs threads).

tests/test_pyodide_wasm.py builds the .so and loads it inside a real Pyodide runtime (tests/pyodide_e2e.mjs), through Pyodide's own dynamic linker and ctypes shim, then runs uvl_source_to_cnf on real models including one large enough to force heap growth. It also asserts the .so imports malloc/free (the 0.4.0 regression guard).

libuvlparser.so is bundled as real package_data (uvllang/_zig_libs/, populated by setup.py's build hook before packaging), so a wheel built this way is installable and functional on its own - see Releasing for the full pyodide build flow that produces a properly pyemscripten_*_wasm32-tagged wheel.

Dependencies

• python-sat - CNF handling
• lark - optional (uvllang[lark]), backend="lark" in the Python API
• antlr4-python3-runtime - optional (uvllang[antlr]), backend="antlr" in the Python API
• z3-solver - optional, for solving SMT output and testing uvl2smt

Testing

pip install -e .[dev]
pytest tests/

Releasing

scripts/release.sh builds everything twine upload needs - the sdist, the native wheel, and the Pyodide/wasm32 wheel - into dist/, validated with twine check. It doesn't upload anything; review dist/ and run twine upload dist/* yourself.

pip install build twine pyodide-build
pyodide xbuildenv install-emscripten            # pyodide-build's own correctly-pinned Emscripten --
                                                 # do NOT rely on a system/distro emscripten package,
                                                 # it will almost certainly be the wrong version
scripts/release.sh

The native wheel is tagged manylinux2014 directly by setup.py - the Zig artifacts are fully statically linked (no libc dependency), so no auditwheel repair step or manylinux build container is needed. The Pyodide step prepends the xbuildenv's emscripten dir to PATH (pyodide build otherwise checks whatever emcc PATH resolves to and aborts on a version mismatch). The script aborts before building anything if pyodide is missing rather than silently producing a partial dist/ - pass --skip-pyodide to opt out on purpose instead.

References

Overview Paper for UVL

@article{UVL2024,
  title   = {UVL: Feature modelling with the Universal Variability Language},
  author  = {David Benavides and Chico Sundermann and Kevin Feichtinger and José A. Galindo and Rick Rabiser and Thomas Thüm},
  journal = {Journal of Systems and Software},
  volume  = {225},
  pages   = {112326},
  year    = 2025,
  doi     = {https://doi.org/10.1016/j.jss.2024.112326},
}

Language Levels in UVL

@inproceedings{SVT+:SPLC23,
	title     = {{UVLParser: Extending UVL With Language Levels and Conversion Strategies}},
	author    = {Sundermann, Chico and Vill, Stefan and Th\"{u}m, Thomas and Feichtinger, Kevin and Agarwal, Prankur and Rabiser, Rick and Galindo, Jos\'{e} A. and Benavides, David},
	booktitle = {Proc.\ Int'l Systems and Software Product Line Conf.\ (SPLC)},
	pages     = {39--42},
	location  = "Tokyo, Japan",
	doi       = {10.1145/3579028.3609013},
	publisher = {ACM},
	address   = {New York, NY, USA},
	month     = aug,
	year      = 2023,
	keywords  = {variability language, feature model, variability model},
}

Links

• UVL Parser
• UVL Models
• UVL Website