From 81d4d604aa43660b732b3538734a52d509d7c5df Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Tue, 31 Mar 2026 16:43:47 +0200
Subject: refactored examples

---
 .../double_integrator_argmax.vnnlib                |  27 +++++++++++++++++++++
 .../double_integrator_epsilon.vnnlib               |  22 +++++++++++++++++
 .../double_integrator_finetune_inv.onnx            | Bin 0 -> 12584 bytes
 .../double_integrator_strict.vnnlib                |  21 ++++++++++++++++
 4 files changed, 70 insertions(+)
 create mode 100644 examples/double_integrator/double_integrator_argmax.vnnlib
 create mode 100644 examples/double_integrator/double_integrator_epsilon.vnnlib
 create mode 100644 examples/double_integrator/double_integrator_finetune_inv.onnx
 create mode 100644 examples/double_integrator/double_integrator_strict.vnnlib

(limited to 'examples/double_integrator')

diff --git a/examples/double_integrator/double_integrator_argmax.vnnlib b/examples/double_integrator/double_integrator_argmax.vnnlib
new file mode 100644
index 0000000..f0a72e9
--- /dev/null
+++ b/examples/double_integrator/double_integrator_argmax.vnnlib
@@ -0,0 +1,27 @@
+; Argmax Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+		(> Y_3 Y_2)
+  )
+  (and 
+    (> Y_1 Y_0)
+		(> Y_2 Y_3)
+  )
+))
diff --git a/examples/double_integrator/double_integrator_epsilon.vnnlib b/examples/double_integrator/double_integrator_epsilon.vnnlib
new file mode 100644
index 0000000..3af9079
--- /dev/null
+++ b/examples/double_integrator/double_integrator_epsilon.vnnlib
@@ -0,0 +1,22 @@
+; Strict Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_2)) 0.1)
+	(> (absolute (- Y_1 Y_3)) 0.1)
+))
diff --git a/examples/double_integrator/double_integrator_finetune_inv.onnx b/examples/double_integrator/double_integrator_finetune_inv.onnx
new file mode 100644
index 0000000..8a7797b
Binary files /dev/null and b/examples/double_integrator/double_integrator_finetune_inv.onnx differ
diff --git a/examples/double_integrator/double_integrator_strict.vnnlib b/examples/double_integrator/double_integrator_strict.vnnlib
new file mode 100644
index 0000000..d3c8c3e
--- /dev/null
+++ b/examples/double_integrator/double_integrator_strict.vnnlib
@@ -0,0 +1,21 @@
+; Strict Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_2))
+	(not (= Y_1 Y_3))
+))
-- 
cgit v1.2.3