Q817-011 proof - use cvc4 for floats

Driver updates and refactoring. Add new floats drivers file.

Also add Clément's old transformation (intended for colibri) for
elimination of ident/types/etc.

Change-Id: I161612592904ed3700b414c01ccab7944654d4d9
(cherry picked from commit a82204236d1e73207dbd71b95236757d0eeacfa2)

Conflicts:
	drivers/cvc4_14.drv
	drivers/cvc4_15.drv
	drivers/cvc4_gnatprove.drv
	drivers/z3_gnatprove.drv
	drivers/z3_gnatprove_ce.drv

Makefile.in

@@ -189,6 +189,9 @@ LIB_PARSER = ptree glob parser typing lexer
 LIB_TRANSFORM = simplify_formula inlining split_goal \
 		args_wrapper detect_polymorphism reduction_engine compute \
 		eliminate_definition eliminate_algebraic \
+		abstract_quantifiers eliminate_unknown_types \
+		eliminate_unknown_lsymbols \
+		eliminate_symbol \
 		eliminate_inductive eliminate_let eliminate_if \
 		libencoding discriminate encoding encoding_select \
 		encoding_guards_full encoding_tags_full \

drivers/cvc4_14.drv

 (** Why3 driver for CVC4 1.4 *)
 
+prelude ";; produced by cvc4_14.drv ;;"
 prelude "(set-logic AUFBVDTNIRA)"
 (*
     A    : Array
     UF   : Uninterpreted Function
     BV   : BitVectors
     DT   : Datatypes
-    NIRA : NonLinear Integer Real Arithmetic
-*)
-(* prelude "(set-logic ALL_SUPPORTED)"
-   does not seem to include DT
+    NIRA : NonLinear Integer+Real Arithmetic
 *)
 
 import "smt-libv2.drv"

drivers/cvc4_15.drv

 (** Why3 driver for CVC4 >= 1.5 *)
 
+prelude ";; produced by cvc4_15.drv ;;"
 prelude "(set-logic AUFBVDTNIRA)"
 (*
     A    : Array
     UF   : Uninterpreted Function
     BV   : BitVectors
     DT   : Datatypes
-    NIRA : NonLinear Integer Reals Arithmetic
-*)
-(* prelude "(set-logic ALL_SUPPORTED)"
-   does not seem to include DT
+    NIRA : NonLinear Integer+Real Arithmetic
 *)
 
 (* Counterexamples: set model parser *)

drivers/cvc4_16.drv

+(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
+
+prelude ";; produced by cvc4_16.drv ;;"
+prelude "(set-info :smt-lib-version 2.5)"
+prelude "(set-logic AUFBVFPDTNIRA)"
+(*
+    A    : Array
+    UF   : Uninterpreted Function
+    BV   : BitVectors
+    FP   : FloatingPoint
+    DT   : Datatypes
+    NIRA : NonLinear Integer+Real Arithmetic
+*)
+prelude "(set-info :source |VC generated by SPARK 2014|)"
+prelude "(set-info :category industrial)"
+prelude "(set-info :status unknown)"
+
+import "smt-libv2.drv"
+import "smt-libv2-bv.gen"
+import "cvc4_bv.gen"
+import "smt-libv2-floats.gen"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_literal"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+(* remove pointless quantifiers from the goal *)
+transformation "introduce_premises"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+(**
+Unfortunately, there is no specific output message when CVC4 reaches its resource limit
+steplimitexceeded "??"
+*)

drivers/smt-libv2-floats-int_via_bv.gen

+(* This is a encoding for int/float conversions via bitvectors. *)
+
+(* we do not translate of_int since z3 will not prove anything if it
+ * appears in its context, see PC07-014
+ *)
+
+theory ieee_float.Float32
+  (* check the sign bit; if pos |%1| else |%1| - 2^129 *)
+   syntax function to_int
+     "(ite (= ((_ extract 128 128) ((_ fp.to_sbv 129) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 129) %1 %2)) (- (bv2int ((_ fp.to_sbv 129) %1 %2)) (bv2int (bvshl (_ bv1 130) (_ bv129 130)))))"
+end
+
+theory ieee_float.Float64
+   (* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
+   syntax function to_int
+     "(ite (= ((_ extract 1024 1024) ((_ fp.to_sbv 1025) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 1025) %1 %2)) (- (bv2int ((_ fp.to_sbv 1025) %1 %2)) (bv2int (bvshl (_ bv1 1026) (_ bv1025 1026)))))"
+end

drivers/smt-libv2-floats-int_via_real.gen

+(* This is a encoding for int/float conversions via reals. *)
+
+theory ieee_float.GenericFloat
+  syntax function to_int "(to_int (fp.to_real (fp.roundToIntegral %1 %2)))"
+end
+
+theory ieee_float.Float32
+  syntax function of_int "((_ to_fp 8 24) %1 (to_real %2))"
+end
+
+theory ieee_float.Float64
+  syntax function of_int "((_ to_fp 11 53) %1 (to_real %2))"
+end

drivers/smt-libv2-floats.gen

@@ -70,8 +70,17 @@ theory ieee_float.Float32
   syntax function zeroF     "((_ to_fp 8 24) #x00000000)"
 
   prelude "(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
+  prelude "(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
+
 
   syntax predicate t'isFinite "(fp.isFinite32 %1)"
+  syntax predicate is_int "(fp.isIntegral32 %1)"
+
+  (* Faithful translations of the axiomatisation, mainly to remove this crud
+     from the smtlib output of SPARK. *)
+  syntax function round "(fp.to_real ((_ to_fp 8 24) %1 %2))"
+  syntax predicate in_range "(<= (abs %1) (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111)))"
+  syntax predicate no_overflow "(<= (abs (fp.to_real ((_ to_fp 8 24) %1 %2))) (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111)))"
 
   remove allprops
 end
@@ -85,8 +94,16 @@ theory ieee_float.Float64
   syntax function zeroF     "((_ to_fp 11 53) #x0000000000000000)"
 
   prelude "(define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
+  prelude "(define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
 
   syntax predicate t'isFinite "(fp.isFinite64 %1)"
+  syntax predicate is_int "(fp.isIntegral64 %1)"
+
+  (* Faithful translations of the axiomatisation, mainly to remove this crud
+     from the smtlib output of SPARK. *)
+  syntax function round "(fp.to_real ((_ to_fp 11 53) %1 %2))"
+  syntax predicate in_range "(<= (abs %1) (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))"
+  syntax predicate no_overflow "(<= (abs (fp.to_real ((_ to_fp 11 53) %1 %2))) (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))"
 
   remove allprops
 end

drivers/smt-libv2-gnatprove.gen

@@ -14,6 +14,8 @@ end
 
 theory _gnatprove_standard_th.Boolean_Func
    syntax function bool_eq "(= %1 %2)"
+   syntax function to_int "(ite %1 1 0)"
+   syntax function of_int "(distinct %1 0)"
    remove allprops
 end
 

src/transform/abstract_quantifiers.ml

+open Term
+open Decl
+
+let rec elim_quant pol f =
+  match f.t_node with
+  | Tquant _ ->
+    if pol then t_true else t_false
+  | _ ->
+    try
+      t_map_sign elim_quant pol f
+    with
+      Failure m -> f
+
+let elim_less (d:decl) =
+  match d.d_node with
+  | Dprop (Paxiom,v,t) ->
+    let t = elim_quant true t in
+    if t_equal t t_true then []
+    else
+      [decl_map (fun _ -> t) d]
+  | _ -> [d]
+
+let () =
+  Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
+    ~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context@."

src/transform/eliminate_symbol.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+open Ident
+open Ty
+open Term
+open Decl
+open Theory
+
+let meta_elim_ls = register_meta "ls:eliminate" [MTlsymbol]
+    ~desc:"Removes@ any@ expression@ containing@ a@ specific@ lsymbol."
+
+let eliminate_symbol env =
+  Trans.on_tagged_ls meta_elim_ls
+    (fun ls_elim ->
+       let elim_ls ls = Sls.exists (ls_equal ls) ls_elim in
+       let rec elim (t:term) =
+         match t.t_node with
+         | Tvar _ | Tconst _ | Ttrue | Tfalse -> false
+         | Tapp (ls,_) when elim_ls ls -> true
+         | _ -> t_any elim t
+       in
+       Trans.decl (fun d -> match d.d_node with
+           | Dparam l when (elim_ls l) -> []
+           | Dlogic l when
+               List.exists (fun (l,def) ->
+                   elim_ls l
+                || let _,t = open_ls_defn def in elim t) l -> []
+           | Dprop (Pgoal,pr,t) when (elim t) ->
+             [create_prop_decl Pgoal pr t_false]
+           | Dprop (_,_,t) when (elim t) -> []
+           | _ -> [d])
+         None)
+
+let () =
+  Trans.register_env_transform "eliminate_symbol" eliminate_symbol
+    ~desc:"Eliminate@ tagged@ symbol."

src/transform/eliminate_unknown_lsymbols.ml

+open Term
+open Decl
+open Theory
+open Task
+
+let debug = Debug.register_info_flag "eliminate_unknown_lsymbols"
+  ~desc:"Print@ debugging@ messages@ of@ the@ eliminate_unknown_types@ transformation."
+
+let abstraction (keep : lsymbol -> bool) =
+  let term_table = Hterm.create 257 in
+  let extra_decls = ref [] in
+
+  let rec abstract t : term =
+    match t.t_node with
+    | Tvar _ | Tconst _ | Tapp(_,[]) | Ttrue | Tfalse -> t
+    | Tapp (ls,_) when keep ls ->
+      t_map abstract t
+    | Tlet _ | Tnot _ | Tbinop _ | Tif _ ->
+      t_map abstract t
+    | _ ->
+      if Debug.test_flag debug then
+        Format.printf "eliminate@ %a@." Pretty.print_term t;
+      let (ls, tabs) = try Hterm.find term_table t with Not_found ->
+        let ls = create_lsymbol (Ident.id_fresh "abstr") [] t.t_ty in
+        let tabs = t_app ls [] t.t_ty in
+        Hterm.add term_table t (ls, tabs);
+        ls, tabs in
+      extra_decls := ls :: !extra_decls;
+      tabs
+  in
+
+  let abstract_decl (d : decl) : decl list =
+    let d = decl_map abstract d in
+    let l = List.fold_left
+        (fun acc ls -> create_param_decl ls :: acc)
+        [d] !extra_decls in
+    extra_decls := [];
+    l
+  in
+
+  Trans.decl abstract_decl None
+
+let syntactic_transform transf =
+  Trans.bind (Trans.fold (fun hd acc ->
+  match hd.task_decl.td_node with
+  | Decl { d_node = Dlogic ((ls,_def)::[]) } -> Sls.add ls acc
+  | _ -> acc) Sls.empty)
+  (fun decl ->
+  Trans.on_meta Printer.meta_syntax_converter (fun metas_conv ->
+  Trans.on_meta Printer.meta_syntax_logic (fun metas ->
+    let symbols = List.fold_left (fun acc meta_arg ->
+      match meta_arg with
+      | [Theory.MAls ls; Theory.MAstr _; Theory.MAint _] -> Sls.add ls acc
+      | _ -> assert false) decl metas_conv in
+    let symbols = List.fold_left (fun acc meta_arg ->
+      match meta_arg with
+      | [Theory.MAls ls; Theory.MAstr _; Theory.MAint _] -> Sls.add ls acc
+      | _ -> assert false) symbols metas in
+    let keep ls =  Sls.exists (ls_equal ls) symbols in
+    Trans.compose (transf keep)
+      (Trans.decl (fun d -> match d.d_node with
+           | Dparam l when not (keep l || l.ls_args = []) -> []
+           | _ -> [d]) None))))
+
+let () =
+  Trans.register_transform "eliminate_unknown_lsymbols"
+    (syntactic_transform abstraction)
+    ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ \
+      constants.@ Used@ by@ the@ Gappa@ pretty-printer."

src/transform/eliminate_unknown_types.ml

+open Term
+open Decl
+open Theory
+open Ty
+
+let debug = Debug.register_info_flag "eliminate_unknown_types"
+  ~desc:"Print@ debugging@ messages@ of@ the@ eliminate_unknown_types@ transformation."
+
+let syntactic_transform transf =
+  Trans.on_meta Printer.meta_syntax_type (fun metas ->
+      let symbols = List.fold_left (fun acc meta_arg ->
+      match meta_arg with
+      | [MAts ts; MAstr _; MAint _] -> Sts.add ts acc
+      | _ -> assert false) Sts.empty metas in
+    transf (fun ts -> Sts.exists (ts_equal ts) symbols))
+
+let remove_terms keep =
+  let keep_ls ls =
+    (* check that we want to keep all the types occurring in the type
+       of ls *)
+    List.for_all (fun ty -> ty_s_all keep ty) ls.ls_args
+    &&
+    begin match ls.ls_value with
+      | Some ty -> ty_s_all keep ty
+      | None -> true            (* bool are kept by default *)
+    end
+  in
+  let keep_term (t:term) =
+    t_s_all (fun ty -> ty_s_all keep ty) (fun _ -> true) t
+    &&
+    begin match t.t_ty with
+      | Some t -> ty_s_all keep t
+      | None -> true
+    end
+  in
+  Trans.decl (fun d ->
+    match d.d_node with
+    | Dtype ty when not (keep ty)                                ->
+      if Debug.test_flag debug then
+        Format.printf "remove@ type@ %a@." Pretty.print_ty_decl ty;
+      []
+    | Ddata l  when List.exists (fun (t,_) -> not (keep t)) l    ->
+      if Debug.test_flag debug then
+        Format.printf "remove@ data@ %a@." Pretty.print_data_decl (List.hd l);
+      []
+    | Dparam l when not (keep_ls l)                              ->
+      if Debug.test_flag debug then
+        Format.printf "remove@ param@ %a@." Pretty.print_ls l;
+      []
+    | Dlogic l when List.exists (fun (l,_) -> not (keep_ls l)) l ->
+      if Debug.test_flag debug then
+        Format.printf "remove@ logic@ %a@." Pretty.print_logic_decl (List.hd l);
+      []
+    | Dprop (Pgoal,pr,t) when not (keep_term t)                  ->
+      if Debug.test_flag debug then
+        Format.printf "change@ goal@ %a@." Pretty.print_term t;
+      [create_prop_decl Pgoal pr t_false]
+    | Dprop (_,_,t) when not (keep_term t)                       ->
+      if Debug.test_flag debug then
+        Format.printf "remove@ prop@ %a@." Pretty.print_term t;
+      []
+    | _ -> [d])
+    None
+
+let () =
+  Trans.register_transform "eliminate_unknown_types" (syntactic_transform remove_terms)
+    ~desc:"Remove@ types@ unknown@ to@ the@ prover@ and@ terms@ referring@ to@ them@."

[François Bobot]

I think :source should be removed. The category is also questionable. @sdailler @marche

[DAILLER Sylvain]

Bad copy-paste, my fault. Please don't hesitate to change this. You can remove the category too. Tell me if I need to do it.

[MARCHE Claude]

This is already taken care of in branch bugfix/v1.0, nothing more to do

[DAILLER Sylvain]

Perhaps we should do a merge of bugfix into master ?

[François Bobot]

I pushed a master with bugfix v1.0 at master-with-bugfixv1.0 for checking CI.

EDIT: merged in master.