Commit e6d18142 authored by MARCHE Claude's avatar MARCHE Claude

versions "if poly" of discriminate and encoding_smt, encoding_tptp

Temporary trick to enforce encoding in presence of algebraic types,
even if they are not polymorphic
parent 1d343bdb
......@@ -18,10 +18,11 @@ timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
......@@ -29,8 +30,8 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
theory BuiltIn
syntax type int "Int"
......
......@@ -57,7 +57,10 @@ let find_in_decl d =
| Ddata dl ->
Debug.dprintf debug "@[Ddata %a@]@."
(Pp.print_list Pp.space Pretty.print_data_decl) dl;
List.iter (fun (ts,_) -> check_ts ts) dl
List.iter (fun (ts,_) -> check_ts ts) dl;
(* FIXME: temporary trick to activate encoding in presence
of algebraic data types *)
raise Found
| Dparam ls ->
Debug.dprintf debug "@[Dparam %a@]@." Pretty.print_ls ls;
check_ls ls
......@@ -65,10 +68,12 @@ let find_in_decl d =
Debug.dprintf debug "@[Dlogic %a@]@."
(Pp.print_list Pp.space Pretty.print_ls) (List.map fst dl);
List.iter (fun (ls,_) -> check_ls ls) dl
(* TODO: check also that definition bodies are monomorphic ? *)
| Dind (_,indl) ->
Debug.dprintf debug "@[Dind %a@]@."
(Pp.print_list Pp.space Pretty.print_ls) (List.map fst indl);
List.iter (fun (ls,_) -> check_ls ls) indl
(* TODO: check also that clauses are monomorphic ? *)
| Dprop (_,pr,t) ->
Debug.dprintf debug "@[Dprop %a@]@." Pretty.print_pr pr;
try check_term t
......
......@@ -309,6 +309,17 @@ let () = Trans.register_env_transform "discriminate" discriminate
~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \
predicate@ symbols@ and@ monomorphize@ task@ premises."
let discriminate_if_poly env =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
(function
| [] -> discriminate env
| _ -> Trans.identity)
let () =
Trans.register_env_transform "discriminate_if_poly"
discriminate_if_poly
~desc:"Same@ as@ discriminate@ but@ only@ if@ polymorphism@ appear."
let on_lsinst fn =
let add_ls acc = function
| [MAls ls; MAls nls] -> Mls.add nls ls acc
......
......@@ -184,7 +184,7 @@ let eliminate_definition_if_poly =
let () =
Trans.register_transform "eliminate_definition_if_poly"
eliminate_definition_if_poly
~desc:"Same@ as@ eliminate_definition@ but@ only@ if@ polymorphism@ appear.";
~desc:"Same@ as@ eliminate_definition@ but@ only@ if@ polymorphism@ appear."
(** Bisect *)
open Task
......
......@@ -82,3 +82,28 @@ let () = register_env_transform "encoding_smt" encoding_smt
let () = register_env_transform "encoding_tptp" encoding_tptp
~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."
(* encoding only if polymorphism occurs *)
let encoding_smt_if_poly env =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
(function
| [] -> encoding_smt env
| _ -> Trans.identity)
let () =
Trans.register_env_transform "encoding_smt_if_poly"
encoding_smt_if_poly
~desc:"Same@ as@ encoding_smt@ but@ only@ if@ polymorphism@ appear."
let encoding_tptp_if_poly env =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
(function
| [] -> encoding_tptp env
| _ -> Trans.identity)
let () =
Trans.register_env_transform "encoding_tptp_if_poly"
encoding_tptp_if_poly
~desc:"Same@ as@ encoding_tptp@ but@ only@ if@ polymorphism@ appear."
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment