From c204e725f6a78ae708591dc502ea3f404d20f156 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 27 Oct 2023 16:41:43 +0200
Subject: [PATCH] [marabou] Rework negation of a formula, but use only
non-strict inequality symbols.
---
config/drivers/marabou.drv | 12 ++++++------
src/printers/marabou.ml | 12 ++++++++----
2 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index dafffbd..1f29308 100644
--- a/config/drivers/marabou.drv
+++ b/config/drivers/marabou.drv
@@ -117,9 +117,9 @@ theory real.Real
meta "invalid trigger" predicate (>)
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 prop MulComm.Comm
remove prop MulAssoc.Assoc
@@ -167,9 +167,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"
end
theory real.RealInfix
@@ -185,9 +185,9 @@ theory real.RealInfix
meta "invalid trigger" predicate (>.)
syntax predicate (<=.) "(%1 <= %2)"
- syntax predicate (<.) "(%1 < %2)"
+ syntax predicate (<.) "(%1 <= %2)"
syntax predicate (>=.) "(%1 >= %2)"
- syntax predicate (>.) "(%1 > %2)"
+ syntax predicate (>.) "(%1 >= %2)"
end
theory Bool
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 5b888e2..fe887fb 100644
--- a/src/printers/marabou.ml
+++ b/src/printers/marabou.ml
@@ -128,20 +128,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