From 77baf78f28f8e1c3a1cedc7cd93ca421ceafa64c Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 12 May 2023 15:31:44 +0200
Subject: [PATCH] [printers] Support lt and gt as relational operators for
Marabou.
---
src/printers/marabou.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 817c094..823782a 100644
--- a/src/printers/marabou.ml
+++ b/src/printers/marabou.ml
@@ -76,10 +76,14 @@ let rec print_term info fmt t =
with
| Some s1, Some s2 ->
if Term.ls_equal ls info.ls_rel_float.le
+ || Term.ls_equal ls info.ls_rel_float.lt
|| Term.ls_equal ls info.ls_rel_real.le
+ || Term.ls_equal ls info.ls_rel_real.lt
then Fmt.pf fmt "+%s -%s <= 0" s1 s2
else if Term.ls_equal ls info.ls_rel_float.ge
+ || Term.ls_equal ls info.ls_rel_float.gt
|| Term.ls_equal ls info.ls_rel_real.ge
+ || Term.ls_equal ls info.ls_rel_real.gt
then Fmt.pf fmt "+%s -%s >= 0" s1 s2
else Printer.unsupportedTerm t "Marabou: unknown relational operator"
| _ -> Printer.unsupportedTerm t "Marabou: unknown variable(s)")
--
GitLab