[PyRAT] Avoid task split and use pyrat full capability to handle logical operators.

src/printers/pyrat.ml

@@ -24,9 +24,10 @@ let number_format =
     Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
   }
 
-let rec print_term info fmt t =
+let rec print_base_term info fmt t =
   let open Why3 in
   match t.Term.t_node with
+  | Tbinop ((Tand | Tor), _, _) -> assert false
   | Tbinop ((Timplies | Tiff), _, _)
   | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
   | Teps _ ->
@@ -34,17 +35,13 @@ let rec print_term info fmt t =
   | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
   | 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
+    | Some s -> Printer.syntax_arguments s (print_base_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)"))
-  | Tbinop (Tand, _, _) ->
-    Printer.unsupportedTerm t "Unexpected conjunction not at top-level"
-  | Tbinop (Tor, t1, t2) ->
-    Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
 
-let rec print_top_level_term info fmt t =
+let rec print_term ?(nested = false) info fmt t =
   let open Why3 in
   (* Don't print things we don't know. *)
   let t_is_known =
@@ -55,15 +52,22 @@ let rec print_top_level_term info fmt t =
   in
   match t.Term.t_node with
   | Tquant _ -> ()
-  | Tbinop (Tand, t1, t2) ->
+  | Tbinop (((Tand | Tor) as lop), t1, t2) ->
     if t_is_known t1 && t_is_known t2
     then
-      Fmt.pf fmt "%a%a"
-        (print_top_level_term info)
-        t1
-        (print_top_level_term info)
-        t2
-  | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
+      let nested = true in
+      let psx, lop, pdx =
+        match lop with
+        | Tand -> ("", "and", "")
+        | Tor -> ("(", "or", ")")
+        | _ -> assert false
+      in
+      Fmt.pf fmt "%s%a %s %a%s" psx (print_term ~nested info) t1 lop
+        (print_term ~nested info) t2 pdx
+  | _ ->
+    if t_is_known t
+    then
+      Fmt.pf fmt "%a%(%)" (print_base_term info) t (if nested then "" else "@.")
 
 let print_decl info fmt d =
   let open Why3 in
@@ -74,8 +78,8 @@ let print_decl info fmt d =
   | Dlogic _ -> ()
   | 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.Paxiom, _, f) -> print_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) -> print_term info fmt f
 
 let rec print_tdecl info fmt task =
   let open Why3 in

src/verification.ml

@@ -42,7 +42,9 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
     (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
-    Trans.apply Split_goal.split_goal_full task_prepared
+    if String.equal prover.prover.prover_name "Marabou"
+    then Trans.apply Split_goal.split_goal_full task_prepared
+    else [ task_prepared ]
   in
   let command = Whyconf.get_complete_command ~with_steps:false prover in
   let nn_file =