From 689c34076d08e59b1382864f9efcd983c8665ae5 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Mon, 23 Mar 2026 17:53:21 +0100 Subject: added FashionMNIST xd --- verify_xor.py | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'verify_xor.py') 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") -- cgit v1.2.3