[Marabou] Negate the goal

          Disjunction handling in verification is not needed

lib/onnx/dune

 (library
   (name onnx)
   (public_name onnx)
-  (libraries base stdio piqirun.pb ocaml-protoc-plugin)
+  (libraries base stdio ocaml-protoc-plugin)
   (synopsis "ONNX parser"))
 (rule
   (targets onnx_protoc.ml)

src/printers/marabou.ml

@@ -5,6 +5,10 @@
 (**************************************************************************)
 
 type info = {
+  le : Why3.Term.lsymbol;
+  ge : Why3.Term.lsymbol;
+  lt : Why3.Term.lsymbol;
+  gt : Why3.Term.lsymbol;
   info_syn : Why3.Printer.syntax_map;
   variables : string Why3.Term.Hls.t;
 }
@@ -61,6 +65,26 @@ let rec print_top_level_term info fmt t =
         t2
   | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
 
+let rec negate_term info t =
+  let open Why3 in
+  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 ]) ->
+    let tt = [ t1; t2 ] in
+    if Term.ls_equal ls info.le
+    then Term.ps_app info.gt tt
+    else if Term.ls_equal ls info.ge
+    then Term.ps_app info.lt tt
+    else if Term.ls_equal ls info.lt
+    then Term.ps_app info.ge tt
+    else if Term.ls_equal ls info.gt
+    then Term.ps_app info.le tt
+    else Printer.unsupportedTerm t "Can't negate that"
+  | _ -> Printer.unsupportedTerm t "Can't negate that"
+
 let print_decl info fmt d =
   let open Why3 in
   match d.Decl.d_node with
@@ -71,7 +95,8 @@ let print_decl info fmt d =
   | Dind _ -> ()
   | Dprop (Decl.Plemma, _, _) -> assert false
   | Dprop (Decl.Paxiom, _, f) -> print_top_level_term info fmt f
-  | Dprop (Decl.Pgoal, _, f) -> print_top_level_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) ->
+    print_top_level_term info fmt (negate_term info f)
 
 let rec print_tdecl info fmt task =
   let open Why3 in
@@ -96,8 +121,17 @@ let rec print_tdecl info fmt task =
 
 let print_task args ?old:_ fmt task =
   let open Why3 in
+  let th = Env.read_theory args.Printer.env [ "ieee_float" ] "Float64" in
+  let le = Theory.ns_find_ls th.th_export [ "le" ] in
+  let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
+  let ge = Theory.ns_find_ls th.th_export [ "ge" ] in
+  let gt = Theory.ns_find_ls th.th_export [ "gt" ] in
   let info =
     {
+      le;
+      lt;
+      ge;
+      gt;
       info_syn = Discriminate.get_syntax_map task;
       variables = Term.Hls.create 10;
     }

src/verification.ml

@@ -50,7 +50,7 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
     if String.equal prover.prover.prover_name "Marabou"
     then
       let conjs = Trans.apply Split_goal.split_goal_full task_prepared in
-      List.map ~f:(Trans.apply Split_disjunction.split_disjunction) conjs
+      List.map ~f:(fun c -> [ c ]) conjs
     else [ [ task_prepared ] ]
   in
   let command = Whyconf.get_complete_command ~with_steps:false prover in