feat: updating all documentaiton with all new features and the z3 solver

Author: jagalindo

_flamapy_plugins/diagnosis.md

@@ -0,0 +1,87 @@
+---
+layout: default
+title: Diagnosis plugin
+parent: Plugins
+grand_parent: Flamapy as framework
+permalink: /framework/plugins/diagnosis_plugin
+nav_order: 7
+---
+
+# Diagnosis plugin
+{: .no_toc }
+
+The diagnosis plugin extends the PySAT metamodel with conflict detection and diagnosis capabilities, explaining why a configuration is inconsistent with a feature model.
+{: .fs-6 .fw-300 }
+
+## Table of contents
+{: .no_toc .text-delta }
+
+1. TOC
+{:toc}
+
+{: .highlight }
+> Official repository
+>
+> ```
+> https://www.github.com/flamapy/pysat_metamodel
+> ```
+
+## pysat_diagnosis metamodel plugin of flamapy framework
+
+The `pysat_diagnosis_metamodel` plugin builds on top of the PySAT metamodel to support automated debugging of feature models and configurations. Given a configuration and a test case, it computes **conflict sets** (minimal subsets of constraints that are inconsistent) and **diagnoses** (minimal sets of constraints whose removal restores consistency). It is shipped together with the `flamapy-sat` package.
+
+### Features of the Diagnosis Metamodel Plugin
+
+1. **Conflict and Diagnosis Algorithms**
+   - Implements QuickXPlain for computing minimal conflict sets.
+   - Implements FastDiag for computing minimal diagnoses.
+   - Uses an HSDAG (Hitting Set Directed Acyclic Graph) to enumerate multiple conflicts/diagnoses.
+
+2. **Metamodel Classes**
+   - Provides the `DiagnosisModel` (extension `pysat_diagnosis`) to represent the knowledge base, the constraints set, and the diagnosis task.
+
+3. **Operations**
+   - Conflict detection and diagnosis given a configuration and a test case.
+
+4. **Transformations**
+   - **Model-to-Model (M2M)**: Transforms feature models (`fm`) into the diagnosis model (`pysat_diagnosis`).
+
+### Installation instructions
+
+The diagnosis metamodel is distributed together with the PySAT plugin:
+
+1. **Install Python**: Ensure that Python 3.9 or later is installed on your system.
+
+2. **Install the PySAT Metamodel Plugin** (which includes the diagnosis metamodel):
+   ```bash
+   pip install flamapy-sat
+   ```
+
+### Links
+
+- **PyPI**: [pysat_metamodel on PyPI](https://pypi.org/project/flamapy-sat/)
+- **GitHub Repository**: [pysat_metamodel on GitHub](https://github.com/flamapy/pysat_metamodel)
+
+
+## Operations
+
+Currently, this plugin enables the following operations:
+
+<ul>
+  {% assign fm_operations = site.operations | where: "flamapy_diagnosis", true %}
+  {% for operation in fm_operations %}
+    <li><a href="{{ operation.url }}">{{ operation.title }}</a></li>
+  {% endfor %}
+</ul>
+
+
+## Transformations supported
+
+### Model to model transformations
+<ul>
+  {% assign transformations = site.transformations | where: "metamodel", "flamapy_diagnosis" %}
+  {% assign m2m_transformations = transformations | where: "type", "model_to_model" %}
+  {% for transformation in m2m_transformations %}
+    <li><a href="{{ transformation.url }}">{{ transformation.title }}</a></li>
+  {% endfor %}
+</ul>

_flamapy_plugins/z3.md

@@ -0,0 +1,91 @@
+---
+layout: default
+title: Z3 plugin
+parent: Plugins
+grand_parent: Flamapy as framework
+permalink: /framework/plugins/z3_plugin
+nav_order: 6
+---
+
+# Z3 plugin
+{: .no_toc }
+
+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.
+{: .fs-6 .fw-300 }
+
+## Table of contents
+{: .no_toc .text-delta }
+
+1. TOC
+{:toc}
+
+{: .highlight }
+> Official repository
+>
+> ```
+> https://www.github.com/flamapy/z3_metamodel
+> ```
+
+## Z3 metamodel plugin of flamapy framework
+
+The `z3_metamodel` plugin integrates the [Z3 SMT solver](https://github.com/Z3Prover/z3) into the {% include flamapy.html %} 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:
+     ```bash
+     pip install flamapy-z3
+     ```
+
+### Links
+
+- **PyPI**: [z3_metamodel on PyPI](https://pypi.org/project/flamapy-z3/)
+- **GitHub Repository**: [z3_metamodel on GitHub](https://github.com/flamapy/z3_metamodel)
+
+
+## Operations
+
+Currently, this plugin enables the following operations on feature models with typed attributes:
+
+<ul>
+  {% assign fm_operations = site.operations | where: "flamapy_z3", true %}
+  {% for operation in fm_operations %}
+    <li><a href="{{ operation.url }}">{{ operation.title }}</a></li>
+  {% endfor %}
+</ul>
+
+
+## Transformations supported
+
+### Model to model transformations
+<ul>
+  {% assign transformations = site.transformations | where: "metamodel", "flamapy_z3" %}
+  {% assign m2m_transformations = transformations | where: "type", "model_to_model" %}
+  {% for transformation in m2m_transformations %}
+    <li><a href="{{ transformation.url }}">{{ transformation.title }}</a></li>
+  {% endfor %}
+</ul>

_operations/all_feature_bounds.md

@@ -0,0 +1,59 @@
+---
+title: All Feature Bounds
+layout: default
+parent: Operations
+grand_parent: Flamapy as framework
+permalink: /framework/operations/all_feature_bounds
+nav_order: 25
+
+flamapy_sat: false
+flamapy_bdd: false
+flamapy_fm: false
+flamapy_z3: true
+flamapy_diagnosis: false
+cmd: false
+facade: true
+python: true
+rest: false
+---
+
+# All Feature Bounds
+
+**Description**:
+Returns the value bounds for all typed attribute features (Integer, Real, String) in the model. Each entry maps a feature name to a dictionary with `min`, `max`, and `bounded` keys. Requires the Z3 metamodel plugin (`flamapy-z3`).
+
+**Application**:
+Useful for understanding the numerical or string ranges that typed feature attributes can take across all valid configurations, aiding in constraint analysis and model validation.
+
+**Example**:
+Obtaining the minimum and maximum price bounds of all typed attributes in a configurable product model.
+
+---
+## Code Examples
+
+### Python easy to use facade usage
+```python
+from flamapy.interfaces.python.flamapy_feature_model import FLAMAFeatureModel
+# Load the feature model (must contain typed attributes)
+fm = FLAMAFeatureModel("path/to/feature/model")
+result = fm.all_feature_bounds()
+print(result)
+```
+
+### Python flamapy framework **ADVANCED** usage
+```python
+from flamapy.core.discover import DiscoverMetamodels
+# Initialize the discover metamodel
+dm = DiscoverMetamodels()
+# Get the fm metamodel representation
+feature_model = dm.use_transformation_t2m("path/to/feature/model", 'fm')
+# Manually call a M2M transformation to Z3
+z3_model = dm.use_transformation_m2m(feature_model, "z3")
+# Get the operation
+operation = dm.get_operation(z3_model, 'Z3AllFeatureBounds')
+# Execute the operation
+operation.execute(z3_model)
+# Get and print the result
+result = operation.get_result()
+print(result)
+```

_operations/atomic_sets.md

@@ -9,6 +9,8 @@ nav_order: 1
 flamapy_sat: false
 flamapy_bdd: false
 flamapy_fm: true
+flamapy_z3: false
+flamapy_diagnosis: false
 cmd: true
 facade: true
 python: true

_operations/attribute_optimization.md

@@ -0,0 +1,53 @@
+---
+title: Attribute Optimization
+layout: default
+parent: Operations
+grand_parent: Flamapy as framework
+permalink: /framework/operations/attribute_optimization
+nav_order: 27
+
+flamapy_sat: false
+flamapy_bdd: false
+flamapy_fm: false
+flamapy_z3: true
+flamapy_diagnosis: false
+cmd: false
+facade: false
+python: true
+rest: false
+---
+
+# Attribute Optimization
+
+**Description**:
+Returns the configurations that optimize one or more numerical attributes (Integer or Real). The optimization is based on the sum of the attribute values across all selected features. When a single attribute is given it returns all optimal configurations; when several attributes are given it returns the Pareto front of non-dominated configurations. Requires the Z3 metamodel plugin (`flamapy-z3`).
+
+**Application**:
+Useful for decision support in product lines with quantitative attributes — for example finding the cheapest, fastest, or most balanced valid configurations.
+
+**Example**:
+Finding the configurations of a car model that minimise total price while maximising total performance.
+
+---
+## Code Examples
+
+### Python flamapy framework usage
+```python
+from flamapy.core.discover import DiscoverMetamodels
+from flamapy.metamodels.z3_metamodel.operations.interfaces import OptimizationGoal
+# Initialize the discover metamodel
+dm = DiscoverMetamodels()
+# Get the fm metamodel representation
+feature_model = dm.use_transformation_t2m("path/to/feature/model", 'fm')
+# Manually call a M2M transformation to Z3
+z3_model = dm.use_transformation_m2m(feature_model, "z3")
+# Get the operation
+operation = dm.get_operation(z3_model, 'Z3AttributeOptimization')
+# Provide the attributes to optimize and the goal for each one
+operation.set_attributes({"price": OptimizationGoal.MINIMIZE})
+# Execute the operation
+operation.execute(z3_model)
+# Get and print the result
+result = operation.get_result()
+print(result)
+```

_operations/average_branching_factor.md

@@ -9,6 +9,8 @@ nav_order: 1
 flamapy_sat: false
 flamapy_bdd: false
 flamapy_fm: true
+flamapy_z3: false
+flamapy_diagnosis: false
 cmd: true
 facade: true
 python: true

_operations/backbone.md

@@ -0,0 +1,69 @@
+---
+title: Backbone
+layout: default
+parent: Operations
+grand_parent: Flamapy as framework
+permalink: /framework/operations/backbone
+nav_order: 22
+
+flamapy_sat: true
+flamapy_bdd: false
+flamapy_fm: false
+flamapy_z3: false
+flamapy_diagnosis: false
+cmd: false
+facade: true
+python: true
+rest: false
+---
+
+# Backbone
+
+**Description**:
+Returns the backbone of the feature model: the set of features that must always be selected (core features) and those that must never be selected (dead features) across all valid configurations, grouped under `core` and `dead` keys.
+
+**Application**:
+Provides a compact summary of the rigid parts of a product line in a single call, useful for model quality assessment.
+
+**Example**:
+Obtaining all features that are mandatory or impossible in a smartphone product line model.
+
+---
+## Code Examples
+
+### Python easy to use facade usage
+```python
+from flamapy.interfaces.python.flamapy_feature_model import FLAMAFeatureModel
+# Load the feature model
+fm = FLAMAFeatureModel("path/to/feature/model")
+# Returns {'core': [...], 'dead': [...]}
+result = fm.backbone()
+print(result)
+```
+
+### Python flamapy framework usage
+```python
+from flamapy.core.discover import DiscoverMetamodels
+# Initialize the discover metamodel
+dm = DiscoverMetamodels()
+# Call the operation. Transformations will be automatically executed
+result = dm.use_operation_from_file("PySATBackbone", "path/to/feature/model")
+print(result)
+```
+### Python flamapy framework **ADVANCED** usage
+```python
+from flamapy.core.discover import DiscoverMetamodels
+# Initialize the discover metamodel
+dm = DiscoverMetamodels()
+# Get the fm metamodel representation
+feature_model = dm.use_transformation_t2m("path/to/feature/model", 'fm')
+# Manually call a M2M transformation to PySAT
+sat_model = dm.use_transformation_m2m(feature_model, "pysat")
+# Get the operation
+operation = dm.get_operation(sat_model, 'PySATBackbone')
+# Execute the operation
+operation.execute(sat_model)
+# Get and print the result
+result = operation.get_result()
+print(result)
+```

_operations/commonality.md

@@ -9,6 +9,8 @@ nav_order: 1
 flamapy_sat: true
 flamapy_bdd: true
 flamapy_fm: false
+flamapy_z3: false
+flamapy_diagnosis: false
 cmd: true
 facade: true
 python: true