[Marabou] Also split premises to create different tasks.

The axiom a \/ b gives two different tasks.

src/transformations/split.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+open Why3
+
+let split_generic filter_prop_kind =
+  Trans.decl_l
+    (fun d ->
+      match d.d_node with
+      | Dprop (k, pr, t) when filter_prop_kind k ->
+        let l =
+          match k with
+          | Paxiom | Plemma -> Split_goal.split_neg_full t
+          | Pgoal -> Split_goal.split_pos_full t
+        in
+        List.map l ~f:(fun t -> [ Decl.create_prop_decl k pr t ])
+      | _ -> [ [ d ] ])
+    None
+
+let split_premises = split_generic (function Paxiom -> true | _ -> false)
+let split_all = split_generic (fun _ -> true)

src/transformations/split_disjunction.ml → src/transformations/split.mli

@@ -20,10 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Base
 open Why3
 
-let split_disjunction =
-  Trans.goal_l (fun pr t ->
-    let l = Split_goal.split_neg_full t in
-    List.map l ~f:(fun t -> [ Decl.create_prop_decl Pgoal pr t ]))
+val split_premises : Task.task Trans.tlist
+(** Split disjunctions appearing in axioms into different tasks. *)
+
+val split_all : Task.task Trans.tlist
+(** Split disjunctions appearing in premises, and conjunctions appearing in the
+    goal, into different tasks. *)

src/verification.ml

@@ -168,7 +168,7 @@ let answer_generic limit config prover config_prover driver task =
   let tasks =
     (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
     match prover with
-    | Prover.Marabou -> Trans.apply Split_goal.split_goal_full task_prepared
+    | Prover.Marabou -> Trans.apply Split.split_all task_prepared
     | _ -> [ task_prepared ]
   in
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in

tests/marabou.t

@@ -37,8 +37,14 @@ Test verify
   >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
   >      let (y1,y2,_,_,_) = net_apply x1 x2 x3 x4 x5 in
   >      y2 .< y1 \/ y1 .< y2
+  > 
+  >   goal J: forall x1 x2 x3 x4 x5.
+  >        ((0.0:t) .< x1 .< (0.5:t) \/ (0.75:t) .< x1 .< (1.0:t)) /\ (0.5:t) .< x2 .< (1.0:t) ->
+  >      let (y1,y2,_,_,_) = net_apply x1 x2 x3 x4 x5 in
+  >      y2 .< y1 \/ y1 .< y2
   > end
   > EOF
   [caisar] Goal G: Unknown ()
   [caisar] Goal H: Unknown ()
   [caisar] Goal I: Unknown ()
+  [caisar] Goal J: Unknown ()