Skip to content
Snippets Groups Projects
Commit 77baf78f authored by Michele Alberti's avatar Michele Alberti
Browse files

[printers] Support lt and gt as relational operators for Marabou.

parent bdbbde88
No related branches found
No related tags found
No related merge requests found
......@@ -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)")
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment