From 3e8616d247f4e18ceef17bd304ac89d12a77e526 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 27 Oct 2023 17:02:33 +0200
Subject: [PATCH] [pyrat] Rework negation of formula w/o touching the driver.
No need to modify the driver because PyRAT handles stict inequality symbols.
---
src/printers/pyrat.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml
index d80dc5f..51573a7 100644
--- a/src/printers/pyrat.ml
+++ b/src/printers/pyrat.ml
@@ -96,20 +96,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
--
GitLab