created class

8 files changed, 36 insertions, 13 deletions

diff --git a/xor.py b/xor/xor.py
index 82a16b8..ebc5477 100644
--- a/xor.py
+++ b/xor/xor.py
@@ -1,7 +1,6 @@
 import torch
 import torch.nn as nn
 import torch.onnx
-import nneq
 
 class xor_mlp(nn.Module):
     def __init__(self, hidden_dim):
@@ -37,15 +36,5 @@ if __name__ == "__main__":
     torch_net_a = train_model("Network A", 8).eval()
     torch_net_b = train_model("Network B", 16).eval()
 
-    onnx_net_a = torch.onnx.export(torch_net_a, (torch.randn(1, 2),), verbose=False).model_proto # type: ignore
-    onnx_net_b = torch.onnx.export(torch_net_b, (torch.randn(1, 2),), verbose=False).model_proto # type: ignore
-
-    z3_net_a = nneq.net(onnx_net_a)
-    z3_net_b = nneq.net(onnx_net_b)
-
-    print("")
-    nneq.strict_equivalence(z3_net_a, z3_net_b)
-    print("")
-    nneq.epsilon_equivalence(z3_net_a, z3_net_b, 0.1)
-    print("")
-    nneq.argmax_equivalence(z3_net_a, z3_net_b)
+    torch.onnx.export(torch_net_a, (torch.randn(1, 2),), "xor_a.onnx")
+    torch.onnx.export(torch_net_b, (torch.randn(1, 2),), "xor_b.onnx")
diff --git a/xor/xor_a.onnx b/xor/xor_a.onnx
new file mode 100644
index 0000000..9c13609
--- /dev/null
+++ b/xor/xor_a.onnx
diff --git a/xor/xor_a.onnx.data b/xor/xor_a.onnx.data
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/xor/xor_a.onnx.data
diff --git a/xor/xor_argmax.vnnlib b/xor/xor_argmax.vnnlib
new file mode 100644
index 0000000..3043d70
--- /dev/null
+++ b/xor/xor_argmax.vnnlib
@@ -0,0 +1,11 @@
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Discrete inputs: X must be 0 or 1
+(assert (or (= X_0 0) (= X_0 1)))
+(assert (or (= X_1 0) (= X_1 1)))
+
+; Violation of argmax equivalence (threshold 0.5)
+(assert (not (= (> Y_0 0.5) (> Y_1 0.5))))
diff --git a/xor/xor_b.onnx b/xor/xor_b.onnx
new file mode 100644
index 0000000..fb18840
--- /dev/null
+++ b/xor/xor_b.onnx
diff --git a/xor/xor_b.onnx.data b/xor/xor_b.onnx.data
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/xor/xor_b.onnx.data
diff --git a/xor/xor_epsilon.vnnlib b/xor/xor_epsilon.vnnlib
new file mode 100644
index 0000000..d4e9bb7
--- /dev/null
+++ b/xor/xor_epsilon.vnnlib
@@ -0,0 +1,12 @@
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Discrete inputs: X must be 0 or 1
+(assert (or (= X_0 0) (= X_0 1)))
+(assert (or (= X_1 0) (= X_1 1)))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (> (absolute (- Y_0 Y_1)) 0.1))
diff --git a/xor/xor_strict.vnnlib b/xor/xor_strict.vnnlib
new file mode 100644
index 0000000..fcf364e
--- /dev/null
+++ b/xor/xor_strict.vnnlib
@@ -0,0 +1,11 @@
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Discrete inputs: X must be 0 or 1
+(assert (or (= X_0 0) (= X_0 1)))
+(assert (or (= X_1 0) (= X_1 1)))
+
+; Violation of strict equivalence: outputs are different
+(assert (not (= Y_0 Y_1)))