[interpretation] Bounded quantification allows to consider part of the implication.

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

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
 

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 =

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)