From 06b3af488e9d33836fb67d963eedfc6284925210 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 17 Feb 2022 12:30:15 +0100
Subject: [PATCH] [PyRAT] Split all tasks so that conjuctions must appear at
top-level only.
---
src/printers/pyrat.ml | 3 ++-
src/verification.ml | 6 ++----
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml
index 2cd238c1..d365b254 100644
--- a/src/printers/pyrat.ml
+++ b/src/printers/pyrat.ml
@@ -31,7 +31,6 @@ let rec print_term info fmt t =
| Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
| Teps _ ->
Printer.unsupportedTerm t "Not supported by PyRAT"
- | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
| Tconst c -> Constant.(print number_format unsupported_escape) fmt c
| Tapp (ls, l) -> (
match Printer.query_syntax info.info_syn ls.ls_name with
@@ -40,6 +39,8 @@ let rec print_term info fmt t =
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
diff --git a/src/verification.ml b/src/verification.ml
index 2a9bfbd8..b25aaa1d 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -40,11 +40,9 @@ let combine_prover_answers answers =
let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
let open Why3 in
let task_prepared = Driver.prepare_task driver task in
- (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
let tasks =
- if String.equal prover.prover.prover_name "Marabou"
- then Trans.apply Split_goal.split_goal_full task_prepared
- else [ task_prepared ]
+ (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
+ Trans.apply Split_goal.split_goal_full task_prepared
in
let command = Whyconf.get_complete_command ~with_steps:false prover in
let nn_file =
--
GitLab