From b9fd37430c014e4059f744957c4b135e2ca29791 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 14 Nov 2023 13:59:22 +0100
Subject: [PATCH] [drivers] Add comment to justify strict inequalities treated
 as non-strict ones.

---
 config/drivers/marabou.drv | 18 +++++++++++++++---
 config/drivers/vnnlib.gen  | 12 ++++++++++--
 2 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index 1f29308..2b23a90 100644
--- a/config/drivers/marabou.drv
+++ b/config/drivers/marabou.drv
@@ -117,8 +117,12 @@ theory real.Real
   meta "invalid trigger" predicate (>)
 
   syntax predicate (<=) "%1 <= %2"
-  syntax predicate (<)  "%1 <= %2"
   syntax predicate (>=) "%1 >= %2"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<)  "%1 <= %2"
   syntax predicate (>)  "%1 >= %2"
 
   remove prop MulComm.Comm
@@ -167,8 +171,12 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "%1 <= %2"
-  syntax predicate lt "%1 <= %2"
   syntax predicate ge "%1 >= %2"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate lt "%1 <= %2"
   syntax predicate gt "%1 >= %2"
 end
 
@@ -185,8 +193,12 @@ theory real.RealInfix
   meta "invalid trigger" predicate (>.)
 
   syntax predicate (<=.) "(%1 <= %2)"
-  syntax predicate (<.)  "(%1 <= %2)"
   syntax predicate (>=.) "(%1 >= %2)"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<.)  "(%1 <= %2)"
   syntax predicate (>.)  "(%1 >= %2)"
 end
 
diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index fe1bd19..59c1c5d 100644
--- a/config/drivers/vnnlib.gen
+++ b/config/drivers/vnnlib.gen
@@ -77,8 +77,12 @@ theory real.Real
   syntax function inv  "(/ 1.0 %1)"
 
   syntax predicate (<=) "(<= %1 %2)"
-  syntax predicate (<)  "(<= %1 %2)"
   syntax predicate (>=) "(>= %1 %2)"
+
+  (* VNN-LIB supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<)  "(<= %1 %2)"
   syntax predicate (>)  "(>= %1 %2)"
 
   remove allprops
@@ -123,8 +127,12 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "(<= %1 %2)"
-  syntax predicate lt "(<= %1 %2)"
   syntax predicate ge "(>= %1 %2)"
+
+  (* VNN-LIB supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate lt "(<= %1 %2)"
   syntax predicate gt "(>= %1 %2)"
 
   syntax predicate is_not_nan ""
-- 
GitLab