Take in a .nnet filename with path and load the network from the file Inputs: filename - const char* that specifies the name and path of file Outputs

The main program

Function to generate equations corresponding to given operation Args: op: (tf.op) for which to generate equations :meta

Recursively populates self.shapeMap, self.varMap, and self.constantMap while adding equations and constraints Args: nodeName (str

Compute the shape and values of a node assuming the input shapes and values have been computed already. Args: nodeName (str): Nam

Function to generate equations corresponding to matrix multiplication Args: op: (tf.op) representing matrix multiplication operat

Function to generate equations corresponding to matrix multiplication Args: node (node): ONNX node representing the MatMul operat

Function to generate maxpooling equations Args: op: (tf.op) representing maxpool operation :meta private:

Function to generate maxpooling equations Args: node (node): ONNX node representing maxpool operation makeEquations (

Function to generate equations corresponding to multiply and divide operations Args: op: (tf.op) representing an element-wise mul

This callback will be invoked when the tableau size changes, typically when new variables are added. */

Analyze command line arguments

Read an ONNX file and create a MarabouNetworkONNX object :meta private:

* Pops the key at the front of the list off and removes its key from the map. */

* Pops the back of the stack until the size is below s. */

Print CxxTest version and exit

Processes the ONNX graph to produce Marabou equations :meta private:

* @brief Processes the graph, adding all the generated constraints to the query. * Unlike the Python implementation, at the moment assumes there is o

* Inserts an element into the map, and pushes its key onto the * back on the stack. The key inserted must be not be currently mapped. */

Read a tensorflow file to create a MarabouNetworkTF object Args: filename (str): Path to tensorflow network inputName

Function to generate equations corresponding to pointwise Relu Args: op: (tf.op) representing Relu operation :meta priva

Function to generate equations corresponding to pointwise Relu Args: node (node): ONNX node representing the Relu operation

Add current suite to list

Function to generate equations corresponding to resize Args: node (node): ONNX node representing the Resize operation

Body of TestDescription::run()

Run marabou and assert the result is according to the expected_result :param marabou_binary: path to marabou executable :param network_pa

Run marabou and assert the result is according to the expected_result :param marabou_binary: path to marabou executable :param network_pa

Run marabou and assert the result is according to the expected_result :param marabou_binary: path to marabou executable :param network_pa