Removed Z3

Author: jmafoster1

causal_testing/specification/scenario.py

@@ -3,7 +3,6 @@
 from collections.abc import Iterable, Mapping
 
 from tabulate import tabulate
-from z3 import ExprRef, substitute
 
 from .variable import Input, Meta, Output, Variable
 
@@ -20,15 +19,15 @@ class Scenario:
     accordingly.
 
     :param {Variable} variables: The set of endogenous variables.
-    :param {ExprRef} constraints: The set of constraints relating the endogenous variables.
+    :param {str} constraints: The set of constraints relating the endogenous variables.
     :attr variables:
     :attr constraints:
     """
 
     variables: Mapping[str, Variable]
-    constraints: set[ExprRef]
+    constraints: set[str]
 
-    def __init__(self, variables: Iterable[Variable] = None, constraints: set[ExprRef] = None):
+    def __init__(self, variables: Iterable[Variable] = None, constraints: set[str] = None):
         if variables is not None:
             self.variables = {v.name: v for v in variables}
         else:
@@ -106,10 +105,6 @@ def setup_treatment_variables(self) -> None:
             self.prime[k] = v_prime.name
             self.unprime[v_prime.name] = k
 
-        substitutions = {(self.variables[n].z3, self.treatment_variables[n].z3) for n in self.variables}
-        treatment_constraints = {substitute(c, *substitutions) for c in self.constraints}
-        self.constraints = self.constraints.union(treatment_constraints)
-
     def variables_of_type(self, t: type) -> set[Variable]:
         """Get the set of scenario variables of a particular type, e.g. Inputs.
 

causal_testing/specification/variable.py

@@ -1,53 +1,16 @@
-"""This module contains the Variable abstract class, as well as its concrete extensions: Input, Output and Meta. The
-function z3_types and the private function _coerce are also in this module."""
+"""This module contains the Variable abstract class, as well as its concrete extensions: Input, Output and Meta."""
 
 from __future__ import annotations
 from abc import ABC
 from collections.abc import Callable
-from enum import Enum
 from typing import Any, TypeVar
 
 import lhsmdu
 from pandas import DataFrame
 from scipy.stats._distn_infrastructure import rv_generic
-from z3 import Bool, BoolRef, Const, EnumSort, Int, RatNumRef, Real, String
 
 # Declare type variable
 T = TypeVar("T")
-z3 = TypeVar("Z3")
-
-
-def z3_types(datatype: T) -> z3:
-    """Cast datatype to Z3 datatype
-    :param datatype: python datatype to be cast
-    :return: Type name compatible with Z3 library
-    """
-    types = {int: Int, str: String, float: Real, bool: Bool}
-    if datatype in types:
-        return types[datatype]
-    if issubclass(datatype, Enum):
-        dtype, _ = EnumSort(datatype.__name__, [str(x.value) for x in datatype])
-        return lambda x: Const(x, dtype)
-    if hasattr(datatype, "to_z3"):
-        return datatype.to_z3()
-    raise ValueError(
-        f"Cannot convert type {datatype} to Z3."
-        + " Please use a native type, an Enum, or implement a conversion manually."
-    )
-
-
-def _coerce(val: Any) -> Any:
-    """Coerce Variables to their Z3 equivalents if appropriate to do so,
-    otherwise assume literal constants.
-
-    :param any val: A value, possibly a Variable.
-    :return: Either a Z3 ExprRef representing the variable or the original value.
-    :rtype: Any
-
-    """
-    if isinstance(val, Variable):
-        return val.z3
-    return val
 
 
 class Variable(ABC):
@@ -56,7 +19,6 @@ class Variable(ABC):
     :param str name: The name of the variable.
     :param T datatype: The datatype of the variable.
     :param rv_generic distribution: The expected distribution of the variable values.
-    :attr type z3: The Z3 mirror of the variable.
     :attr name:
     :attr datatype:
     :attr distribution:
@@ -70,125 +32,12 @@ class Variable(ABC):
     def __init__(self, name: str, datatype: T, distribution: rv_generic = None, hidden: bool = False):
         self.name = name
         self.datatype = datatype
-        self.z3 = z3_types(datatype)(name)
         self.distribution = distribution
         self.hidden = hidden
 
     def __repr__(self):
         return f"{self.typestring()}: {self.name}::{self.datatype.__name__}"
 
-    # Thin wrapper for Z1 functions
-
-    def __add__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self + other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self + other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__add__(_coerce(other))
-
-    def __ge__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self >= other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self >= other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__ge__(_coerce(other))
-
-    def __gt__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self > other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self > other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__gt__(_coerce(other))
-
-    def __le__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self <= other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self <= other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__le__(_coerce(other))
-
-    def __lt__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self < other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self < other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__lt__(_coerce(other))
-
-    def __mod__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self % other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self % other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__mod__(_coerce(other))
-
-    def __mul__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self * other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self * other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__mul__(_coerce(other))
-
-    def __ne__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self != other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self != other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__ne__(_coerce(other))
-
-    def __neg__(self) -> BoolRef:
-        """Create the Z3 expression `-self`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `-self`.
-        :rtype: BoolRef
-        """
-        return self.z3.__neg__()
-
-    def __pow__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self ^ other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self ^ other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__pow__(_coerce(other))
-
-    def __sub__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self - other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self - other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__sub__(_coerce(other))
-
-    def __truediv__(self, other: Any) -> BoolRef:
-        """Create the Z3 expression `self / other`.
-
-        :param any other: The object to compare against.
-        :return: The Z3 expression `self / other`.
-        :rtype: BoolRef
-        """
-        return self.z3.__truediv__(_coerce(other))
-
-    # End thin wrapper
-
     def cast(self, val: Any) -> T:
         """Cast the supplied value to the datatype T of the variable.
 
@@ -209,16 +58,6 @@ def cast(self, val: Any) -> T:
             return self.datatype(val)
         return self.datatype(str(val))
 
-    def z3_val(self, z3_var, val: Any) -> T:
-        """Cast value to Z3 value"""
-        native_val = self.cast(val)
-        if isinstance(native_val, Enum):
-            values = [z3_var.sort().constructor(c)() for c in range(z3_var.sort().num_constructors())]
-            values = [v for v in values if val.__class__(str(v)) == val]
-            assert len(values) == 1, f"Expected {values} to be length 1"
-            return values[0]
-        return native_val
-
     def sample(self, n_samples: int) -> [T]:
         """Generate a Latin Hypercube Sample of size n_samples according to the
         Variable's distribution.

causal_testing/surrogate/surrogate_search_algorithms.py

@@ -98,6 +98,7 @@ def create_gene_types(
             var_space[adj] = {}
 
         for relationship in list(specification.scenario.constraints):
+            print(relationship)
             rel_split = str(relationship).split(" ")
 
             if rel_split[0] in var_space:
@@ -109,7 +110,6 @@ def create_gene_types(
                         var_space[rel_split[0]]["high"] = int(rel_split[2]) + 1
                     else:
                         var_space[rel_split[0]]["high"] = datatype(rel_split[2])
-
         gene_space = []
         gene_space.append(var_space[surrogate_model.treatment])
         for adj in surrogate_model.adjustment_set:

dafni/main_dafni.py

@@ -126,9 +126,6 @@ def validate_variables(data_dict: dict) -> tuple:
 
         constraints = set()
 
-        for variable, input_var in zip(variables, inputs):
-            if "constraint" in variable:
-                constraints.add(input_var.z3 == variable["constraint"])
     else:
         raise ValidationError("Cannot find the variables defined by the causal tests.")
 

pyproject.toml

@@ -15,7 +15,6 @@ requires-python = ">=3.10"
 license = { text = "MIT" }
 keywords = ["causal inference", "verification"]
 dependencies = [
-    "z3_solver~=4.11.2", # z3_solver does not follow semantic versioning and tying to 4.11 introduces problems
     "fitter~=1.7",
     "lifelines~=0.29.0",
     "lhsmdu~=1.1",

tests/json_front_tests/test_json_class.py

@@ -99,13 +99,9 @@ def test_f_flag(self):
         }
         self.json_class.test_plan = example_test
         effects = {"NoEffect": NoEffect()}
-        mutates = {
-            "Increase": lambda x: self.json_class.scenario.treatment_variables[x].z3
-            > self.json_class.scenario.variables[x].z3
-        }
         estimators = {"LinearRegressionEstimator": LinearRegressionEstimator}
         with self.assertRaises(StatisticsError):
-            self.json_class.run_json_tests(effects, estimators, True, mutates)
+            self.json_class.run_json_tests(effects, estimators, True)
 
     def test_generate_coefficient_tests_from_json(self):
         example_test = {
@@ -149,15 +145,9 @@ def test_run_json_tests_from_json(self):
         }
         self.json_class.test_plan = example_test
         effects = {"NoEffect": NoEffect()}
-        mutates = {
-            "Increase": lambda x: self.json_class.scenario.treatment_variables[x].z3
-            > self.json_class.scenario.variables[x].z3
-        }
         estimators = {"LinearRegressionEstimator": LinearRegressionEstimator}
 
-        test_results = self.json_class.run_json_tests(
-            effects=effects, estimators=estimators, f_flag=False, mutates=mutates
-        )
+        test_results = self.json_class.run_json_tests(effects=effects, estimators=estimators, f_flag=False)
         self.assertTrue(test_results[0]["failed"])
 
     def test_generate_tests_from_json_no_dist(self):
@@ -176,13 +166,9 @@ def test_generate_tests_from_json_no_dist(self):
         }
         self.json_class.test_plan = example_test
         effects = {"NoEffect": NoEffect()}
-        mutates = {
-            "Increase": lambda x: self.json_class.scenario.treatment_variables[x].z3
-            > self.json_class.scenario.variables[x].z3
-        }
         estimators = {"LinearRegressionEstimator": LinearRegressionEstimator}
 
-        self.json_class.run_json_tests(effects=effects, mutates=mutates, estimators=estimators, f_flag=False)
+        self.json_class.run_json_tests(effects=effects, estimators=estimators, f_flag=False)
 
         # Test that the final log message prints that failed tests are printed, which is expected behaviour for this scenario
         with open("temp_out.txt", "r") as reader:
@@ -206,13 +192,9 @@ def test_formula_in_json_test(self):
         }
         self.json_class.test_plan = example_test
         effects = {"Positive": Positive()}
-        mutates = {
-            "Increase": lambda x: self.json_class.scenario.treatment_variables[x].z3
-            > self.json_class.scenario.variables[x].z3
-        }
         estimators = {"LinearRegressionEstimator": LinearRegressionEstimator}
 
-        self.json_class.run_json_tests(effects=effects, mutates=mutates, estimators=estimators, f_flag=False)
+        self.json_class.run_json_tests(effects=effects, estimators=estimators, f_flag=False)
         with open("temp_out.txt", "r") as reader:
             temp_out = reader.readlines()
         self.assertIn("test_output ~ test_input", "".join(temp_out))
@@ -282,13 +264,9 @@ def add_modelling_assumptions(self):
         }
         self.json_class.test_plan = example_test
         effects = {"Positive": Positive()}
-        mutates = {
-            "Increase": lambda x: self.json_class.scenario.treatment_variables[x].z3
-            > self.json_class.scenario.variables[x].z3
-        }
         estimators = {"ExampleEstimator": ExampleEstimator}
         with self.assertRaises(TypeError):
-            self.json_class.run_json_tests(effects=effects, mutates=mutates, estimators=estimators, f_flag=False)
+            self.json_class.run_json_tests(effects=effects, estimators=estimators, f_flag=False)
 
     def tearDown(self) -> None:
         if os.path.exists("temp_out.txt"):