Marabou Integration

.gitignore

@@ -55,3 +55,12 @@ obj/table.c.o
 /regr_smlp/data/smlp_s2_tx.csv
 /regr_smlp/master/Test130_*.*
 /regr_smlp/master/Test131_*.*
+/result
+/data
+.idea
+src/logs.log
+*.pb
+*.h5
+*.onnx
+variables/
+saved_model/

Marabou-Abstract_Solvers.md

@@ -0,0 +1,36 @@
+
+# INFO: File Structure
+
+- src/smlp_py/NN_verifiers: contains scripts to test the marabou models and verify the validity of the conversion of pb files into h5 files.
+- src/smlp_py/marabou: helper files that contain examples of maraboupy commands.
+- src/smlp_py/smtlib:
+	- parser.py & smt_to_pysmt.py contain helper functions. They are not used in SMLP's pipeline.
+	- text_to_sympy.py: Contains all the logic of converting, simplifying and reformatting expressions to a state that is easily translated into marabou expressions.
+- src/smlp_py/solvers: This folder will contain all the logic of the external neural network verifiers that are going to be integrated into the SMLP pipeline.
+- src/smlp_py/vnnlib: Contains the logic for for the need in the future to utilise the VNNLIB format (solver agnostic, several solvers support this format) to interact with the solvers.
+
+
+# INFO: The abstract solver
+abstract_solver.py defines an abstract solver class that is used to interface all the functionalities that all integrated solvers must support. This is because the main flow has been updated to reference the abstract solver functionalities, and thus all functions must be overridden by every new solver.
+
+Some methods are optionally overridden as their content usually cover most use cases. 
+
+# HOW: Integrating multiple solvers
+In the solvers/ folder, each solver must have it own subfolder. Currently, z3 and marabou are the only supported solvers. Each solver must have 2 files:
+1) Operations.py :  this file contains the functions that are utilised during the formula building and processing part of the workflow. For example, the method #smlp_and contains the conjunction logic utilised within the formula building phase, in marabou's case, the conjunction operations take place by using pysmt. Whereas is z3's case, the operators library is used to manage the formulas. 
+2) solver.py : This file contains the class that extends our abstract solver and operations class. Consequently, it will have to override all the functions mentioned in the abstract solver class in order to function properly. 
+
+
+# INFO: How the universal solver class is used in the main worklfow
+The current PR contains changes in multiple files that contain core functionalities used in the main SMLP workflow. Re-usable parts of the flow or certain cases that are handled differently for each solver have been moved into the z3 solver and have been replaced with the universal solver class's functions. 
+The universal solver (universal_solver.py) acts as the intermediary and eventually point to the specified solver (marabou, z3), depending on the given "version" argument. Possible values are:
+
+```
+Solver.Version.PYSMT
+Solver.Version.FORM2
+
+```
+
+# INFO: Pysmt processing
+The file #text_to_sympy .py contains all the logic required to transform the formulas into marabou queries. 
+My dissertation can be used as a reference point to understand the underlying methodologies used inside each function. 

src/smlp_py/NN_verifiers/compare_models.py

@@ -0,0 +1,75 @@
+import tensorflow as tf
+import numpy as np
+import h5py
+
+
+def read_h5_weights(h5_file_path):
+    with h5py.File(h5_file_path, 'r') as f:
+        weights = {}
+        for layer_name in f.keys():
+            layer = f[layer_name]
+            for weight_name in layer.keys():
+                weights[layer_name + '/' + weight_name] = np.array(layer[weight_name])
+    return weights
+
+
+def verify_pb_file(pb_file_path):
+    # Verify the protobuf file is valid
+    try:
+        with tf.io.gfile.GFile(pb_file_path, "rb") as f:
+            graph_def = tf.compat.v1.GraphDef()
+            graph_def.ParseFromString(f.read())
+        return True
+    except tf.errors.InvalidArgumentError as e:
+        print(f"Error verifying the PB file: {e}")
+        return False
+
+
+def read_pb_weights(pb_file_path):
+    # Verify the file first
+    if not verify_pb_file(pb_file_path):
+        raise ValueError(f"The file at {pb_file_path} is not a valid TensorFlow protobuf file.")
+
+    # Load the protobuf graph
+    graph_def = tf.compat.v1.GraphDef()
+    with tf.io.gfile.GFile(pb_file_path, "rb") as f:
+        graph_def.ParseFromString(f.read())
+
+    # Import the graph and get the weights
+    with tf.compat.v1.Graph().as_default() as graph:
+        tf.import_graph_def(graph_def, name="")
+
+    weights = {}
+    with tf.compat.v1.Session(graph=graph) as sess:
+        for op in graph.get_operations():
+            if op.type == "Const":
+                weights[op.name] = sess.run(op.outputs[0])
+    return weights
+
+
+def compare_weights(h5_weights, pb_weights):
+    for key in h5_weights:
+        if key in pb_weights:
+            if np.allclose(h5_weights[key], pb_weights[key]):
+                print(f"Weights for {key} match.")
+            else:
+                print(f"Weights for {key} do not match.")
+        else:
+            print(f"Weight {key} not found in PB model.")
+
+    for key in pb_weights:
+        if key not in h5_weights:
+            print(f"Weight {key} not found in H5 model.")
+
+
+def check_weights(h5_file_path, pb_file_path):
+    h5_weights = read_h5_weights(h5_file_path)
+    pb_weights = read_pb_weights(pb_file_path)
+    compare_weights(h5_weights, pb_weights)
+
+
+# Example usage:
+# check_weights('path_to_model.h5', 'path_to_model.pb')
+
+# Example usage:
+check_weights("/home/ntinouldinho/Desktop/smlp/result/abc_smlp_toy_basic_nn_keras_model_complete.h5", "/home/ntinouldinho/Desktop/smlp/src/smlp_py/NN_verifiers/saved_model.pb")

src/smlp_py/NN_verifiers/test_marabou.py

@@ -0,0 +1,190 @@
+from src.smlp_py.NN_verifiers.verifiers import MarabouVerifier
+from src.smlp_py.smtlib.text_to_sympy import TextToPysmtParser
+
+from pysmt.shortcuts import Symbol, And, Not, Or, Implies, simplify, LT, Real, Times, Minus, Plus, Equals, GE, ToReal, LE
+from pysmt.typing import *
+import tf2onnx
+import numpy as np
+from pysmt.shortcuts import Symbol, Times, Minus, Div, Real
+from pysmt.smtlib.parser import get_formula
+# from pysmt.oracles import get_logic
+from pysmt.typing import REAL
+from z3 import simplify, parse_smt2_string
+import z3
+from pysmt.smtlib.script import smtlibscript_from_formula
+from io import StringIO
+
+from maraboupy.MarabouPythonic import *
+
+
+if __name__ == "__main__":
+    import numpy as np
+    from tensorflow.keras.models import load_model
+    import os
+
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    relative_h5_path = os.path.join(script_dir, '../../../result/abc_smlp_toy_basic_nn_keras_model_complete.h5')
+    absolute_h5_path = os.path.normpath(relative_h5_path)
+    # Load the model from the .h5 file
+    model = load_model(absolute_h5_path)
+
+    # Prepare your input data
+    input_data = np.array([[1.043789425, 0, 0.191919192, 0]])  # Example input data
+
+    # Pass the inputs to the model and get the outputs
+    outputs = model.predict(input_data)
+
+    # Print the outputs
+    print("Model outputs:", outputs)
+
+    from keras.models import load_model
+
+    # model = load_model("/home/kkon/Desktop/smlp/result/abc_smlp_toy_basic_nn_keras_model_complete.h5")
+    # model_proto, external_tensor_storage = tf2onnx.convert.from_keras(model, opset=13, output_path="smlp_toy.onnx")
+    print("SAVING TO ONNX")
+    parser = TextToPysmtParser()
+    parser.init_variables(symbols=[("x1", "real"), ('x2', 'real'), ('p1', 'real'), ('p2', 'real'),
+                                  ('y1', 'real'), ('y2', 'real')])
+
+    mb = MarabouVerifier(parser=parser)
+    mb.init_variables(inputs=[("x1", "Real"), ('x2', 'Integer'), ('p1', 'Real'), ('p2', 'Integer')],
+                      outputs=[('y1', 'Real'), ('y2', 'Real')])
+    mb.initialize()
+
+    smlp_formula = '(let ((|:0| (* (/ 281474976710656 2944425288877159) (- y1 (/ 1080863910568919 4503599627370496))))) (let ((|:1| (* (/ 281474976710656 2559564553220679) (- (* (/ 1 2) (+ y1 y2)) (/ 1170935903116329 1125899906842624))))) (>= (ite (< |:0| |:1|) |:0| |:1|) 1)))'
+    smlp_str = f"""
+                (declare-fun y1 () Real)
+                (declare-fun y2 () Real)
+                (assert {smlp_formula})
+                """
+
+    smlp_parsed = z3.parse_smt2_string(smlp_str)
+    smlp_simplified = z3.simplify(smlp_parsed[0])
+    ex = parser.parse(str(smlp_simplified))
+    # ex = parser.replace_constants_with_floats_and_evaluate(ex)
+    marabou_formula = parser.convert_ite_to_conjunctions_disjunctions(ex)
+    print(marabou_formula.serialize())
+
+
+
+
+
+    y1 = parser.get_symbol("y1")
+    y2 = parser.get_symbol("y2")
+    p1 = parser.get_symbol("p1")
+    p2 = parser.get_symbol("p2")
+    x1 = parser.get_symbol("x1")
+    x2 = parser.get_symbol("x2")
+
+    x2_int = parser.create_integer_disjunction("x2_unscaled", (-1, 1))
+    p2_int = parser.create_integer_disjunction("p2_unscaled", (3, 7))
+    # alpha = (((-1 <= x2) & (0.0 <= x1) & (x2 <= 1) & (x1 <= 10.0)) & (((p2 < 5) & (x1 == 10.0)) & (x2 < 12)))
+    # beta = ((4 <= y1) & (6 <= y2))
+
+
+    #  with x as input: y1==6.847101329531717 & y2==10.31207527363552
+    #  with x as knob:  y1==4.120704402283359 &
+    solution = And(
+        Equals(x1, Real(10)),
+        Equals(x2, Real(-1)),
+        Equals(p1, Real(2)),
+        Equals(p2, Real(3))
+    )
+
+    print(smtlibscript_from_formula(solution))
+    theta = And(
+        GE(p1, Real(6.8)),
+        GE(p2, Real(3.8)),
+        LE(p1, Real(7.2)),
+        LE(p2, Real(4.2))
+    )
+    alpha = And(
+        GE(x2, Real(-1)),
+        LE(x2, Real(1)),
+        GE(x1, Real(0.0)),
+        LE(x1, Real(10.0)),
+        And(
+            LT(p2, Real(5)),
+            Equals(x1, Real(10.0)),
+            LT(x2, Real(12))
+        )
+    )
+
+    beta = And(
+        GE(y1, Real(4)),
+        GE(y2, Real(8)),
+    )
+
+    not_beta = Or(
+        LT(y1, Real(4)),
+        LT(y2, Real(8))
+    )
+    eta = And(
+        GE(p1, Real(0.0)),
+        LE(p1, Real(10.0)),
+        GE(p2, Real(3)),
+        LE(p2, Real(7)),
+        Or(
+            p1.Equals(Real(2.0)),
+            p1.Equals(Real(4.0)),
+            p1.Equals(Real(7.0))
+        )
+    )
+    script = smtlibscript_from_formula(eta)
+
+    outstream = StringIO()
+    script.serialize(outstream)
+    output = outstream.getvalue()
+    smlp_parsed = z3.parse_smt2_string(output)
+    smlp_simplified = z3.simplify(smlp_parsed[0])
+    mb.apply_restrictions(x2_int)
+    mb.apply_restrictions(p2_int)
+    # mb.apply_restrictions(beta)
+    # mb.apply_restrictions(alpha)
+    # mb.apply_restrictions(eta)
+    # mb.apply_restrictions(marabou_formula)
+    mb.apply_restrictions(solution)
+
+    # mb.apply_restrictions(theta)
+
+    witness= mb.solve()
+    print(witness)
+
+##################  TEST PARSER ###########################
+# if __name__ == "__main__":
+#     parser = TextToPysmtParser()
+#     parser.init_variables(inputs=[("x1", "real"), ('x2', 'int'), ('p1', 'real'), ('p2', 'int'),
+#                                   ('y1', 'real'), ('y2', 'real')])
+#
+#     mb = MarabouVerifier(parser=parser)
+#     mb.init_variables(inputs=[("x1", "Real"), ('x2', 'Integer'), ('p1', 'Integer'), ('p2', 'Integer')],
+#                       outputs=[('y1', 'Real'), ('y2', 'Real')])
+#
+#
+#     # (1<=(ite)) and (y<=4) and (y>=8)
+#     # ite_without_ite = Or(And(c, t), And(Not(c), f))
+#
+#     y1 = parser.get_symbol("y1")
+#     y2 = parser.get_symbol("y2")
+#
+#     ex = parser.parse('(y1+y2)/2')
+#
+#     c = y1 > y2
+#     t = y1
+#     f = y2
+#     # ite_without_ite = Or(And(c, t), And(Not(c), f))
+#
+#     condition_true = Times(ToReal(c), y1)  # y1 if y1 > y2
+#     condition_false = Times(ToReal(Not(c)), y2)  # y2 if y1 <= y2
+#
+#     # Combine them
+#     ite_without_ite = Plus(condition_true, condition_false)
+#
+#     # Final expression (ite_without_ite >= 1)
+#     inequality = GE(ite_without_ite, Real(1))
+#
+#     # Combine with the inequality 1 <= ITE(c, t, f)
+#     # inequality = Real(1) <= ite_without_ite
+#     print(inequality)
+
+