[printer] Simplify the Marabou printer to handle only non-strict relational operators.

src/printers/marabou.ml

@@ -55,7 +55,7 @@ let rec print_term info fmt t =
   | Tbinop ((Timplies | Tiff | Tor), _, _)
   | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
   | Teps _ ->
-    Printer.unsupportedTerm t "Not supported by Marabou"
+    Printer.unsupportedTerm t "Marabou: not a base term"
   | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
   | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
   | Tapp (ls, [ { t_node = Tapp (ls1, []); _ }; { t_node = Tapp (ls2, []); _ } ])
@@ -81,24 +81,19 @@ let rec print_term info fmt t =
       else if Term.ls_equal ls info.ls_rel_float.ge
               || Term.ls_equal ls info.ls_rel_real.ge
       then Fmt.pf fmt "+%s -%s >= 0" s1 s2
-      else if Term.ls_equal ls info.ls_rel_float.lt
-              || 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.gt
-              || Term.ls_equal ls info.ls_rel_real.gt
-      then Fmt.pf fmt "+%s -%s > 0" s1 s2
-      else Printer.unsupportedTerm t "Unknown relational operator"
-    | _ -> Printer.unsupportedTerm t "Unknown variable(s)")
+      else Printer.unsupportedTerm t "Marabou: unknown relational operator"
+    | _ -> Printer.unsupportedTerm t "Marabou: unknown variable(s)")
   | Tapp (ls, l) -> (
     match Printer.query_syntax info.info_syn ls.ls_name with
     | Some s -> Printer.syntax_arguments s (print_term info) fmt l
     | None -> (
       match (Term.Hls.find_opt info.variables ls, l) with
       | Some s, [] -> Fmt.string fmt s
-      | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
+      | _ -> Printer.unsupportedTerm t "Marabou: unknown variable(s)"))
 
 let rec print_top_level_term info fmt t =
-  (* Don't print things we don't know. *)
+  (* We do not print unknown symbols: returns false if not a known syntax or
+     variable. *)
   let t_is_known =
     Term.t_s_all
       (fun _ -> true)
@@ -118,9 +113,9 @@ let rec print_top_level_term info fmt t =
   | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
 
 let rec negate_term info t =
+  (* Assumption: conjunctions have been split beforehand, hence cannot appear at
+     this stage. *)
   match t.Term.t_node with
-  | Tquant _ -> Printer.unsupportedTerm t "Quantification"
-  | Tbinop (Tand, _, _) -> Printer.unsupportedTerm t "Conjunction"
   | Tbinop (Tor, t1, t2) ->
     Term.t_and (negate_term info t1) (negate_term info t2)
   | Tapp (ls, [ t1; t2 ]) ->
@@ -128,31 +123,27 @@ let rec negate_term info t =
     (* Negate float relational symbols. *)
     let ls_neg =
       if Term.ls_equal ls info.ls_rel_float.le
-      then info.ls_rel_float.gt
-      else if Term.ls_equal ls info.ls_rel_float.ge
-      then info.ls_rel_float.lt
-      else if Term.ls_equal ls info.ls_rel_float.lt
+         || 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.gt
+      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.le
       else ls
     in
     (* Negate real relational symbols. *)
     let ls_neg =
       if Term.ls_equal ls info.ls_rel_real.le
-      then info.ls_rel_real.gt
-      else if Term.ls_equal ls info.ls_rel_real.ge
-      then info.ls_rel_real.lt
-      else if Term.ls_equal ls info.ls_rel_real.lt
+         || 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.gt
+      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.le
       else ls_neg
     in
     if Term.ls_equal ls_neg ls
-    then Printer.unsupportedTerm t "Cannot negate such term"
+    then Printer.unsupportedTerm t "Marabou: cannot negate term"
     else Term.ps_app ls_neg tt
-  | _ -> Printer.unsupportedTerm t "Cannot negate such term"
+  | _ -> Printer.unsupportedTerm t "Marabou: cannot negate term"
 
 let print_decl info fmt d =
   match d.Decl.d_node with
@@ -209,5 +200,5 @@ let print_task args ?old:_ fmt task =
   print_tdecl info fmt task
 
 let init () =
-  Printer.register_printer ~desc:"Printer for the Marabou prover." "marabou"
+  Printer.register_printer ~desc:"Printer@ for@ the@ Marabou@ prover." "marabou"
     print_task