aboutsummaryrefslogtreecommitdiff
path: root/examples/tll/tll_argmax.vnnlib
diff options
context:
space:
mode:
Diffstat (limited to 'examples/tll/tll_argmax.vnnlib')
-rw-r--r--examples/tll/tll_argmax.vnnlib16
1 files changed, 0 insertions, 16 deletions
diff --git a/examples/tll/tll_argmax.vnnlib b/examples/tll/tll_argmax.vnnlib
deleted file mode 100644
index c084e52..0000000
--- a/examples/tll/tll_argmax.vnnlib
+++ /dev/null
@@ -1,16 +0,0 @@
-; Argmax Equivalence for TLL
-
-; 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 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 (and (> Y_0 0.5) (< Y_1 0.5)))