Skip to content

GitLab

why3
why3
Commit 1b291599 authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

encoding_smt should work with the default option

parent 637c820f
Hide whitespace changes
Inline Side-by-side
Showing with 142 additions and 301 deletions
Makefile.in
View file @ 1b291599
......@@ -108,11 +108,11 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf
LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction encoding_decorate encoding_decorate_mono \
encoding_bridge\
split_conjunction encoding_const \
eliminate_definition eliminate_algebraic \
encoding_enumeration \
eliminate_inductive eliminate_let eliminate_if \
encoding_enumeration encoding encoding_decorate_mono \
encoding_decorate encoding_bridge \
explicit_polymorphism encoding_simple encoding_instantiate \
simplify_array filter_trigger split_goal
......@@ -464,27 +464,6 @@ install::
mkdir -p $(BINDIR)
cp -f bin/why3-cpulimit $(BINDIR)
#########
# drivers
#########
#Only generated drivers
DIR_DRIVERS := drivers/
DRIVERS := z3_inst cvc3_inst z3_simple cvc3_simple
DRIVERS := $(addsuffix .drv, $(DRIVERS))
DRIVERS := $(addprefix $(DIR_DRIVERS), $(DRIVERS))
#Not great for -j
$(DRIVERS) : $(DIR_DRIVERS)z3.drv $(DIR_DRIVERS)cvc3.drv drivers/gen_drv.sh
drivers/gen_drv.sh
byte opt: $(DRIVERS)
clean::
rm -f $(DRIVERS)
########
# bench
########
......
drivers/cvc3.drv
View file @ 1b291599
......@@ -20,7 +20,7 @@ transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_decorate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "Int"
......@@ -56,6 +56,9 @@ theory int.Int
remove prop Trans
remove prop Antisymm
remove prop Total
meta "encoding : kept" type int
end
theory real.Real
......@@ -90,6 +93,8 @@ theory real.Real
remove prop Antisymm
remove prop Total
meta "encoding : kept" type real
end
(*
......
drivers/gen_drv.sh deleted 100755 → 0
View file @ 637c820f
#!/bin/sh
DIR=drivers/
replace (){
prover=$1;
suffix=$2;
src=$3
dst=$4
cat ${DIR}${prover}.drv |sed -e "s/${src}/${dst}/" > ${DIR}${prover}_${suffix}.drv
}
for prover in z3 cvc3; do
replace $prover "inst" transformation\ \"encoding_decorate\" transformation\ \"encoding_instantiate\"
done
for prover in z3 cvc3; do
replace $prover "simple" transformation\ \"encoding_decorate\" \
"transformation \"encoding_enumeration\"\ntransformation \"explicit_polymorphism\"\ntransformation \"encoding_simple_kept\""
done
drivers/why3_encoding_decorate.drv
View file @ 1b291599
......@@ -8,7 +8,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "encoding_decorate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "int"
......
drivers/z3.drv
View file @ 1b291599
......@@ -20,7 +20,7 @@ transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_decorate"
transformation "encoding_smt"
(* transformation "encoding_decorate_every_simple" *)
theory BuiltIn
......@@ -33,7 +33,7 @@ end
theory int.Int
prelude ";;; this is a prelude for Z3, Arithmetic"
syntax logic zero "0"
syntax logic (+) "(+ %1 %2)"
......@@ -59,6 +59,8 @@ theory int.Int
remove prop Antisymm
remove prop Total
meta "encoding : kept" type int
end
......@@ -94,6 +96,8 @@ theory real.Real
remove prop Antisymm
remove prop Total
meta "encoding : kept" type real
end
(*
......
src/core/term.ml
View file @ 1b291599
......@@ -443,6 +443,7 @@ end)
module Sterm = Term.S
module Mterm = Term.M
module Hterm = Term.H
module Wterm = Term.W
module Hsfmla = Hashcons.Make (struct
......
src/core/term.mli
View file @ 1b291599
......@@ -173,6 +173,7 @@ and trigger = expr list
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
module Wterm : Hashweak.S with type key = term
module Mfmla : Map.S with type key = fmla
module Sfmla : Set.S with type elt = fmla
......
src/transform/encoding_bridge.ml
View file @ 1b291599
......@@ -25,18 +25,17 @@ open Task
open Theory
open Task
open Decl
open Encoding
let why_filename = ["transform" ; "encoding_decorate"]
let meta_kept = Encoding_decorate.meta_kept
(* From Encoding Polymorphism CADE07*)
type lconv = {tb2t : lsymbol;
t2tb : lsymbol;
tb : ty}
type tenv = {kept : Sts.t option;
type tenv = {kept : Sts.t;
clone_builtin : tysymbol -> Theory.tdecl list;
specials : lconv Hty.t;
trans_lsymbol : lsymbol Hls.t;
......@@ -52,7 +51,6 @@ let load_prelude kept env =
let type_t = Theory.ns_find_ts builtin.th_export ["t"] in
let trans_tsymbol = Hts.create 17 in
let clone_builtin ts =
let task = None in
let name = ts.ts_name.id_string in
let th_uc = create_theory (id_fresh ("bridge_for_"^name)) in
let th_uc =
......@@ -66,7 +64,7 @@ let load_prelude kept env =
let t2tb = ns_find_ls th.th_export ["t2tb"] in
let tb = ns_find_ts th.th_export ["tb"] in
let lconv = { tb2t = tb2t; t2tb = t2tb; tb = ty_app tb []} in
let task = Task.use_export task th in
let task = Task.use_export None th in
Hts.add trans_tsymbol ts tb;
Hty.add specials (ty_app ts []) lconv;
task_tdecls task in
......@@ -91,13 +89,7 @@ let rec ty_of_ty tenv ty =
let ty_of_ty_specials tenv ty =
if Hty.mem tenv.specials ty then ty else ty_of_ty tenv ty
let is_kept tenv ts =
ts.ts_args = [] &&
begin
match tenv.kept with
| None -> true (* every_simple *)
| Some s -> Sts.mem ts s
end
let is_kept tenv ts = ts.ts_args = [] && Sts.mem ts tenv.kept
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
......@@ -155,26 +147,15 @@ let rec rewrite_term tenv t =
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv) tl p.ls_args in
conv_res_app tenv p tl t.t_ty
| Tconst _ | Tvar _ | Tif _ | Tlet _ -> t_map fnT fnF t
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
| _ -> t_map fnT fnF t
and rewrite_fmla tenv f =
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
let fnT = rewrite_term tenv in
let fnF = rewrite_fmla tenv in
match f.f_node with
| Fapp(p, tl) when ls_equal p ps_equ ->
let tl = List.map fnT tl in
begin
match tl with
| [a1;_] ->
let ty = a1.t_ty in
let tl = List.map2 (conv_arg tenv) tl [ty;ty] in
f_app p tl
| _ -> assert false
end
| Fapp(p, [t1;t2]) when ls_equal p ps_equ ->
f_equ (fnT t1) (fnT t2)
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
......@@ -227,15 +208,8 @@ let decl tenv d =
let t env = Trans.on_meta meta_kept (fun tds ->
let s = Task.find_tagged_ts meta_kept tds Sts.empty in
let init_task,tenv = load_prelude (Some s) env in
let init_task,tenv = load_prelude s env in
Trans.tdecl (decl tenv) init_task)
let () = Trans.register_env_transform "encoding_bridge" t
let t_all env =
let init_task,tenv = load_prelude None env in
Trans.tdecl (decl tenv) init_task
let () = Trans.register_env_transform "encoding_bridge_every_simple" t_all
let () = register_enco_kept "bridge" t
src/transform/encoding_decorate.ml
View file @ 1b291599
......@@ -25,20 +25,14 @@ open Task
open Theory
open Task
open Decl
open Encoding
let why_filename = ["transform" ; "encoding_decorate"]
let meta_kept = register_meta "encoding_decorate : kept" [MTtysymbol]
(* From Encoding Polymorphism CADE07*)
type lconv = {d2t : lsymbol;
t2u : lsymbol;
tty : term}
type tenv = {kept : Sts.t option;
clone_builtin : tysymbol -> Theory.tdecl list;
specials : lconv Hty.t;
type tenv = {kept : Sts.t;
keptty : Sty.t;
deco : ty;
undeco : ty;
sort : lsymbol;
......@@ -58,42 +52,10 @@ let load_prelude kept env =
let task = None in
let task = Task.use_export task prelude in
let trans_tsymbol = Hts.create 17 in
let specials = Hty.create 17 in
let builtin = Env.find_theory env why_filename "Builtin" in
let type_t = Theory.ns_find_ts builtin.th_export ["t"] in
let logic_d2t = Theory.ns_find_ls builtin.th_export ["d2t"] in
let logic_t2u = Theory.ns_find_ls builtin.th_export ["t2u"] in
let logic_tty = Theory.ns_find_ls builtin.th_export ["tty"] in
let clone_builtin ts =
let task = None in
let name = ts.ts_name.id_string in
let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
let th_uc = Theory.use_export th_uc prelude in
let th_uc =
if ts_equal ts ts_int || ts_equal ts ts_real then th_uc
else Theory.add_ty_decl th_uc [ts,Tabstract] in
let ty = ty_app ts [] in
let add_fsymbol fs th_uc =
Theory.add_logic_decl th_uc [fs,None] in
let tty = create_fsymbol (id_clone ts.ts_name) [] tyty in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] ty in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [ty] undeco in
let th_uc = add_fsymbol d2ty (add_fsymbol ty2u (add_fsymbol tty th_uc)) in
let th_inst = create_inst
~ts:[type_t,ts]
~ls:[logic_d2t,d2ty;logic_t2u,ty2u;logic_tty,tty]
~lemma:[] ~goal:[] in
let lconv = { d2t = d2ty; t2u = ty2u; tty = t_app tty [] tyty} in
let th_uc = Theory.clone_export th_uc builtin th_inst in
let th = close_theory th_uc in
let task = Task.use_export task th in
Hts.add trans_tsymbol ts tty;
Hty.add specials (ty_app ts []) lconv;
task_tdecls task in
let kepty = Sts.fold (fun ts -> Sty.add (ty_app ts [])) kept Sty.empty in
task,
{ kept = kept;
clone_builtin = Wts.memoize 7 clone_builtin;
specials = specials;
keptty = kepty;
deco = deco;
undeco = undeco;
ty = tyty;
......@@ -102,13 +64,7 @@ let load_prelude kept env =
trans_tsymbol = trans_tsymbol}
let is_kept tenv ts =
ts.ts_args = [] &&
begin
ts_equal ts ts_int || ts_equal ts ts_real (* for the constant *)
|| match tenv.kept with
| None -> true (* every_simple *)
| Some s -> Sts.mem ts s
end
ts.ts_args = [] && Sts.mem ts tenv.kept
(* Translate a type to a term *)
let rec term_of_ty tenv tvar ty =
......@@ -131,14 +87,14 @@ let sort_app tenv tvar t ty =
(* Convert a type at the right of an arrow *)
let conv_ty_neg tenv ty =
if Hty.mem tenv.specials ty then
if Sty.mem ty tenv.keptty then
ty
else
tenv.deco
(* Convert a type at the left of an arrow *)
let conv_ty_pos tenv ty =
if Hty.mem tenv.specials ty then
if Sty.mem ty tenv.keptty then
ty
else
tenv.undeco
......@@ -163,31 +119,11 @@ let conv_ts tenv ts =
let tyl = List.map (fun _ -> tenv.ty) ts.ts_args in
create_fsymbol preid tyl tenv.ty
(* Convert the argument of a function from specials to deco or deco to
specials if needed*)
let conv_arg tenv tvar t ty =
let tty = t.t_ty in
if ty_equal tty ty then t else
if ty_equal ty tenv.deco then
let tylconv = Hty.find tenv.specials tty in
let t = (t_app tylconv.t2u [t] tenv.undeco) in
sort_app tenv tvar t tty
else (* tty is tenv.deco *)
begin
assert (ty_equal tty tenv.deco);
let tylconv = Hty.find tenv.specials ty in
t_app tylconv.d2t [t] ty
end
(* Convert to undeco or to a specials an application *)
let conv_res_app tenv tvar p tl ty =
let tty = Util.of_option p.ls_value in
if ty_equal tty ty then t_app p tl tty else
begin
assert (ty_equal tty tenv.undeco);
let t = t_app p tl tenv.undeco in
sort_app tenv tvar t ty
end
let conv_res_app tenv tvar t ty =
let tty = t.t_ty in
if Sty.mem tty tenv.keptty then t
else sort_app tenv tvar t ty
let conv_vs tenv tvar (vsvar,acc) vs =
let tres,vsres =
......@@ -214,7 +150,8 @@ let conv_vs_let vsvar vs ty_res =
let rec rewrite_term tenv tvar vsvar t =
(*Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t;*)
(* Format.eprintf "@[<hov 3>Term : %a : %a =>@\n@?" *)
(* Pretty.print_term t Pretty.print_ty t.t_ty; *)
let fnT = rewrite_term tenv tvar in
let fnF = rewrite_fmla tenv tvar vsvar in
match t.t_node with
......@@ -223,8 +160,8 @@ let rec rewrite_term tenv tvar vsvar t =
| Tapp(p,tl) ->
let tl = List.map (fnT vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
conv_res_app tenv tvar p tl t.t_ty
let t' = t_app_infer p tl in
conv_res_app tenv tvar t' t.t_ty
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) ->
......@@ -238,27 +175,19 @@ let rec rewrite_term tenv tvar vsvar t =
"Encoding decorate : I can't encode this term"
and rewrite_fmla tenv tvar vsvar f =
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
(* Format.eprintf "@[<hov>Fmla : %a =>@]@." Pretty.print_fmla f; *)
let fnT = rewrite_term tenv tvar vsvar in
let fnF = rewrite_fmla tenv tvar in
match f.f_node with
| Fapp(p, tl) when ls_equal p ps_equ ->
let tl = List.map fnT tl in
begin
match tl with
| [a1;_] ->
let ty =
if Hty.mem tenv.specials a1.t_ty
then a1.t_ty
else tenv.deco in
let tl = List.map2 (conv_arg tenv tvar) tl [ty;ty] in
f_app p tl
| _ -> assert false
end
| Fapp(p, [a1;a2]) when ls_equal p ps_equ ->
let a1 = fnT a1 in let a2 = fnT a2 in
(* Format.eprintf "@[<hov>%a : %a = %a : %a@]@." *)
(* Pretty.print_term a1 Pretty.print_ty a1.t_ty *)
(* Pretty.print_term a2 Pretty.print_ty a2.t_ty; *)
f_equ a1 a2
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
f_app p tl
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
......@@ -281,8 +210,7 @@ let decl (tenv:tenv) d =
(* let fnT = rewrite_term tenv in *)
let fnF = rewrite_fmla tenv in
match d.d_node with
| Dtype [ts,Tabstract] when is_kept tenv ts ->
tenv.clone_builtin ts
| Dtype [ts,Tabstract] when is_kept tenv ts -> [create_decl d]
| Dtype [ts,Tabstract] ->
let tty =
try
......@@ -333,15 +261,7 @@ let decl tenv d =
let t env = Trans.on_meta meta_kept (fun tds ->
let s = Task.find_tagged_ts meta_kept tds Sts.empty in
let init_task,tenv = load_prelude (Some s) env in
let init_task,tenv = load_prelude s env in
Trans.tdecl (decl tenv) init_task)
let () = Trans.register_env_transform "encoding_decorate" t
let t_all env =
let init_task,tenv = load_prelude None env in
Trans.tdecl (decl tenv) init_task
let () = Trans.register_env_transform "encoding_decorate_every_simple" t_all
let () = register_enco_poly "decorate" t
src/transform/encoding_decorate.mli
View file @ 1b291599
......@@ -23,4 +23,3 @@
Jean-Francois Couchot et Stephane Lescuyer *)
val why_filename : string list
val meta_kept : Theory.meta
src/transform/encoding_enumeration.ml
View file @ 1b291599
......@@ -79,12 +79,12 @@ let decl tenv d = match d.d_node with
| _ ->
[decl_map (rewrite_term tenv) (rewrite_fmla tenv) d]
let t =
let encoding_enumeration =
let projs = Hts.create 17 in
Trans.on_meta meta_enum (fun tds ->
let enum = Task.find_tagged_ts meta_enum tds Sts.empty in
let tenv = { enum = enum ; projs = projs } in
Trans.decl (decl tenv) None)
let () = Trans.register_transform "encoding_enumeration" t
let () = Trans.register_transform "encoding_enumeration" encoding_enumeration
src/transform/encoding_enumeration.mli
View file @ 1b291599
......@@ -17,3 +17,4 @@
(* *)
(**************************************************************************)
val encoding_enumeration : Task.task Trans.trans
src/transform/encoding_instantiate.ml
View file @ 1b291599
......@@ -26,23 +26,19 @@ open Task
open Theory
open Task
open Decl
open Encoding
let meta_kept = register_meta
"encoding_instantiate : kept" [MTtysymbol]
let meta_level = register_meta_excl
"encoding_instantiate : level" [MTstring]
let meta_complete = register_meta_excl
let meta_complete = register_meta_excl
"encoding_instantiate : complete" [MTstring]
(* Ce type est utiliser pour indiquer un alpha *)
let tv_dumb = create_tvsymbol (id_fresh "instantiate_alpha")
let tv_dumb = create_tvsymbol (id_fresh "instantiate_alpha")
let ty_dumb = ty_var tv_dumb
(* TODO : transmettre les tags des logiques polymorphe vers les logiques
instantié. Un tag sur un logique polymorphe doit être un tag sur toute
la famille de fonctions *)
(* TODO : transmettre les tags des logiques polymorphe vers les logiques
instantié. Un tag sur un logique polymorphe doit être un tag sur toute
la famille de fonctions *)
module OHTyl = OrderedHashList(Tty)
module Mtyl = Map.Make(OHTyl)
......@@ -59,7 +55,7 @@ type tenv =
| Incomplete (* The environnement when the transformation isn't complete*)
(* A type is projected on term or type depending
(* A type is projected on term or type depending
of its color (green part,red part, black part) *)
type tty =
| Tyterm of ty
......@@ -100,7 +96,7 @@ type env = {
edefined_tsymbol : tysymbol Mtyl.t Mts.t;
}
(* The environnement of the transformation during
(* The environnement of the transformation during
the transformation of a formula *)
type menv = {
tenv : tenv;
......@@ -114,12 +110,12 @@ type menv = {
let print_env fmt menv =
Format.fprintf fmt "defined_lsymbol (%a)@."
(Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
(Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
(Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
(Pp.print_list Pp.space Pretty.print_ty)
Pretty.print_ls)) menv.defined_lsymbol;
Format.fprintf fmt "defined_tsymbol (%a)@."
(Pp.print_iter2 Mts.iter Pp.semi Pp.comma Pretty.print_ts
(Pp.print_iter2 Mts.iter Pp.semi Pp.comma Pretty.print_ts
(Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
(Pp.print_list Pp.space Pretty.print_ty)
Pretty.print_ts)) menv.defined_tsymbol
......@@ -137,9 +133,9 @@ let rec projty menv tvar ty =
Tyty (Mty.find ty menv.projty)
with Not_found ->
match menv.tenv with
| Incomplete ->
| Incomplete ->
(* In this configuration there is no term representing type,
all type are a type or are in the black part
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
......@@ -152,7 +148,7 @@ let rec projty menv tvar ty =
| Complete ->
let tyl = List.map aux tyl in
let tyl_red = List.map reduce_to_type tyl in
let tys =
let tys =
try
Mtyl.find tyl_red (Mts.find ts menv.defined_tsymbol)
with Not_found ->
......@@ -162,8 +158,8 @@ let rec projty menv tvar ty =
match e with
| Tyterm _ -> (create_tvsymbol (id_fresh "a"))::acc
| Tyty _ -> acc) [] tyl in
let tys = if List.length args = List.length ts.ts_args
then ts
let tys = if List.length args = List.length ts.ts_args
then ts
else create_tysymbol (id_clone ts.ts_name) args None in
let insts = Mtyl.add tyl_red tys insts in
menv.defined_tsymbol <-
......@@ -187,7 +183,7 @@ let projty_real menv tvar ty = reduce_to_real (projty menv tvar ty)
(* | Complete -> projty menv Mtv.empty d *)
let reduce_to_default menv tvar d ty =
let reduce_to_default menv tvar d ty =
match projty menv tvar ty with
| Tyty ty -> ty
| Tyterm _ -> ty_var d
......@@ -196,7 +192,7 @@ let find_logic menv tvar p tyl ret =
if ls_equal p ps_equ then p else begin
let inst = ls_app_inst p tyl ret in
(*Format.eprintf "inst : %a@."
(Pp.print_iter2 Mtv.iter Pp.comma Pp.space Pp.nothing
(Pp.print_iter2 Mtv.iter Pp.comma Pp.space Pp.nothing
Pretty.print_ty) inst;*)
let inst = Mtv.mapi (reduce_to_default menv tvar) inst in
let inst_l = Mtv.fold (fun _ v acc -> v::acc) inst [] in
......@@ -208,9 +204,9 @@ let find_logic menv tvar p tyl ret =
(* (List.length inst_l); *)
try
let insts = Mls.find p menv.defined_lsymbol in
Mtyl.find inst_l insts
Mtyl.find inst_l insts
with Not_found ->