From 31c025cdb1e830aa95418d9e80cb85cf3bbcecd1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 5 Mar 2024 17:01:15 +0100
Subject: [PATCH] [interpretation] Bounded quantification allows to consider
part of the implication.
---
src/interpretation/interpreter.ml | 23 +++++++++++--
.../interpreter_reduction_engine.ml | 16 ++++-----
.../interpreter_reduction_engine.mli | 1 +
tests/acasxu.t | 34 ++++++++++++++++++-
4 files changed, 61 insertions(+), 13 deletions(-)
diff --git a/src/interpretation/interpreter.ml b/src/interpretation/interpreter.ml
index 1e3ade9..99a50d9 100644
--- a/src/interpretation/interpreter.ml
+++ b/src/interpretation/interpreter.ml
@@ -117,12 +117,29 @@ let rec bounded_quant engine vs ~cond : IRE.bounded_quant_result option =
let substitutions =
[ ITypes.term_of_op ~args engine op (Some vs.vs_ty) ]
in
- Some { new_quant; substitutions }
+ Some
+ { new_quant; substitutions; remaining_implication = Why3.Term.t_true }
| Tapp ({ ls_name = { id_string = "has_length"; _ }; _ }, _) -> None
| Tbinop (Tand, a, b) -> (
match bounded_quant engine vs ~cond:a with
- | None -> bounded_quant engine vs ~cond:b
- | r -> r)
+ | None -> (
+ match bounded_quant engine vs ~cond:b with
+ | None -> None
+ | Some { new_quant; substitutions; remaining_implication } ->
+ Some
+ {
+ new_quant;
+ substitutions;
+ remaining_implication =
+ Why3.Term.t_and_simp a remaining_implication;
+ })
+ | Some { new_quant; substitutions; remaining_implication } ->
+ Some
+ {
+ new_quant;
+ substitutions;
+ remaining_implication = Why3.Term.t_and_simp remaining_implication b;
+ })
| _ ->
Logging.user_error ?loc:vs.vs_name.id_loc (fun m ->
m
diff --git a/src/interpretation/interpreter_reduction_engine.ml b/src/interpretation/interpreter_reduction_engine.ml
index 6b90428..c34d89e 100644
--- a/src/interpretation/interpreter_reduction_engine.ml
+++ b/src/interpretation/interpreter_reduction_engine.ml
@@ -40,6 +40,7 @@ type params = {
type bounded_quant_result = {
new_quant : vsymbol list;
substitutions : term list;
+ remaining_implication : term;
}
type builtin_value =
@@ -788,20 +789,17 @@ let reduce_bounded_quant engine ls_lt limit t sigma st rem =
in
{ value_stack = st; cont_stack = loop rem b }
| ( Term cond :: st,
- (Kbinop Timplies, _)
- :: (Kquant ((Tforall as quant), [ vs ], _), t_orig)
- :: rem ) -> (
+ (Kbinop Timplies, _) :: (Kquant (Tforall, [ vs ], _), t_orig) :: rem )
+ -> (
match engine.bounded_quant engine vs ~cond with
| None -> raise Exit
| Some res -> (
- let t_empty, binop =
- match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
- in
let rem =
match res.new_quant with
| [] -> rem
- | _ -> (Kquant (quant, res.new_quant, []), t_orig) :: rem
+ | _ -> (Kquant (Tforall, res.new_quant, []), t_orig) :: rem
in
+ let t = Term.t_implies_simp res.remaining_implication t in
let rec loop rem = function
| [] -> rem
| t_i :: l ->
@@ -810,13 +808,13 @@ let reduce_bounded_quant engine ls_lt limit t sigma st rem =
| [] -> rem
| _ ->
(* conjunction *)
- (Kbinop binop, t_true) :: rem
+ (Kbinop Tand, t_true) :: rem
in
let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
loop rem l
in
match res.substitutions with
- | [] -> { value_stack = Term t_empty :: st; cont_stack = rem }
+ | [] -> { value_stack = Term t_true :: st; cont_stack = rem }
| _ -> { value_stack = st; cont_stack = loop rem res.substitutions }))
| _ -> raise Exit
diff --git a/src/interpretation/interpreter_reduction_engine.mli b/src/interpretation/interpreter_reduction_engine.mli
index 644f50e..9e69e6d 100644
--- a/src/interpretation/interpreter_reduction_engine.mli
+++ b/src/interpretation/interpreter_reduction_engine.mli
@@ -105,6 +105,7 @@ type 'a built_in_theories =
type bounded_quant_result = {
new_quant : Term.vsymbol list;
substitutions : Term.term list;
+ remaining_implication : Term.term;
}
type 'a bounded_quant =
diff --git a/tests/acasxu.t b/tests/acasxu.t
index 85dce51..3ac4e06 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -125,7 +125,39 @@ Test verify on acasxu
> end
> EOF
- $ caisar verify --prover PyRAT --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT --ltag=ProverSpec --ltag=InterpretGoal file.mlw 2>&1 | ./filter_tmpdir.sh
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'run'vc':
+ forall x:t, x1:t, x2:t, x3:t, x4:t.
+ ((le (0.0:t) x /\ le x (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x1 /\
+ le x1 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x2 /\
+ le x2 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) x3 /\ le x3 (1200.0:t)) /\ le (0.0:t) x4 /\ le x4 (1200.0:t)) /\
+ le (55947.6909999999988940544426441192626953125:t) x /\
+ le (1145.0:t) x3 /\ le x4 (60.0:t) ->
+ le
+ (add RNE
+ (mul RNE
+ (nn_nnet
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0] (373.9499200000000200816430151462554931640625:t))
+ (7.51888402010059753166615337249822914600372314453125:t))
+ (1500.0:t)
+ nn_nnet,
+ (Interpreter_types.Model
+ (Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename = "./TestNetwork.nnet";
+ nn_format = Language.NNet }))
+ vector,
+ 5
[ERROR]{TransformationsUtils} Not an input variable: div RNE
(sub RNE x (19791.0:t))
(60261.0:t)
--
GitLab