diff --git a/src/interpretation/interpreter.ml b/src/interpretation/interpreter.ml
index 1e3ade98a013cef789b848259e7097c16fd1caf3..99a50d9f9fab1773cbffa72f3c1a35063f5d03de 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 6b9042886a8e502377b46d64c47f4b03a7b45a36..c34d89e67697c768afcde0dc44632866d31ff049 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 644f50e51309bc37d19290f32297827e317d2287..9e69e6d8a2feec27d64e638899c403c082fa0aab 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 85dce51da413d84d8e1f546d5c125947dd4ea8df..3ac4e06e93438f4b30b6d6fb0927907da32aceec 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)