From db54e31384f72cb62a4e1177b8b97edabbb45d7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 27 Sep 2022 11:10:34 +0200
Subject: [PATCH] [Marabou] Also split premises to create different tasks.
The axiom a \/ b gives two different tasks.
---
src/transformations/split.ml | 41 +++++++++++++++++++
.../{split_disjunction.ml => split.mli} | 11 ++---
src/verification.ml | 2 +-
tests/marabou.t | 6 +++
4 files changed, 54 insertions(+), 6 deletions(-)
create mode 100644 src/transformations/split.ml
rename src/transformations/{split_disjunction.ml => split.mli} (86%)
diff --git a/src/transformations/split.ml b/src/transformations/split.ml
new file mode 100644
index 00000000..84dd760f
--- /dev/null
+++ b/src/transformations/split.ml
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* 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)
diff --git a/src/transformations/split_disjunction.ml b/src/transformations/split.mli
similarity index 86%
rename from src/transformations/split_disjunction.ml
rename to src/transformations/split.mli
index 7295542d..6717d02e 100644
--- a/src/transformations/split_disjunction.ml
+++ b/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. *)
diff --git a/src/verification.ml b/src/verification.ml
index 7044769f..c37aeb02 100644
--- a/src/verification.ml
+++ b/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
diff --git a/tests/marabou.t b/tests/marabou.t
index 390d8ff2..79fb48a2 100644
--- a/tests/marabou.t
+++ b/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 ()
--
GitLab