[drivers] Add comment to justify strict inequalities treated as non-strict ones.

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
 

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 ""