Arrays : a new transformation which use instantiation and bridge.

Currently only in the driver z3_array.drv

drivers/why3_smt.drv

@@ -3,12 +3,14 @@
 printer "why3"
 filename "%f-%t-%g.why"
 
+transformation "inline_trivial"
 transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 
-transformation "encoding_smt"
+transformation "encoding_smt_array"
+transformation "encoding_sort"
 
 theory BuiltIn
   syntax type  int  "int"

drivers/z3.drv

@@ -22,8 +22,6 @@ transformation "eliminate_algebraic"
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
 
-(* transformation "encoding_array" *)
-
 transformation "encoding_smt"
 transformation "encoding_sort"
 
@@ -134,10 +132,10 @@ theory int.EuclideanDivision
 end
 
 theory transform.array.Array
-  syntax logic get "(select %1 %2)"
-  syntax logic set "(store %1 %2)"
-  remove prop Select_eq
-  remove prop Select_neq
+  syntax cloned logic get "(select %1 %2)"
+  syntax cloned logic set "(store %1 %2 %3)"
+  remove cloned prop Select_eq
+  remove cloned prop Select_neq
 
 end
 

drivers/z3_array.drv

+(* Why driver for SMT syntax *)
+
+prelude ";;; this is a prelude for Z3"
+
+printer "smtv1"
+filename "%f-%t-%g.smt"
+
+valid "^unsat"
+unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
+time "why3cpulimit time : %s s"
+
+
+(* À discuter *)
+transformation "simplify_recursive_definition"
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "encoding_smt_array"
+transformation "encoding_sort"
+
+theory BuiltIn
+  syntax type int   "Int"
+  syntax type real  "Real"
+  syntax logic (=)  "(= %1 %2)"
+end
+
+theory int.Int
+
+  prelude ";;; this is a prelude for Z3 integer arithmetic"
+
+  syntax logic zero "0"
+  syntax logic one  "1"
+
+  syntax logic (+)  "(+ %1 %2)"
+  syntax logic (-)  "(- %1 %2)"
+  syntax logic (*)  "(* %1 %2)"
+  syntax logic (-_) "(- %1)"
+
+  syntax logic (<=) "(<= %1 %2)"
+  syntax logic (<)  "(< %1 %2)"
+  syntax logic (>=) "(>= %1 %2)"
+  syntax logic (>)  "(> %1 %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+  meta "encoding : kept" type int
+
+end
+
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3 real arithmetic"
+
+  syntax logic zero "0.0"
+  syntax logic one  "1.0"
+
+  syntax logic (+)  "(+ %1 %2)"
+  syntax logic (-)  "(- %1 %2)"
+  syntax logic (*)  "(* %1 %2)"
+  syntax logic (/)  "(/ %1 %2)"
+  syntax logic (-_) "(- %1)"
+  syntax logic inv  "(/ 1.0 %1)"
+
+  syntax logic (<=) "(<= %1 %2)"
+  syntax logic (<)  "(< %1 %2)"
+  syntax logic (>=) "(>= %1 %2)"
+  syntax logic (>)  "(> %1 %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+  meta "encoding : kept" type real
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool   "bool"
+   syntax logic True  "true"
+   syntax logic False "false"
+   syntax logic andb  "(and %1 %2)"
+   syntax logic orb   "(or %1 %2)"
+   syntax logic xorb  "(xor %1 %2)"
+   syntax logic notb  "(not %1)"
+   meta cloned "encoding_decorate : kept" type bool
+end
+*)
+
+
+theory int.EuclideanDivision
+   syntax logic div "(div %1 %2)"
+   syntax logic mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory transform.array.Array
+  syntax cloned logic get "(select %1 %2)"
+  syntax cloned logic set "(store %1 %2 %3)"
+  remove cloned prop Select_eq
+  remove cloned prop Select_neq
+
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

examples/programs/encodebench.rc

@@ -8,6 +8,13 @@ prover = "yices"
 prover = "eprover"
 timelimit = 1
 
+[tools array]
+command = "why3-cpulimit %t %m -s z3 -smt %f 2>&1"
+driver = "/usr/local/share/why3/drivers/z3_array.drv"
+#loadpath = "examples/programs"
+#use = "meta.Partial_incomplete"
+timelimit = 1
+
 [tools instantiate]
 prover = "cvc3"
 prover = "z3"
@@ -31,6 +38,7 @@ transform = "split_goal"
 
 [bench fast_and_funny]
 tools = fast
+tools = array
 tools = instantiate
 probs = funny
 timeline = "encodebench.time"

examples/programs/meta.why

@@ -2,6 +2,10 @@ theory Partial
   meta "enco_kept" "instantiate"
 end
 
+theory Partial_incomplete
+  meta "encoding_instantiate : complete" "no"
+end
+
 theory Explicit
 
 end
\ No newline at end of file

src/core/trans.ml

@@ -218,7 +218,7 @@ let print_meta f m task =
     Pp.print_iter1 Stdecl.iter Pp.newline Pretty.print_tdecl fmt
       (find_meta_tds task m).tds_set
   in
-  Debug.dprintf f "%a@." print_tds m;
+  Debug.dprintf f "meta %s : %a@." m.Theory.meta_name print_tds m;
   task
 
 (** register transformations *)

src/transform/encoding.ml

@@ -23,6 +23,7 @@ open Task
 open Trans
 
 let meta_kept = register_meta "encoding : kept" [MTty]
+let meta_kept_array = register_meta "encoding : kept_array" [MTty]
 let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
 
 let debug = Debug.register_flag "encoding"

src/transform/encoding.mli

@@ -23,8 +23,18 @@ open Task
 open Trans
 
 val meta_kept : meta
+val meta_kept_array : meta
 val meta_base : meta
 
 val register_enco_select : string -> (env -> task trans) -> unit
 val register_enco_kept : string -> (env -> task trans) -> unit
 val register_enco_poly : string -> (env -> task trans) -> unit
+
+
+val monomorphise_goal : Task.task Trans.trans
+val maybe_encoding_enumeration : Task.task Trans.trans
+
+val enco_poly_smt : Env.env -> Task.task Trans.trans
+val print_kept : Task.task Trans.trans
+
+val encoding_smt : Env.env ->  Task.task Trans.trans

src/transform/encoding_arrays.ml

@@ -27,6 +27,7 @@ open Task
 open Decl
 open Encoding
 
+(*
 (* Ce type est utiliser pour indiquer un underscore *)
 let tv_dumb = create_tvsymbol (id_fresh "Dumb")
 let ty_dumb = ty_var tv_dumb
@@ -306,10 +307,10 @@ let collect_arrays poly_ts tds =
       | Some ty -> ty)
       ts tys in
   Sts.fold extract tds Mty.empty
-
+*)
 let meta_mono_array = register_meta "encoding_arrays : mono_arrays"
   [MTtysymbol;MTty;MTty]
-
+(*
 (* Some general env creation function *)
 let create_env env task thpoly tds =
   let pget = ns_find_ls thpoly.th_export ["get"] in
@@ -388,7 +389,7 @@ let encoding_arrays env =
   Trans.on_used_theory thpoly (fun used ->
     if not used then Trans.identity
     else Trans.on_tagged_ts meta_kept_array (create_trans_complete env thpoly))
-
+*)
 (* This one take use the tag but also all the type which appear in the goal *)
 let is_ty_mono ~only_mono ty =
   try
@@ -399,7 +400,7 @@ let is_ty_mono ~only_mono ty =
     true
   with Exit when not only_mono -> false
 
-
+(*
 (* select the type array which appear as argument of set and get.
   set and get must be in sls *)
 let find_mono_array ~only_mono sls sty f =
@@ -442,7 +443,150 @@ let trans_array env =
 let trans_array env = Trans.compose (trans_array env) (encoding_arrays env)
 
 let () = Trans.register_env_transform "encoding_array" trans_array
+*)
+(*********************************)
+(** Another way *)
+(** Use partial on the subtype of arrays and twin on arrays
+    (just add the twin) *)
+
+(* select the type array which appear as argument of set and get.
+  set and get must be in sls. After that take the subtype of them *)
+let find_mono_array ~only_mono sls sty f =
+  let add sty ls tyl _ =
+    match tyl with
+      | ty::_ when Sls.mem ls sls && is_ty_mono ~only_mono ty ->
+        Sty.add ty sty
+      | _ -> sty in
+  f_app_fold add sty f
+
+let create_meta_ty meta ty = create_meta meta [MAty ty]
 
+let create_meta_ty meta = Wty.memoize 17 (create_meta_ty meta)
+
+let create_meta_tyl meta =
+  let cmty = create_meta_ty meta in
+  fun sty d ->
+    Sty.fold (flip $ cons cmty) sty d
+
+let create_meta_tyl_arrays = create_meta_tyl meta_kept_array
+let create_meta_tyl_kept = create_meta_tyl meta_kept
+
+let subtype ty acc =
+  let rec ty_add sty ty = ty_fold ty_add (Sty.add ty sty) ty in
+  (* don't add the top type, only the subtype *)
+  ty_fold ty_add acc ty
+
+let mono_in_goal sls pr f =
+  let sty = (try find_mono_array ~only_mono:true sls Sty.empty f
+    with Exit -> assert false) (*monomorphise goal should have been used*) in
+  let decls = create_meta_tyl_arrays sty
+    [create_decl (create_prop_decl Pgoal pr f)] in
+  let sty = Sty.fold subtype sty Sty.empty in
+  create_meta_tyl_kept sty decls
+
+let mono_in_goal sls = Trans.tgoal (mono_in_goal sls)
+
+let select_subterm_array th_array =
+  let set = ns_find_ls th_array.th_export ["set"] in
+  let get = ns_find_ls th_array.th_export ["get"] in
+  let sls = Sls.add set (Sls.add get Sls.empty) in
+  mono_in_goal sls
+
+(** Were all is tide together *)
+open Trans
+open Encoding_instantiate
+let meta_arrays_to_meta_kept =
+  Trans.on_tagged_ty meta_kept_array (fun sty ->
+    Trans.store (function
+    | Some { task_decl = td; task_prev = prev } ->
+      let add ty task = add_meta task meta_kept [Theory.MAty ty] in
+      let task = Sty.fold add sty prev in
+      add_tdecl task td
+    | _ -> assert false
+    ))
+
+(* Some general env creation function *)
+let create_env_array env thpoly task tenv kept kept_array =
+  let pget = ns_find_ls thpoly.th_export ["get"] in
+  let pset = ns_find_ls thpoly.th_export ["set"] in
+   let pt = ns_find_ts thpoly.th_export ["t"] in
+  (* let pkey = ns_find_ts thpoly.th_export ["key"] in *)
+  (* let pvalue = ns_find_ts thpoly.th_export ["value"] in *)
+  (* Clonable theories of arrays *)
+  let thclone = Env.find_theory env ["transform";"array"] "Array" in
+  let cget = ns_find_ls thclone.th_export ["get"] in
+  let cset = ns_find_ls thclone.th_export ["set"] in
+  let ct = ns_find_ts thclone.th_export ["t"] in
+  let ckey = ns_find_ts thclone.th_export ["key"] in
+  let celt = ns_find_ts thclone.th_export ["elt"] in
+  let clone_arrays ty (task,tenv) =
+    let key,elt =
+      match ty.ty_node with
+        | Tyapp (_,[key;elt]) -> key,elt
+        | _ -> assert false in
+    (** create needed alias for the instantiation *)
+    let add_ty task ty =
+      match ty.ty_node with
+        | Tyapp (ts,[]) -> task,ts
+        | _ ->
+          let ts = create_tysymbol (id_fresh "alias for clone") [] (Some ty) in
+          add_ty_decl task [ts,Tabstract],ts in
+    let task,tskey = add_ty task key in
+    let task,tselt = add_ty task elt in
+    let ts_name = "bta_"^(Pp.string_of_wnl Pretty.print_ty ty) in
+    let ts = create_tysymbol (id_fresh ts_name) [] None in
+    let task = add_ty_decl task [ts,Tabstract] in
+    let th_inst = create_inst ~ts:[ct,ts; ckey,tskey; celt,tselt] ~ls:[]
+      ~lemma:[] ~goal:[] in
+    let task = Task.clone_export task thclone th_inst in
+    (** Recover the subtitution *)
+    let sls = match task with
+      | Some {task_decl = {td_node = Clone(_,{sm_ls=sls})}} -> sls
+      | _ -> assert false in
+    (** type *)
+    (* let tsy = ty_app ts [] in *)
+    (** add get to lsymbol *)
+    (** Warning its the instanciation, so [elt;key] is really not a
+        safe way to define the instancition (depend on variable
+        order...) *)
+    let add s = Mtyl.add [elt;key] (Mls.find cget sls) s in
+    let edefined_lsymbol = Mls.change pget
+      (function | None -> Some (add Mtyl.empty) | Some s -> Some (add s))
+      tenv.edefined_lsymbol in
+    (** add set to lsymbol *)
+    let add s = Mtyl.add [elt;key] (Mls.find cset sls) s in
+    let edefined_lsymbol = Mls.change pset
+      (function | None -> Some (add Mtyl.empty) | Some s -> Some (add s))
+      edefined_lsymbol in
+    (** add arrays to tsymbol *)
+    let add s = Mtyl.add [key;elt] ts s in
+    let edefined_tsymbol = Mts.change pt
+      (function | None -> Some (add Mtyl.empty) | Some s -> Some (add s))
+      tenv.edefined_tsymbol in
+    task,{tenv with edefined_lsymbol = edefined_lsymbol;
+      edefined_tsymbol = edefined_tsymbol
+         } in
+  (** add the type which compose keep *)
+  let task_tenv = create_env task tenv kept in
+  (** add the clone *)
+  Sty.fold clone_arrays kept_array task_tenv
+
+let encoding_smt_array env =
+  let th_array = Env.find_theory env ["array"] "Array" in
+  Trans.on_used_theory th_array (fun used ->
+    if not used then Encoding.encoding_smt env else
+      compose Encoding.monomorphise_goal
+        (compose Encoding.maybe_encoding_enumeration
+           (compose (select_subterm_array th_array)
+              (compose Encoding.print_kept
+                 (compose (Encoding_instantiate.t
+                             (create_env_array env th_array))
+                    (compose meta_arrays_to_meta_kept
+                       (compose Encoding.print_kept
+                          (compose (Encoding_bridge.t env)
+                             (Encoding.enco_poly_smt env)))))))))
+
+let () = Trans.register_env_transform "encoding_smt_array" encoding_smt_array
 
 (*
 Local Variables:

src/transform/encoding_bridge.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    François Bobot                                                     *)
+(*    Jean-Christophe Filliâtre                                          *)
+(*    Claude Marché                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+val t : Env.env -> Task.task Trans.trans

src/transform/encoding_instantiate.ml

@@ -17,7 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
+open Stdlib
 open Util
 open Ident
 open Ty
@@ -57,13 +57,6 @@ end)
 module Mtyl = Map.Make(OHTyl)
 module Htyl = Hashtbl.Make(OHTyl)
 
-type tenv_aux = {
-  deco : ty;
-  undeco : ty;
-  sort : lsymbol;
-  ty : ty;
-}
-
 type tenv =
   | Complete (* The transformation keep the polymorphism *)
   | Incomplete (* The environnement when the transformation isn't complete*)
@@ -105,11 +98,14 @@ let reduce_to_real = function
 type env = {
   etenv : tenv;
   ekeep : Sty.t;
+  prop_toremove : ty Mtv.t Mpr.t;
   eprojty : ty Mty.t;
   edefined_lsymbol : lsymbol Mtyl.t Mls.t;
   edefined_tsymbol : tysymbol Mtyl.t Mts.t;
 }
 
+type auto_clone = task -> tenv -> Sty.t -> Sty.t -> task * env
+
 (* The environnement of the transformation during
    the transformation of a formula *)
 type menv = {
@@ -367,10 +363,51 @@ let ty_quant =
     | _ -> ty_fold add_vs s ty in
   f_ty_fold add_vs Stv.empty
 
+let add_decl_ud menv task =
+  let task = Sts.fold
+    (fun ts task -> add_ty_decl task [ts,Tabstract])
+    menv.undef_tsymbol task in
+  let task = Sls.fold
+    (fun ls task -> add_logic_decl task [ls,None])
+    menv.undef_lsymbol task in
+  task
+
+
 (* The Core of the transformation *)
 let fold_map task_hd ((env:env),task) =
   match task_hd.task_decl.td_node with
-    | Use _ | Clone _ | Meta _ -> env,add_tdecl task task_hd.task_decl
+    | Use _ | Clone _ -> env,add_tdecl task task_hd.task_decl
+    | Meta(meta,ml) ->
+      begin try
+        let menv =  {
+          tenv = env.etenv;
+          keep = env.ekeep;
+          projty = env.eprojty;
+          defined_lsymbol = env.edefined_lsymbol;
+          defined_tsymbol = env.edefined_tsymbol;
+          undef_lsymbol = Sls.empty;
+          undef_tsymbol = Sts.empty;
+        } in
+        let map = function
+          | MAty ty -> MAty (projty_real menv Mtv.empty ty)
+          (* | MAts {ts_name = name; ts_args = []; ts_def = Some ty} -> *)
+          (*   MAts (conv_ts tenv ud name ty) *)
+          (* | MAts {ts_args = []; ts_def = None} as x -> x *)
+          | MAts _ -> raise Exit
+          | MAls _ -> raise Exit
+          | MApr _ -> raise Exit
+          | MAstr _ as s -> s
+          | MAint _ as i -> i in
+        let arg = (List.map map ml) in
+        let task = add_meta (add_decl_ud menv task) meta arg in
+        {env with edefined_lsymbol = menv.defined_lsymbol;
+          edefined_tsymbol = menv.defined_tsymbol;
+          eprojty = menv.projty;
+        }, task
+      with
+        | Printer.UnsupportedType _
+        | Exit -> env,add_tdecl task task_hd.task_decl
+      end
     | Decl d -> match d.d_node with
     | Dtype [_,Tabstract] -> (env,task)
     (* Nothing here since the type kept are already defined and the other
@@ -409,6 +446,11 @@ Perhaps you could use eliminate_definition"
         undef_tsymbol = Sts.empty;
       } in
       let conv_f task tvar =
+        if begin
+          try (Mtv.equal ty_equal) tvar (Mpr.find pr env.prop_toremove)
+          with Not_found -> false end
+        then task
+        else
         (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
         (*   (f_ty_subst tvar Mvs.empty f) *)
         (*   print_env menv; *)
@@ -423,12 +465,7 @@ Perhaps you could use eliminate_definition"
         (*   menv.undef_lsymbol *)
         (*   (Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) *)
         (*   menv.undef_tsymbol; *)
-        let task = Sts.fold
-          (fun ts task -> add_ty_decl task [ts,Tabstract])
-          menv.undef_tsymbol task in
-        let task = Sls.fold
-          (fun ls task -> add_logic_decl task [ls,None])
-          menv.undef_lsymbol task in
+        let task = add_decl_ud menv task in
         let task = add_prop_decl task k pr f in
         task
       in
@@ -465,6 +502,7 @@ let create_env task tenv keep =
   task,{
     etenv = tenv;
     ekeep = keep;
+    prop_toremove = Mpr.empty;
     eprojty = projty;
     edefined_lsymbol = Mls.empty;
     edefined_tsymbol = Mts.empty
@@ -493,12 +531,29 @@ let create_trans_complete kept complete =
 let encoding_instantiate =
   Trans.on_tagged_ty meta_kept (fun kept ->
   Trans.on_meta_excl meta_complete (fun complete ->
-  create_trans_complete kept complete))
+    create_trans_complete kept complete))
 
 let () =
   register_enco_kept "instantiate" (fun _ -> encoding_instantiate)
 
 
+let create_trans_complete create_env kept kept_array complete =
+  let task = use_export None builtin_theory in
+  let tenv = match complete with
+    | None | Some [MAstr "yes"] -> Complete
+    | Some [MAstr "no"] ->  Incomplete
+    | _ -> failwith "instantiate complete wrong argument" in
+  let init_task,env = create_env task tenv kept kept_array in
+  Trans.fold_map fold_map env init_task
+
+let t create_env =
+  Trans.on_tagged_ty meta_kept (fun kept ->
+  Trans.on_meta_excl meta_complete (fun complete ->
+    Trans.on_tagged_ty meta_kept_array (fun kept_array ->
+      create_trans_complete create_env kept kept_array complete)))
+
+
+
 (* Select *)
 
 let find_mono ~only_mono sty f =