After encoding smt type applications still exist but type variables not.

Encoding_instantiate keeps the type of the green part complexe.
Encoding_simple2 (bad name) replaces the complexe types by constants.

One day we can add a better comprehesion of (int,int) array for instance
 inside encoding_simple2 or inside the printers.

Makefile.in

@@ -113,7 +113,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
 		eliminate_inductive eliminate_let eliminate_if \
 		encoding_enumeration encoding encoding_decorate_mono \
 		encoding_decorate encoding_bridge \
-		explicit_polymorphism encoding_simple encoding_instantiate \
+		explicit_polymorphism encoding_simple encoding_simple2 encoding_instantiate \
 		simplify_array filter_trigger split_goal
 
 LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa

drivers/cvc3.drv

@@ -21,6 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
+transformation "encoding_simple2"
 
 theory BuiltIn
   syntax type int   "Int"

drivers/z3.drv

@@ -21,6 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
+transformation "encoding_simple2"
 (* transformation "encoding_decorate_every_simple" *)
 
 theory BuiltIn

src/transform/encoding_decorate.ml

@@ -57,10 +57,9 @@ let load_prelude kept env =
     | Some ty -> Sty.add ty sty
     | None -> Sty.add (ty_app ts []) sty in
   let kepty = Sts.fold add kept Sty.empty in
-  let add ty sts = match ty.ty_node with
-    | Tyapp (ts,[]) -> Sts.add ts sts
-    | _ -> sts in
-  let kept = Sty.fold add kepty Sts.empty in
+  let add_ts sts ts = Sts.add ts sts in
+  let add_ts ty sts = ty_s_fold add_ts sts ty in
+  let kept = Sty.fold add_ts kepty Sts.empty in
   task,
   { kept = kept;
     keptty = kepty;
@@ -73,9 +72,6 @@ let load_prelude kept env =
     trans_consts = Hterm.create 3;
   }
 
-let is_kept tenv ts = 
-  ts.ts_args = [] && Sts.mem ts tenv.kept
-
 (* Translate a type to a term *)
 let rec term_of_ty tenv tvar ty =
   match ty.ty_node with
@@ -231,7 +227,6 @@ let decl (tenv:tenv) d =
   let fnF = rewrite_fmla tenv in
   match d.d_node with
     | Dtype [{ts_def = Some _},_] -> []
-    | Dtype [ts,Tabstract] when is_kept tenv ts -> [create_decl d]
     | Dtype [ts,Tabstract] -> 
         let tty = 
           try 
@@ -240,7 +235,8 @@ let decl (tenv:tenv) d =
             let tty = conv_ts tenv ts in
             Hts.add tenv.trans_tsymbol ts tty;
             tty in
-        [create_decl (create_logic_decl [(tty,None)])]
+        let td = [create_decl (create_logic_decl [(tty,None)])] in
+        if Sts.mem ts tenv.kept then (create_decl d)::td else td
     | Dtype _ -> Printer.unsupportedDecl 
         d "encoding_decorate : I can work only on abstract \
             type which are not in recursive bloc."

src/transform/encoding_instantiate.ml

@@ -141,9 +141,10 @@ let rec projty menv tvar ty =
               (* In this configuration there is no term representing type,
                  all type are a type or are in the black part
                  (the or is not a xor)*)
-              let preid = id_clone ts.ts_name in
-              let ts = create_tysymbol preid [] None (*Some ty*) in
-              let tty = ty_app ts [] in
+              (* let preid = id_clone ts.ts_name in *)
+              (* let ts = create_tysymbol preid [] None (\*Some ty*\) in *)
+              (* let tty = ty_app ts [] in *)
+              let tty = ty in
               menv.projty <- Mty.add ty tty menv.projty;
               menv.undef_tsymbol <- Sts.add ts menv.undef_tsymbol;
               (*Format.eprintf "projty : ts : %a env : %a@." Pretty.print_ts ts
@@ -449,33 +450,25 @@ let collect_green_part tds =
   let sts = Task.find_tagged_ts meta_kept tds Sts.empty in
   let extract ts tys =
     assert (ts.ts_args = []); (* UnsupportedTySymbol? *)
-    Sty.add (match ts.ts_def with
+    Mty.add (match ts.ts_def with
       | None -> ty_app ts []
-      | Some ty -> ty) tys in
-  let sty = Sts.fold extract sts Sty.empty in
-  (* complete by subterm *)
-  let rec subty sty ty = ty_fold subty (Sty.add ty sty) ty in
-  Sty.fold (flip subty) sty Sty.empty
-
+      | Some ty -> ty) ts tys in
+  Sts.fold extract sts Mty.empty
+  
+  
 
 (* Some general env creation function *)
 let create_env task tenv tds =
   let keep = collect_green_part tds in
-  let projty = Sty.fold (fun ty ty_ty ->
-    let ty2 = match ty.ty_node with
-      | Tyapp (_,[]) -> ty
-      | Tyapp (ts,_) ->
-        let ts = create_tysymbol (id_clone ts.ts_name) [] None in
-        ty_app ts []
-      | _ -> assert false in
-    Mty.add ty ty2 ty_ty)
+  let projty = Mty.fold (fun ty _ ty_ty ->
+    Mty.add ty ty ty_ty)
     keep Mty.empty in
-  let task = Mty.fold (fun _ ty task ->
-    match ty.ty_node with
-      | Tyapp (ts,[]) ->
-        let task = add_ty_decl task [ts,Tabstract] in
-        add_meta task meta_kept [MAts ts]
-      | _ -> assert false) projty task in
+  let task = Mty.fold (fun ty ts task ->
+    let add_ts task ts = add_ty_decl task [ts,Tabstract] in
+    let task = ty_s_fold add_ts task ty in
+    let task = add_ts task ts in
+    task (* the meta is yet here *)) keep task in
+  let keep = Mty.fold (fun ty _ sty -> Sty.add ty sty) keep Sty.empty in
     task,{
     etenv = tenv;
     ekeep = keep;

src/transform/encoding_simple2.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Util
+open Ident
+open Ty
+open Term
+open Decl
+open Theory
+open Task
+
+let meta_kept = register_meta "encoding_decorate : kept" [MTtysymbol]
+
+(* From Encoding Polymorphism CADE07*)
+
+type tenv = {
+  specials : tysymbol Hty.t;
+  trans_lsymbol : lsymbol Hls.t
+}
+
+let init_tenv = {
+  specials = Hty.create 17;
+  trans_lsymbol = Hls.create 17 }
+
+
+(* Convert type *)
+let conv_ty tenv undefined ty =
+  match ty.ty_node with
+    | Tyapp (_,[]) -> ty
+    | Tyapp (ts,_) -> 
+        let ts = 
+          try
+            Hty.find tenv.specials ty
+          with Not_found ->
+            let ts = create_tysymbol (id_dup ts.ts_name) [] None in
+            Hty.add tenv.specials ty ts;
+            ts in
+        Hts.replace undefined ts ();
+        ty_app ts [] 
+    | _ -> Printer.unsupportedType ty "type variable must be encoded"
+
+(* Convert a variable *)
+let conv_vs tenv ud vs =
+  let ty = conv_ty tenv ud vs.vs_ty in
+  if ty_equal ty vs.vs_ty then vs else
+  create_vsymbol (id_dup vs.vs_name) ty
+
+(* Convert a logic symbol to the encoded one *)
+let conv_ls tenv ud ls =
+  if ls_equal ls ps_equ then ls
+  else try Hls.find tenv.trans_lsymbol ls with Not_found ->
+  let ty_res = Util.option_map (conv_ty tenv ud) ls.ls_value in
+  let ty_arg = List.map (conv_ty tenv ud) ls.ls_args in
+  let ls' =
+    if Util.option_eq ty_equal ty_res ls.ls_value &&
+       List.for_all2 ty_equal ty_arg ls.ls_args then ls
+    else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res
+  in
+  Hls.add tenv.trans_lsymbol ls ls';
+  ls'
+
+
+let rec rewrite_term tenv ud vm t =
+  let fnT = rewrite_term tenv ud in
+  let fnF = rewrite_fmla tenv ud in
+  match t.t_node with
+  | Tconst _ -> t
+  | Tvar x ->
+      Mvs.find x vm
+  | Tapp (fs,tl) ->
+      let fs = conv_ls tenv ud fs in
+      let tl = List.map (fnT vm) tl in
+      t_app fs tl (of_option fs.ls_value)
+  | Tif (f, t1, t2) ->
+      t_if (fnF vm f) (fnT vm t1) (fnT vm t2)
+  | Tlet (t1, b) ->
+      let u,t2,close = t_open_bound_cb b in
+      let u' = conv_vs tenv ud u in
+      let t1' = fnT vm t1 in
+      let t2' = fnT (Mvs.add u (t_var u') vm) t2 in
+      t_let t1' (close u' t2')
+  | Tcase _ | Teps _ | Tbvar _ ->
+      Printer.unsupportedTerm t "unsupported term"
+
+and rewrite_fmla tenv ud vm f =
+  let fnT = rewrite_term tenv ud in
+  let fnF = rewrite_fmla tenv ud in
+  match f.f_node with
+  | Fapp (ps,tl) when ls_equal ps ps_equ ->
+      f_app ps (List.map (fnT vm) tl)
+  | Fapp (ps,tl) ->
+      let ps = conv_ls tenv ud ps in
+      let tl = List.map (fnT vm) tl in
+      f_app ps tl
+  | Fquant (q,b) ->
+      let vl, tl, f1, close = f_open_quant_cb b in
+      let add m v = let v' = conv_vs tenv ud v in Mvs.add v (t_var v') m, v' in
+      let vm', vl' = Util.map_fold_left add vm vl in
+      let tl' = tr_map (fnT vm') (fnF vm') tl in
+      let f1' = fnF vm' f1 in
+      f_quant q (close vl' tl' f1')
+  | Flet (t1, b) ->
+      let u,f1,close = f_open_bound_cb b in
+      let u' = conv_vs tenv ud u in
+      let t1' = fnT vm t1 in
+      let f1' = fnF (Mvs.add u (t_var u') vm) f1 in
+      f_let t1' (close u' f1')
+  | Fcase _ ->
+      Printer.unsupportedFmla f "unsupported formula"
+  | _ -> f_map (fnT vm) (fnF vm) f
+
+let decl_ud ud acc =
+  let add ts () acc = (create_ty_decl [ts,Tabstract])::acc in
+  Hts.fold add ud acc
+
+let decl tenv d =
+  let fnT = rewrite_term tenv in
+  let fnF = rewrite_fmla tenv in
+  match d.d_node with
+  | Dtype dl ->
+      let add acc = function
+        | ({ts_def = Some _} | {ts_args = _::_}), Tabstract -> acc
+        | _, Tabstract as d -> d::acc
+        | _ -> Printer.unsupportedDecl d "use eliminate_algebraic"
+      in
+      let l = List.rev (List.fold_left add [] dl) in
+      if l = [] then [] else [create_ty_decl l]
+  | Dlogic ll ->
+    let ud = Hts.create 3 in
+    let conv = function
+      | ls, None -> create_logic_decl [conv_ls tenv ud ls, None]
+      | _ -> Printer.unsupportedDecl d "use eliminate_definition"
+    in
+    decl_ud ud (List.map conv ll)
+  | Dind _ ->
+      Printer.unsupportedDecl d "use eliminate_inductive"
+  | Dprop _ ->
+    let ud = Hts.create 3 in
+    decl_ud ud [decl_map (fnT ud Mvs.empty) (fnF ud Mvs.empty) d]
+
+let t = 
+  let tenv = init_tenv in
+  Trans.decl (decl tenv) None
+
+let () = Trans.register_transform "encoding_simple2" t
+