4 files changed, 83 insertions, 0 deletions
diff --git a/examples/xor/xor.py b/examples/xor/xor.py
new file mode 100644
index 0000000..ebc5477
--- /dev/null
+++ b/examples/xor/xor.py
@@ -0,0 +1,40 @@
+import torch
+import torch.nn as nn
+import torch.onnx
+
+class xor_mlp(nn.Module):
+    def __init__(self, hidden_dim):
+        super().__init__()
+        self.layers = nn.Sequential(
+            nn.Linear(2, hidden_dim),
+            nn.ReLU(),
+            nn.Linear(hidden_dim, 1)
+        )
+    def forward(self, x):
+        return self.layers(x)
+
+def train_model(name: str, dim):
+    X = torch.tensor([[0,0], [0,1], [1,0], [1,1]], dtype=torch.float32)
+    Y = torch.tensor([[0], [1], [1], [0]], dtype=torch.float32)
+
+    net = xor_mlp(hidden_dim=dim)
+    loss_fn = nn.MSELoss()
+    optimizer = torch.optim.Adam(net.parameters(), lr=0.1)
+
+    print(f"Training {name}...")
+    for epoch in range(1000):
+        optimizer.zero_grad()
+        out = net(X)
+        loss = loss_fn(out, Y)
+        loss.backward()
+        optimizer.step()
+        if (epoch+1) % 100 == 0:
+            print(f"  Epoch {epoch+1}, Loss: {loss.item():.4f}")
+    return net
+
+if __name__ == "__main__":
+    torch_net_a = train_model("Network A", 8).eval()
+    torch_net_b = train_model("Network B", 16).eval()
+
+    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/examples/xor/xor_argmax.vnnlib b/examples/xor/xor_argmax.vnnlib
new file mode 100644
index 0000000..d38bc31
--- /dev/null
+++ b/examples/xor/xor_argmax.vnnlib
@@ -0,0 +1,14 @@
+; Argmax Equivalence for XOR
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded 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
+(assert (not (= (> Y_0 0.5) (> Y_1 0.5))))
diff --git a/examples/xor/xor_epsilon.vnnlib b/examples/xor/xor_epsilon.vnnlib
new file mode 100644
index 0000000..427243e
--- /dev/null
+++ b/examples/xor/xor_epsilon.vnnlib
@@ -0,0 +1,15 @@
+; Epsilon Equivalence for XOR
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded 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/examples/xor/xor_strict.vnnlib b/examples/xor/xor_strict.vnnlib
new file mode 100644
index 0000000..bead476
--- /dev/null
+++ b/examples/xor/xor_strict.vnnlib
@@ -0,0 +1,14 @@
+; Strict Equivalence for XOR
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded 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)))