Z3Constraint(): remove the @var_types parameter

Relevant Z3 types are now automatically detected for mapping
INT()-based or String()-based nodes

data_models/tutorial/tuto.py

@@ -672,7 +672,6 @@ def keycode_helper(blob, constraints, node_internals):
                               "And([SubSeq(delim_1, 1, 1) == '[', delim_2 == ']'])"
                               "])",
                      vars=('delim_1', 'delim_2'),
-                     var_types={'delim_1': z3.String, 'delim_2': z3.String},
                  ),
              ],
              'constraints_highlight': True,

docs/source/data_model.rst

@@ -2076,7 +2076,7 @@ instead of :class:`framework.constraint_helpers.Constraint` and provide a Z3 for
 
 .. code-block:: python
    :linenos:
-   :emphasize-lines: 12, 21
+   :emphasize-lines: 20
 
         csp_str_desc = \
             {'name': 'csp_str',
@@ -2089,7 +2089,6 @@ instead of :class:`framework.constraint_helpers.Constraint` and provide a Z3 for
                               "And([SubSeq(delim_1, 1, 1) == '[', delim_2 == ']'])"
                               "])",
                      vars=('delim_1', 'delim_2'),
-                     var_types={'delim_1': z3.String, 'delim_2': z3.String},
                  ),
              ],
              'constraints_highlight': True,
@@ -2115,12 +2114,9 @@ instead of :class:`framework.constraint_helpers.Constraint` and provide a Z3 for
 
 
 One difference with :class:`framework.constraint_helpers.Z3Constraint` is that you may provide Z3 formulas
-using variables of different kinds, namely integers and character strings.
-By default, variables will be interpreted as integers, and Z3 integer variables will be created
-to represent them. If you need to describe constraints between ``String()`` nodes, then you have to
-specify that the corresponding variables within the formula are strings. This will be done through
-the ``var_types`` parameter expecting a dictionary, mapping variable names to a Z3 variable type
-(l.12 in the example).
+using variables of different kinds, namely integers and character strings. Note that the Z3 variable
+types relevant for mapping ``INT()``-based or ``String()``-based nodes will be automatically created
+for you (respectively ``z3.Int`` and ``z3.String``).
 
 .. note::
 
@@ -2135,7 +2131,7 @@ with the parameter ``restrict_csp``. This is what is performed by the :class:`fr
 infrastructure when walking a specific node which is part of a CSP, so that the walked node won't be modified
 further to the CSP solving process.
 
-Finally, if ever ``INT()-based`` or ``String()-based`` nodes have default values (like in the example above l.21),
+Finally, if ever ``INT()``-based or ``String()``-based nodes have default values (like in the example above l.20),
 the first generated data will be compliant with the specified CSP as well as the default values.
 If no solution is found for the CSP with the default values, a :class:`framework.constraint_helpers.ConstraintError`
 exception will be raised.

framework/constraint_helpers.py

@@ -91,7 +91,7 @@ class Z3Constraint(object):
     _orig_relation = None
     _is_relation_translated = None
 
-    def __init__(self, relation, vars: Tuple, var_to_varns: dict = None, var_types: dict = None):
+    def __init__(self, relation, vars: Tuple, var_to_varns: dict = None):
         """
 
         Args:
@@ -104,15 +104,6 @@ def __init__(self, relation, vars: Tuple, var_to_varns: dict = None, var_types:
 
         self.vars = vars
         self.var_to_varns = var_to_varns
-        self.var_types = var_types
-        self.z3vars = {}
-        for v in vars:
-            if self.var_types is not None and self.var_types[v] is not None:
-                v_type = self.var_types[v]
-            else:
-                v_type = None
-            self.z3vars[v] = v_type(v) if v_type else Int(v)
-
         self._is_relation_translated = False
         self.relation = self._orig_relation = relation
 
@@ -200,8 +191,6 @@ def __init__(self, constraints: Constraint or Z3Constraint or List[Constraint or
                 r_copy = copy.copy(r)
                 self._constraints.append(r_copy)
                 self._vars += r_copy.vars
-                if self.z3_problem and r_copy.var_types:
-                    self._var_types.update(r_copy.var_types)
                 if r_copy.var_to_varns:
                     if self._var_to_varns is None:
                         self._var_to_varns = {}
@@ -210,16 +199,30 @@ def __init__(self, constraints: Constraint or Z3Constraint or List[Constraint or
                         if v not in r_copy.var_to_varns:
                             self._var_to_varns[v] = v
 
-                if isinstance(r, Z3Constraint):
-                    self._z3vars.update(r_copy.z3vars)
-
         self._var_node_mapping = {}
         self._var_domain = {}
         self._var_default_value = {}
         self._var_domain_updated = False
 
         self.highlight_variables = highlight_variables
 
+    def freeze(self):
+        if self.z3_problem:
+            for r in self._constraints:
+                for var in r.vars:
+                    dom = self._var_domain[var]
+                    # print(f'\n*** DEBUG: var:{var}, type:{type(dom[0])}')
+                    if isinstance(dom[0], int):
+                        self._var_types[var] = z3.Int
+                    elif isinstance(dom[0], bytes):
+                        self._var_types[var] = z3.String
+                    else:
+                        raise NotImplementedError
+
+                    self._z3vars[var] = self._var_types[var](var)
+
+        self.save_current_var_domains()
+
     def reset(self):
         # print(f'\n*** DBG RESET - info:'
         #       f'\n --> variables: {self._vars}'

framework/node_builder.py

@@ -881,7 +881,7 @@ def _setup_constraints(self, node, constraints, root_namespace, constraint_highl
                                    max=nd.cc.value_type.maxi_gen,
                                    default=default_val)
 
-        csp.save_current_var_domains()
+        csp.freeze()
         node.set_csp(csp)
 
 class State(object):