diff options
Diffstat (limited to 'verify_xor.py')
| -rw-r--r-- | verify_xor.py | 17 |
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") |