added LICENSE

10 files changed, 100 insertions, 0 deletions

diff --git a/fashion_mnist/fashion_mnist.py b/examples/fashion_mnist/fashion_mnist.py
index 1c9dcf7..1c9dcf7 100644
--- a/fashion_mnist/fashion_mnist.py
+++ b/examples/fashion_mnist/fashion_mnist.py
diff --git a/fashion_mnist/fashion_mnist_argmax.vnnlib b/examples/fashion_mnist/fashion_mnist_argmax.vnnlib
index 0c4412b..0c4412b 100644
--- a/fashion_mnist/fashion_mnist_argmax.vnnlib
+++ b/examples/fashion_mnist/fashion_mnist_argmax.vnnlib
diff --git a/fashion_mnist/fashion_mnist_epsilon.vnnlib b/examples/fashion_mnist/fashion_mnist_epsilon.vnnlib
index 948e501..948e501 100644
--- a/fashion_mnist/fashion_mnist_epsilon.vnnlib
+++ b/examples/fashion_mnist/fashion_mnist_epsilon.vnnlib
diff --git a/fashion_mnist/fashion_mnist_strict.vnnlib b/examples/fashion_mnist/fashion_mnist_strict.vnnlib
index 8242c34..8242c34 100644
--- a/fashion_mnist/fashion_mnist_strict.vnnlib
+++ b/examples/fashion_mnist/fashion_mnist_strict.vnnlib
diff --git a/examples/verify_fashion_mnist.py b/examples/verify_fashion_mnist.py
new file mode 100644
index 0000000..4de0d1e
--- /dev/null
+++ b/examples/verify_fashion_mnist.py
@@ -0,0 +1,50 @@
+# Copyright (C) 2026 Eric Marin
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Affero General Public License as
+# published by the Free Software Foundation, either version 3 of the
+# License, or (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Affero General Public License for more details.
+#
+# You should have received a copy of the GNU Affero General Public License
+# along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+import sys, os
+sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+
+import z3
+import nneq
+
+def check_property(onnx_a, onnx_b, vnnlib):
+    solver = nneq.Solver()
+    
+    print(f"--- Checking {vnnlib} ---")
+    
+    solver.load_onnx(onnx_a)
+    solver.load_onnx(onnx_b)
+    solver.load_vnnlib(vnnlib)
+    
+    result = solver.check()
+    
+    if result == z3.unsat:
+        print("VERIFIED (UNSAT): The networks are equivalent under this property.")
+    elif result == z3.sat:
+        print("FAILED (SAT): The networks are NOT equivalent.")
+        print("Counter-example input:")
+        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_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_strict.vnnlib")
+    check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_epsilon.vnnlib")
+    check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_argmax.vnnlib")
diff --git a/examples/verify_xor.py b/examples/verify_xor.py
new file mode 100644
index 0000000..f1de0cb
--- /dev/null
+++ b/examples/verify_xor.py
@@ -0,0 +1,50 @@
+# Copyright (C) 2026 Eric Marin
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Affero General Public License as
+# published by the Free Software Foundation, either version 3 of the
+# License, or (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Affero General Public License for more details.
+#
+# You should have received a copy of the GNU Affero General Public License
+# along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+import sys, os
+sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+
+import z3
+import nneq
+
+def check_property(onnx_a, onnx_b, vnnlib):
+    solver = nneq.Solver()
+    
+    print(f"--- Checking {vnnlib} ---")
+    
+    solver.load_onnx(onnx_a)
+    solver.load_onnx(onnx_b)
+    solver.load_vnnlib(vnnlib)
+    
+    result = solver.check()
+    
+    if result == z3.unsat:
+        print("VERIFIED (UNSAT): The networks are equivalent under this property.")
+    elif result == z3.sat:
+        print("FAILED (SAT): The networks are NOT equivalent.")
+        print("Counter-example input:")
+        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_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_strict.vnnlib")
+    check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_epsilon.vnnlib")
+    check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_argmax.vnnlib")
diff --git a/xor/xor.py b/examples/xor/xor.py
index ebc5477..ebc5477 100644
--- a/xor/xor.py
+++ b/examples/xor/xor.py
diff --git a/xor/xor_argmax.vnnlib b/examples/xor/xor_argmax.vnnlib
index d38bc31..d38bc31 100644
--- a/xor/xor_argmax.vnnlib
+++ b/examples/xor/xor_argmax.vnnlib
diff --git a/xor/xor_epsilon.vnnlib b/examples/xor/xor_epsilon.vnnlib
index 427243e..427243e 100644
--- a/xor/xor_epsilon.vnnlib
+++ b/examples/xor/xor_epsilon.vnnlib
diff --git a/xor/xor_strict.vnnlib b/examples/xor/xor_strict.vnnlib
index bead476..bead476 100644
--- a/xor/xor_strict.vnnlib
+++ b/examples/xor/xor_strict.vnnlib