From f59d01d0e8d8b1f5a53df34ab647fa3ee8da09d8 Mon Sep 17 00:00:00 2001 From: tagomaru Date: Wed, 3 Jan 2024 21:08:01 -0800 Subject: [PATCH] add test code --- maraboupy/test/test_network_composition.py | 121 +++++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 maraboupy/test/test_network_composition.py diff --git a/maraboupy/test/test_network_composition.py b/maraboupy/test/test_network_composition.py new file mode 100644 index 000000000..f4faf945c --- /dev/null +++ b/maraboupy/test/test_network_composition.py @@ -0,0 +1,121 @@ +# Tests MarabouNetwork features not tested by it's subclasses +from maraboupy import Marabou +from maraboupy import MarabouCore +import os +import numpy as np + +# Global settings +OPT = Marabou.createOptions(verbosity = 0) # Turn off printing +TOL = 1e-6 # Set tolerance for checking Marabou evaluations +NETWORK_FOLDER = "../../resources/nnet/" # Folder for test networks +NETWORK_ONNX_FOLDER = "../../resources/onnx/" # Folder for test networks in onnx format + +def test_zero_split_unknown(): + """ + Tests that a network with no splits is correctly read and solved as unknown + """ + filename = 'fc1.onnx' + filename = os.path.join(os.path.dirname(__file__), NETWORK_ONNX_FOLDER, filename) + network = Marabou.read_onnx_with_threshold(filename, maxNumberOfLinearEquations=100) + + # check that the network has one split + assert len(network.ipqs) == 1 + + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + exitCode, _, _ = network.solve(options=OPT) + + assert exitCode == "UNKNOWN" + +def test_zero_split_unsat(): + """ + Tests that a network with no splits is correctly read and solved as unsat + """ + filename = 'fc1.onnx' + filename = os.path.join(os.path.dirname(__file__), NETWORK_ONNX_FOLDER, filename) + network = Marabou.read_onnx_with_threshold(filename, maxNumberOfLinearEquations=100) + + # check that the network has no splits + assert len(network.ipqs) == 1 + + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + network.setLowerBound(network.outputVars[0][0][0], 100) + + exitCode, _, _ = network.solve(options=OPT) + + assert exitCode == "unsat" + + network = Marabou.read_onnx(filename) + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + network.setLowerBound(network.outputVars[0][0][0], 100) + + exitCode2, _, _ = network.calculateBounds(options=OPT) + + # exitCode2 should be also unsat + assert exitCode == exitCode2 + +def test_one_split_unknown(): + """ + Tests that a network with one split is correctly read and solved as unknown + """ + filename = 'fc1.onnx' + filename = os.path.join(os.path.dirname(__file__), NETWORK_ONNX_FOLDER, filename) + network = Marabou.read_onnx_with_threshold(filename, maxNumberOfLinearEquations=50) + + # check that the network has one split + assert len(network.ipqs) == 2 + + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + exitCode, _, _ = network.solve(options=OPT) + + assert exitCode == "UNKNOWN" + +def test_one_split_unsat(): + """ + Tests that a network with one split is correctly read and solved as unsat + """ + filename = 'fc1.onnx' + filename = os.path.join(os.path.dirname(__file__), NETWORK_ONNX_FOLDER, filename) + network = Marabou.read_onnx_with_threshold(filename, maxNumberOfLinearEquations=50) + + # check that the network has one split + assert len(network.ipqs) == 2 + + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + network.setLowerBound(network.outputVars[0][0][0], 100) + + exitCode, _, _ = network.solve(options=OPT) + + assert exitCode == "unsat" + + network = Marabou.read_onnx(filename) + network.setLowerBound(network.inputVars[0][0][0], 3) + network.setUpperBound(network.inputVars[0][0][0], 5) + network.setLowerBound(network.inputVars[0][0][1], 3) + network.setUpperBound(network.inputVars[0][0][1], 10) + + network.setLowerBound(network.outputVars[0][0][0], 100) + + exitCode2, _, _ = network.calculateBounds(options=OPT) + + # exitCode2 should be also unsat + assert exitCode == exitCode2 \ No newline at end of file