From 8e937f27633ac77b3f9c5249c89036f90f5983c6 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 27 Oct 2023 16:20:53 +0200
Subject: [PATCH] [vnnlib] Rework negation of a formula, but use only
 non-strict inequality symbols.

---
 config/drivers/vnnlib.gen     |   8 +-
 src/printers/vnnlib.ml        |  12 +-
 tests/interpretation_acasxu.t | 216 +++++++++++++++++++++++++++++++++-
 3 files changed, 227 insertions(+), 9 deletions(-)

diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index 5a2ae27..fe1bd19 100644
--- a/config/drivers/vnnlib.gen
+++ b/config/drivers/vnnlib.gen
@@ -77,9 +77,9 @@ theory real.Real
   syntax function inv  "(/ 1.0 %1)"
 
   syntax predicate (<=) "(<= %1 %2)"
-  syntax predicate (<)  "(< %1 %2)"
+  syntax predicate (<)  "(<= %1 %2)"
   syntax predicate (>=) "(>= %1 %2)"
-  syntax predicate (>)  "(> %1 %2)"
+  syntax predicate (>)  "(>= %1 %2)"
 
   remove allprops
   meta "encoding:kept" type real
@@ -123,9 +123,9 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "(<= %1 %2)"
-  syntax predicate lt "(< %1 %2)"
+  syntax predicate lt "(<= %1 %2)"
   syntax predicate ge "(>= %1 %2)"
-  syntax predicate gt "(> %1 %2)"
+  syntax predicate gt "(>= %1 %2)"
 
   syntax predicate is_not_nan ""
   remove allprops
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index 2372b4d..90888b4 100644
--- a/src/printers/vnnlib.ml
+++ b/src/printers/vnnlib.ml
@@ -445,20 +445,24 @@ let rec negate_term info t =
     (* Negate float relational symbols. *)
     let ls_neg =
       if Term.ls_equal ls info.ls_rel_float.le
-         || Term.ls_equal ls info.ls_rel_float.lt
+      then info.ls_rel_float.gt
+      else if Term.ls_equal ls info.ls_rel_float.lt
       then info.ls_rel_float.ge
       else if Term.ls_equal ls info.ls_rel_float.ge
-              || Term.ls_equal ls info.ls_rel_float.gt
+      then info.ls_rel_float.lt
+      else if Term.ls_equal ls info.ls_rel_float.gt
       then info.ls_rel_float.le
       else ls
     in
     (* Negate real relational symbols. *)
     let ls_neg =
       if Term.ls_equal ls info.ls_rel_real.le
-         || Term.ls_equal ls info.ls_rel_real.lt
+      then info.ls_rel_real.gt
+      else if Term.ls_equal ls info.ls_rel_real.lt
       then info.ls_rel_real.ge
       else if Term.ls_equal ls info.ls_rel_real.ge
-              || Term.ls_equal ls info.ls_rel_real.gt
+      then info.ls_rel_real.lt
+      else if Term.ls_equal ls info.ls_rel_real.gt
       then info.ls_rel_real.le
       else ls_neg
     in
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 2e04d6c..11080ff 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -4,7 +4,7 @@ Test interpret on acasxu
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ cat > file.mlw <<EOF
   > theory T
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -92,6 +92,8 @@ Test interpret on acasxu
   >       not (advises nn i clear_of_conflict)
   > end
   > EOF
+
+  $ caisar verify --prover PyRAT --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:
   -0.328421367053318091766556108268559910356998443603515625 <= x0
   x0 <= 0.67985927880386987087746319957659579813480377197265625
@@ -130,3 +132,215 @@ Test interpret on acasxu
   
   Goal P1: Unknown ()
   Goal P3: Unknown ()
+
+  $ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; H
+  (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+  
+  ;; H
+  (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+  
+  ;; H
+  (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_3 -0.5))
+  
+  ;; H
+  (assert (<= X_3 0.5))
+  
+  ;; H
+  (assert (>= X_4 -0.5))
+  
+  ;; H
+  (assert (<= X_4 0.5))
+  
+  ;; H
+  (assert (>= X_0 0.60000151009774149724051994780893437564373016357421875))
+  
+  ;; H
+  (assert (>= X_3 0.450000000000000011102230246251565404236316680908203125))
+  
+  ;; H
+  (assert (<= X_4 -0.450000000000000011102230246251565404236316680908203125))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal P1
+  (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; H
+  (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+  
+  ;; H
+  (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+  
+  ;; H
+  (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_3 -0.5))
+  
+  ;; H
+  (assert (<= X_3 0.5))
+  
+  ;; H
+  (assert (>= X_4 -0.5))
+  
+  ;; H
+  (assert (<= X_4 0.5))
+  
+  ;; H
+  (assert (>= X_0 -0.303529646039727207806890874053351581096649169921875))
+  
+  ;; H
+  (assert (<= X_0 -0.298551301837009008810497334707179106771945953369140625))
+  
+  ;; H
+  (assert (>= X_1 -0.0095492965855130916563719978285007528029382228851318359375))
+  
+  ;; H
+  (assert (<= X_1 0.0095492965855130916563719978285007528029382228851318359375))
+  
+  ;; H
+  (assert (>= X_2 0.493380323584843072382000173092819750308990478515625))
+  
+  ;; H
+  (assert (>= X_3 0.299999999999999988897769753748434595763683319091796875))
+  
+  ;; H
+  (assert (>= X_4 0.299999999999999988897769753748434595763683319091796875))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal P3
+  (assert (<= Y_0 Y_1))
+  (assert (<= Y_0 Y_2))
+  (assert (<= Y_0 Y_3))
+  (assert (<= Y_0 Y_4))
+  
+  Goal P1: Unknown ()
+  Goal P3: Unknown ()
+
+  $ caisar verify --prover Marabou --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= -0.328421367053318091766556108268559910356998443603515625
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  x1 >= -0.499999999999967081887319864108576439321041107177734375
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  x2 >= -0.499999999999967081887319864108576439321041107177734375
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  x3 >= -0.5
+  x3 <= 0.5
+  x4 >= -0.5
+  x4 <= 0.5
+  x0 >= 0.60000151009774149724051994780893437564373016357421875
+  x3 >= 0.450000000000000011102230246251565404236316680908203125
+  x4 <= -0.450000000000000011102230246251565404236316680908203125
+  y0 >= 3.991125645861615112153231166303157806396484375
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= -0.328421367053318091766556108268559910356998443603515625
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  x1 >= -0.499999999999967081887319864108576439321041107177734375
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  x2 >= -0.499999999999967081887319864108576439321041107177734375
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  x3 >= -0.5
+  x3 <= 0.5
+  x4 >= -0.5
+  x4 <= 0.5
+  x0 >= -0.303529646039727207806890874053351581096649169921875
+  x0 <= -0.298551301837009008810497334707179106771945953369140625
+  x1 >= -0.0095492965855130916563719978285007528029382228851318359375
+  x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+  x2 >= 0.493380323584843072382000173092819750308990478515625
+  x3 >= 0.299999999999999988897769753748434595763683319091796875
+  x4 >= 0.299999999999999988897769753748434595763683319091796875
+  +y0 -y1 <= 0
+  +y0 -y2 <= 0
+  +y0 -y3 <= 0
+  +y0 -y4 <= 0
+  
+  Goal P1: Unknown ()
+  Goal P3: Unknown ()
-- 
GitLab