UVL-SMT: A JavaSMT-Based Reasoning Library for UVL

Dependencies

This project depends on JavaSMT for reasoning and java-fm-metamodel for the internal feature model representation. The required dependencies are part of the pom.xml and can be installed via maven. To use Z3, we need the binaries in src/main/resources/bin. They can be included by setting -Djava.library.path=./src/main/resources/bin

The compilation can be performed using maven, e.g., mvn clean compile

Usage

Example for checking satisfiability of a UVL feature model:

FMToSmtConverter smtConverter;
try {
    smtConverter = new FmToSMTConverter(uvlFeatureModel);
} catch (InvalidConfigurationException e) {
    throw new RuntimeException(e);
}
smtChecker = new SMTSatisfiabilityChecker(smtConverter.convertFeatureModel(), smtConverter.getContext());
smtChecker.isSat();

Known issues

• The underlying SMT library (JavaSMT with z3) does not treat constraint with division by zero as UNSAT, which may cause unintended effects