diff options
| author | ericmarin <maarin.eric@gmail.com> | 2026-03-26 20:28:38 +0100 |
|---|---|---|
| committer | ericmarin <maarin.eric@gmail.com> | 2026-03-26 21:27:10 +0100 |
| commit | 3e338c3be65638ef1898c32c707c50422acafb18 (patch) | |
| tree | 80a29ac6b7baee3bbfe4f161fc893fd5948d9409 /verify_xor.py | |
| parent | 689c34076d08e59b1382864f9efcd983c8665ae5 (diff) | |
| download | vein-3e338c3be65638ef1898c32c707c50422acafb18.tar.gz vein-3e338c3be65638ef1898c32c707c50422acafb18.zip | |
added LICENSE
Diffstat (limited to 'verify_xor.py')
| -rw-r--r-- | verify_xor.py | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/verify_xor.py b/verify_xor.py deleted file mode 100644 index 90623a0..0000000 --- a/verify_xor.py +++ /dev/null @@ -1,32 +0,0 @@ -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("./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") |
