Z3 plugin

The Z3 plugin provides the metamodel classes required to work with feature models that contain typed attributes (Integer, Real, String) and to analyse them using the Z3 SMT solver.

Table of contents

1. Z3 metamodel plugin of flamapy framework
   1. Features of the Z3 Metamodel Plugin
   2. Installation instructions
   3. Links
2. Operations
3. Transformations supported
   1. Model to model transformations

Official repository

https://www.github.com/flamapy/z3_metamodel

Z3 metamodel plugin of flamapy framework

The z3_metamodel plugin integrates the Z3 SMT solver into the flamapy framework. Unlike the SAT and BDD plugins which operate on Boolean feature models, Z3 supports typed attributes, enabling analysis of feature models with Integer, Real, and String constraints.

Features of the Z3 Metamodel Plugin

1. SMT Solver Integration
   • Leverages the Z3 SMT solver for constraint solving beyond Boolean logic.
   • Handles Integer, Real, and String typed attributes alongside Boolean features.
2. Metamodel Classes
   • Provides the Z3Model class to represent feature models with typed attributes.
   • Supports transformation from feature models to Z3 constraint systems.
3. Operations
   • Satisfiability checking for models with typed attributes.
   • Configuration enumeration and counting with attribute constraints.
   • Feature and attribute bound computation (min/max ranges per attribute).
   • Attribute optimization (minimise/maximise attribute values over valid configurations).
4. Transformations
   • Model-to-Model (M2M): Transforms feature models into Z3 constraint representations.

Installation instructions

To install the z3_metamodel plugin, follow these steps:

1. Install Python: Ensure that Python 3.9 or later is installed on your system.

2. Install the Z3 Metamodel Plugin:

   • Using pip, the Python package manager, you can install the z3_metamodel plugin directly from PyPI:

     pip install flamapy-z3
     

Links

• PyPI: z3_metamodel on PyPI
• GitHub Repository: z3_metamodel on GitHub

Operations

Currently, this plugin enables the following operations on feature models with typed attributes:

• All Feature Bounds
• Attribute Optimization
• Configurations
• Number of Configurations
• Core Features
• Dead Features
• False Optional Features
• Feature Bounds
• Satisfiable
• Satisfiable Configuration
• Variable Bounds

Transformations supported

Model to model transformations