added FashionMNIST

xd

1 files changed, 9 insertions, 8 deletions

diff --git a/verify_xor.py b/verify_xor.py
index 7328229..90623a0 100644
--- a/verify_xor.py
+++ b/verify_xor.py
@@ -1,7 +1,7 @@
 import z3
 import nneq
 
-def check_equivalence(onnx_a, onnx_b, vnnlib):
+def check_property(onnx_a, onnx_b, vnnlib):
     solver = nneq.Solver()
     
     print(f"--- Checking {vnnlib} ---")
@@ -17,15 +17,16 @@ def check_equivalence(onnx_a, onnx_b, vnnlib):
     elif result == z3.sat:
         print("FAILED (SAT): The networks are NOT equivalent.")
         print("Counter-example input:")
-        m = solver.model()
-        sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name())
-        for s in sorted_symbols:
-            print(f"  {s.name()} = {m[s]}")
+        print(solver.model())
+        # m = solver.model()
+        # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name())
+        # for s in sorted_symbols:
+            # print(f"  {s.name()} = {m[s]}")
     else:
         print("UNKNOWN")
     print("")
 
 if __name__ == "__main__":
-    check_equivalence("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_strict.vnnlib")
-    check_equivalence("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_epsilon.vnnlib")
-    check_equivalence("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_argmax.vnnlib")
+    check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_strict.vnnlib")
+    check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_epsilon.vnnlib")
+    check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_argmax.vnnlib")