added LICENSE

4 files changed, 0 insertions, 83 deletions

diff --git a/xor/xor.py b/xor/xor.py
deleted file mode 100644
index ebc5477..0000000
--- a/xor/xor.py
+++ /dev/null
@@ -1,40 +0,0 @@
-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/xor/xor_argmax.vnnlib b/xor/xor_argmax.vnnlib
deleted file mode 100644
index d38bc31..0000000
--- a/xor/xor_argmax.vnnlib
+++ /dev/null
@@ -1,14 +0,0 @@
-; 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/xor/xor_epsilon.vnnlib b/xor/xor_epsilon.vnnlib
deleted file mode 100644
index 427243e..0000000
--- a/xor/xor_epsilon.vnnlib
+++ /dev/null
@@ -1,15 +0,0 @@
-; 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/xor/xor_strict.vnnlib b/xor/xor_strict.vnnlib
deleted file mode 100644
index bead476..0000000
--- a/xor/xor_strict.vnnlib
+++ /dev/null
@@ -1,14 +0,0 @@
-; 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)))