feat(z3): support the Tseytin CNF encoding as an opt-in

Add cnf_method='tseytin' to FmToZ3, applied only to purely propositional boolean
constraints (arithmetic, typed and aggregation constraints fall back to the
direct translation). Auxiliary variables are fresh, globally-unique Z3 booleans
kept out of the feature map so enumeration and bounds operations ignore them.
Z3 already clausifies internally, so this is provided for cross-backend
uniformity and experimentation rather than performance. Add parity and
fallback tests.

Author: José Ángel Galindo Duarte

flamapy/metamodels/z3_metamodel/models/z3_model.py

@@ -35,6 +35,9 @@ def __init__(self) -> None:
         self.attributes: dict[str, list[Any]] = {}  # attr_name -> [z3var]
         self.attributes_types: dict[str, AttributeType] = {}  # attr_name -> AttributeType
         self.constraints: list[Any] = []  # list of z3 expressions
+        # Auxiliary (Tseytin) boolean variables. Kept out of ``features`` so that feature
+        # enumeration/counting/bounds operations ignore them.
+        self.auxiliary_variables: list[Any] = []
         self.original_model: Optional[VariabilityModel] = None
 
     def create_const(self, ftype: FeatureType | AttributeType, value: Any) -> Any:

flamapy/metamodels/z3_metamodel/transformations/fm_to_z3.py

@@ -61,10 +61,16 @@ def get_source_extension() -> str:
     def get_destination_extension() -> str:
         return "z3"
 
-    def __init__(self, source_model: FeatureModel) -> None:
+    def __init__(self, source_model: FeatureModel, cnf_method: str = 'direct') -> None:
         self.source_model = source_model
         self.destination_model: Z3Model = Z3Model()
         self._counter: int = 0
+        # 'direct' (default) builds Z3 boolean expressions straight from the AST. 'tseytin'
+        # applies the Tseytin CNF encoding to purely propositional boolean constraints
+        # (others fall back to 'direct'). Framework-only opt-in; Z3 already clausifies
+        # internally, so this exists for cross-backend uniformity/experimentation, not speed.
+        self.cnf_method = cnf_method
+        self._aux_counter: int = 0
 
     def transform(self) -> Z3Model:
         self.destination_model = Z3Model()
@@ -258,9 +264,54 @@ def _add_cardinality_formula(self, relation: Relation) -> None:
         self._add_inactive_parent_constraints(parent, children)
 
     def _add_constraint_formula(self, ctc: Constraint) -> None:
+        if self.cnf_method == 'tseytin' and self._is_propositional_boolean(ctc):
+            self._add_tseytin_constraint(ctc)
+            return
         expr = self._get_expression(ctc.ast.root, None)
         self.destination_model.add_constraint(expr)
 
+    def _is_propositional_boolean(self, ctc: Constraint) -> bool:
+        """Whether a constraint is purely propositional over boolean features, i.e. safe
+        for the Tseytin CNF encoding. Arithmetic/aggregation/typed constraints are not."""
+        if any(op not in LOGICAL_OPERATORS for op in ctc.ast.get_operators()):
+            return False
+        for operand in ctc.ast.get_operands():
+            if not isinstance(operand, str):
+                return False
+            info = self.destination_model.get_variable(operand)
+            if info is None or info.ftype != FeatureType.BOOLEAN:
+                return False
+        return True
+
+    def _add_tseytin_constraint(self, ctc: Constraint) -> None:
+        clauses, aux_names = ctc.ast.get_clauses_with_aux(method='tseytin')
+        ctx = self.destination_model.ctx
+        # Fresh, globally-unique Z3 Bool per auxiliary name (same-named Bools in one Z3
+        # context are the same variable, so per-constraint names must not collide).
+        local: dict[str, Any] = {}
+        for name in aux_names:
+            self._aux_counter += 1
+            aux_var = z3.Bool(f'__tseytin_aux_{self._aux_counter}', ctx=ctx)
+            local[name] = aux_var
+            self.destination_model.auxiliary_variables.append(aux_var)
+
+        def literal_expr(term: str) -> Any:
+            negated = term.startswith('-')
+            name = term[1:] if negated else term
+            if name in local:
+                expr = local[name]
+            else:
+                info = self.destination_model.get_variable(name)
+                if info is None:
+                    raise FlamaException(f'Unsupported feature: {name}')
+                expr = info.sel
+            return z3.Not(expr) if negated else expr
+
+        for clause in clauses:
+            literals = [literal_expr(term) for term in clause]
+            formula = literals[0] if len(literals) == 1 else z3.Or(*literals)
+            self.destination_model.add_constraint(formula)
+
     def _get_expression(self, node: Node, parent: Optional[Node]) -> z3.ExprRef:
         if node.is_term():
             return self._get_term_expression(node, parent)

tests/test_tseytin.py

@@ -0,0 +1,69 @@
+"""The opt-in Tseytin CNF encoding must yield the same Z3 analysis results as the
+default direct translation, and must fall back to the direct translation for any
+constraint that is not purely propositional over boolean features."""
+import os
+import tempfile
+
+from flamapy.metamodels.fm_metamodel.transformations import UVLReader
+from flamapy.metamodels.z3_metamodel.transformations import FmToZ3
+from flamapy.metamodels.z3_metamodel.operations.z3_satisfiable import Z3Satisfiable
+from flamapy.metamodels.z3_metamodel.operations.z3_configurations import Z3Configurations
+from flamapy.metamodels.z3_metamodel.operations.z3_configurations_number import (
+    Z3ConfigurationsNumber,
+)
+
+
+# Purely propositional model: every cross-tree constraint is boolean.
+_PROP_UVL = """features
+    Root {abstract}
+        optional
+            A
+            B
+            C
+            D
+constraints
+    (A | B) => (C <=> D)
+    A => !B
+"""
+
+# All-arithmetic constraints; the Tseytin path must fall back to direct translation.
+_ARITH_MODEL = 'resources/models/uvl_models/fm03_integer_conditional_bounded.uvl'
+
+
+def _build_from_uvl_text(text, cnf_method):
+    handle, path = tempfile.mkstemp(suffix='.uvl')
+    try:
+        with os.fdopen(handle, 'w') as file:
+            file.write(text)
+        return FmToZ3(UVLReader(path).transform(), cnf_method=cnf_method).transform()
+    finally:
+        os.remove(path)
+
+
+def _projected(model):
+    configs = Z3Configurations().execute(model).get_result()
+    return {frozenset(k for k, v in c.elements.items() if v is True) for c in configs}
+
+
+def test_tseytin_matches_direct_on_propositional_model() -> None:
+    direct = _build_from_uvl_text(_PROP_UVL, 'direct')
+    tseytin = _build_from_uvl_text(_PROP_UVL, 'tseytin')
+
+    assert Z3ConfigurationsNumber().execute(direct).get_result() == \
+        Z3ConfigurationsNumber().execute(tseytin).get_result()
+    assert _projected(direct) == _projected(tseytin)
+    assert tseytin.auxiliary_variables  # gates were introduced
+    # Auxiliary variables must not have been registered as features.
+    assert not set(str(a) for a in tseytin.auxiliary_variables) & set(tseytin.features.keys())
+
+
+def test_tseytin_falls_back_for_arithmetic_constraints() -> None:
+    direct = FmToZ3(UVLReader(_ARITH_MODEL).transform(), cnf_method='direct').transform()
+    tseytin = FmToZ3(UVLReader(_ARITH_MODEL).transform(), cnf_method='tseytin').transform()
+
+    # Nothing was propositional, so no auxiliary variables were created.
+    assert tseytin.auxiliary_variables == []
+    assert Z3Satisfiable().execute(direct).get_result() == \
+        Z3Satisfiable().execute(tseytin).get_result()
+    assert Z3ConfigurationsNumber().execute(direct).get_result() == \
+        Z3ConfigurationsNumber().execute(tseytin).get_result()