diff --git a/Makefile.in b/Makefile.in index 39fd11dfa96d453764823e62cfa7c6e2e0f82feb..1096ae40add7cb60b0e062f7c93aeff26a73ab58 100644 --- a/Makefile.in +++ b/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 diff --git a/drivers/cvc3.drv b/drivers/cvc3.drv index d5f461212be54ff4e582cf1402a1905c1559e100..01819bcbcee283e534f3ddcfad04fed4117ef6fc 100644 --- a/drivers/cvc3.drv +++ b/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" diff --git a/drivers/z3.drv b/drivers/z3.drv index 27d2644b1ae532475e69494db6d077ad54d3bfa3..03f1cb9410b006aae32059faad9e83d16335d534 100644 --- a/drivers/z3.drv +++ b/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 diff --git a/src/transform/encoding_decorate.ml b/src/transform/encoding_decorate.ml index 3ec60393523efcc44109dd3b03598ced28f9f444..82f565a3689ccfebadb28947295f6fd1b7a7376a 100644 --- a/src/transform/encoding_decorate.ml +++ b/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." diff --git a/src/transform/encoding_instantiate.ml b/src/transform/encoding_instantiate.ml index 50dd80e53cdad40ec64ddf060d02c182171cbe0a..d9c99ded7bbabd0c3fbc7c59b7067e22ca615f46 100644 --- a/src/transform/encoding_instantiate.ml +++ b/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; diff --git a/src/transform/encoding_simple2.ml b/src/transform/encoding_simple2.ml new file mode 100644 index 0000000000000000000000000000000000000000..8e285187f0606ceb9c5f576e81ff34ad65d866ab --- /dev/null +++ b/src/transform/encoding_simple2.ml @@ -0,0 +1,162 @@ +(**************************************************************************) +(* *) +(* 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 +