From b49a0e723d331c8ad8f96ff2acb85ff56773f771 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 10 Dec 2021 11:52:41 +0100
Subject: [PATCH] [Marabou] Negate the goal
Disjunction handling in verification is not needed
---
lib/onnx/dune | 2 +-
src/printers/marabou.ml | 36 +++++++++++++++++++++++++++++++++++-
src/verification.ml | 2 +-
3 files changed, 37 insertions(+), 3 deletions(-)
diff --git a/lib/onnx/dune b/lib/onnx/dune
index 65ba5412..c8fcadaa 100644
--- a/lib/onnx/dune
+++ b/lib/onnx/dune
@@ -1,7 +1,7 @@
(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)
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 28a6c84d..4c23beca 100644
--- a/src/printers/marabou.ml
+++ b/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;
}
diff --git a/src/verification.ml b/src/verification.ml
index b38e5c7f..c7507c5b 100644
--- a/src/verification.ml
+++ b/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
--
GitLab