Drop support for Tensorflow and fix MacOS bug in unit test to pass CI…

… tests (#827)

* fix unit test and CI

* bump python version

* test

* remove test

* test_sub

* add network

* add a test for Sub

* remove local robustness method

.github/workflows/ci.yml

@@ -52,7 +52,7 @@ jobs:
 
       - uses: actions/setup-python@v5
         with:
-          python-version: "3.8"
+          python-version: "3.9"
 
       - name: Install system packages
         if: runner.os == 'Linux'

CHANGELOG.md

@@ -1,6 +1,7 @@
 # Changelog
 
 ## Next Release
+  - Dropped support for parsing Tensorflow network format. Newest Marabou version that supports Tensorflow is at commit 190555573e4702.
 
 ## Version 2.0.0
 

maraboupy/Marabou.py

@@ -21,10 +21,6 @@
     from maraboupy.MarabouNetworkNNet import *
 except ImportError:
     warnings.warn("NNet parser is unavailable because the numpy package is not installed")
-try:
-    from maraboupy.MarabouNetworkTF import *
-except ImportError:
-    warnings.warn("Tensorflow parser is unavailable because tensorflow package is not installed")
 try:
     from maraboupy.MarabouNetworkONNX import *
 except ImportError:
@@ -43,24 +39,6 @@ def read_nnet(filename, normalize=False):
     """
     return MarabouNetworkNNet(filename, normalize=normalize)
 
-
-def read_tf(filename, inputNames=None, outputNames=None, modelType="frozen", savedModelTags=[]):
-    """Constructs a MarabouNetworkTF object from a frozen Tensorflow protobuf
-
-    Args:
-        filename (str): Path to tensorflow network
-        inputNames (list of str, optional): List of operation names corresponding to inputs
-        outputNames (list of str, optional): List of operation names corresponding to outputs
-        modelType (str, optional): Type of model to read. The default is "frozen" for a frozen graph.
-                            Can also use "savedModel_v1" or "savedModel_v2" for the SavedModel format
-                            created from either tensorflow versions 1.X or 2.X respectively.
-        savedModelTags (list of str, optional): If loading a SavedModel, the user must specify tags used, default is []
-
-    Returns:
-        :class:`~maraboupy.MarabouNetworkTF.MarabouNetworkTF`
-    """
-    return MarabouNetworkTF(filename, inputNames, outputNames, modelType, savedModelTags)
-
 def read_onnx(filename, inputNames=None, outputNames=None):
     """Constructs a MarabouNetworkONNX object from an ONNX file
 

maraboupy/MarabouNetwork.py

@@ -105,7 +105,7 @@ def calculateBounds(self, filename="", verbose=True, options=None):
         if options == None:
             options = MarabouCore.Options()
         exitCode, bounds, stats = MarabouCore.calculateBounds(ipq, options, str(filename))
-        
+
         if verbose:
             print(exitCode)
             if exitCode == "":
@@ -115,95 +115,6 @@ def calculateBounds(self, filename="", verbose=True, options=None):
 
         return [exitCode, bounds, stats]
 
-    def evaluateLocalRobustness(self, input, epsilon, originalClass, verbose=True, options=None, targetClass=None):
-        """Function evaluating a specific input is a local robustness within the scope of epslion
-
-        Args:
-            input (numpy.ndarray): Target input
-            epsilon (float): L-inf norm of purturbation
-            originalClass (int): Output class of a target input
-            verbose (bool): If true, print out solution after solve finishes
-            options (:class:`~maraboupy.MarabouCore.Options`): Object for specifying Marabou options, defaults to None
-            targetClass (int): If set, find a feasible solution with which the value of targetClass is max within outputs.
-
-        Returns:
-            (tuple): tuple containing:
-                - vals (Dict[int, float]): Empty dictionary if UNSAT, otherwise a dictionary of SATisfying values for variables
-                - stats (:class:`~maraboupy.MarabouCore.Statistics`): A Statistics object to how Marabou performed
-                - maxClass (int): Output class which value is max within outputs if SAT.
-        """
-        inputVars = None
-        if (type(self.inputVars) is list):
-            if (len(self.inputVars) != 1):
-                raise NotImplementedError("Operation for %d inputs is not implemented" % len(self.inputVars))
-            inputVars = self.inputVars[0][0]
-        elif (type(self.inputVars) is np.ndarray):
-            inputVars = self.inputVars[0]
-        else:
-            err_msg = "Unpexpected type of input vars."
-            raise RuntimeError(err_msg)
-
-        if inputVars.shape != input.shape:
-            raise RuntimeError("Input shape of the model should be same as the input shape\n input shape of the model: {0}, shape of the input: {1}".format(inputVars.shape, input.shape))
-
-        if (type(self.outputVars) is list):
-            if (len(self.outputVars) != 1):
-                raise NotImplementedError("Operation for %d outputs is not implemented" % len(self.outputVars))
-        elif (type(self.outputVars) is np.ndarray):
-            if (len(self.outputVars) != 1):
-                raise NotImplementedError("Operation for %d outputs is not implemented" % len(self.outputVars))
-        else:
-            err_msg = "Unpexpected type of output vars."
-            raise RuntimeError(err_msg)
-
-        if options == None:
-            options = MarabouCore.Options()
-
-        # Add constratins to all input nodes
-        flattenInputVars = inputVars.flatten()
-        flattenInput = input.flatten()
-        for i in range(flattenInput.size):
-            self.setLowerBound(flattenInputVars[i], flattenInput[i] - epsilon)
-            self.setUpperBound(flattenInputVars[i], flattenInput[i] + epsilon)
-
-        maxClass = None
-        outputStartIndex = self.outputVars[0][0][0]
-
-        if targetClass is None:
-            outputLayerSize = len(self.outputVars[0][0])
-            # loop for all of output classes except for original class
-            for outputLayerIndex in range(outputLayerSize):
-                if outputLayerIndex != originalClass:
-                    self.addMaxConstraint(set([outputStartIndex + outputLayerIndex, outputStartIndex + originalClass]), 
-                        outputStartIndex + outputLayerIndex)
-                    exitCode, vals, stats = self.solve(options = options)
-                    if (stats.hasTimedOut()):
-                        break
-                    elif (len(vals) > 0):
-                        maxClass = outputLayerIndex
-                        break
-        else:
-            self.addMaxConstraint(set(self.outputVars[0][0]), outputStartIndex + targetClass)
-            exitCode, vals, stats = self.solve(options = options)
-            if verbose:
-                if not stats.hasTimedOut() and len(vals) > 0:
-                    maxClass = targetClass
-
-        # print timeout, or feasible inputs and outputs if verbose is on.
-        if verbose:
-            if stats.hasTimedOut():
-                print("TO")
-            elif len(vals) > 0:
-                print("sat")
-                for j in range(len(self.inputVars[0])):
-                    for i in range(self.inputVars[0][j].size):
-                        print("input {} = {}".format(i, vals[self.inputVars[0][j].item(i)]))
-
-                for j in range(len(self.outputVars[0])):
-                    for i in range(self.outputVars[0][j].size):
-                        print("output {} = {}".format(i, vals[self.outputVars[0][j].item(i)]))
-
-        return [vals, stats, maxClass]
 
     def evaluateWithMarabou(self, inputValues, filename="evaluateWithMarabou.log", options=None):
         """Function to evaluate network at a given point using Marabou as solver