From e2abe9d9ec649b849cc39b516c1db1b4fa592003 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Sat, 21 Mar 2026 11:47:40 +0100 Subject: created class --- verify_xor.py | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 verify_xor.py (limited to 'verify_xor.py') diff --git a/verify_xor.py b/verify_xor.py new file mode 100644 index 0000000..7328229 --- /dev/null +++ b/verify_xor.py @@ -0,0 +1,31 @@ +import z3 +import nneq + +def check_equivalence(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:") + 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") -- cgit v1.2.3