Commit 9640fb2b authored by Andrei Paskevich's avatar Andrei Paskevich

implement printers as memoizing transformations

also, avoid the "encoding_sort" transformation, if it can be done
directly in the printer.

On the same example as in the previous commits, this gives 5x
acceleration together with some memory usage reduction.
parent 064fe08e
(* Why3 driver for beagle
see http://users.cecs.anu.edu.au/~baumgart/systems/beagle/ *)
printer "tptp-tff"
printer "tptp-tff0"
filename "%f-%t-%g.p"
valid "Proof found"
......@@ -34,8 +34,10 @@ transformation "eliminate_algebraic"
transformation "eliminate_let"
transformation "eliminate_if"
transformation "discriminate"
transformation "encoding_smt"
transformation "encoding_sort"
import "discrimination.gen"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
......@@ -45,11 +47,6 @@ theory BuiltIn
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "eliminate_algebraic" "no_index"
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "all"
meta "select_kept" "all"
end
theory int.Int
......
(* Why3 driver for princess
see http://www.philipp.ruemmer.org/princess.shtml *)
printer "tptp-tff"
printer "tptp-tff0"
filename "%f-%t-%g.p"
valid "Proof found"
......@@ -36,7 +36,8 @@ transformation "eliminate_if"
transformation "discriminate"
transformation "encoding_smt"
transformation "encoding_sort"
import "discrimination.gen"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
......@@ -46,11 +47,6 @@ theory BuiltIn
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "eliminate_algebraic" "no_index"
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "all"
meta "select_kept" "all"
end
theory int.Int
......
......@@ -33,7 +33,7 @@ transformation "encoding_smt"
theory BuiltIn
syntax predicate (=) "(EQ %1 %2)"
meta "encoding : kept" type int
meta "encoding : base" type int
(* no symbol discrimination, no kept types *)
meta "select_inst" "none"
......
(* Why driver for first-order tptp provers supporting TFF0 *)
printer "tptp-tff"
printer "tptp-tff0"
filename "%f-%t-%g.p"
valid "Proof found"
......@@ -29,8 +29,10 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "discriminate"
transformation "encoding_smt"
transformation "encoding_sort"
import "discrimination.gen"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
......@@ -40,11 +42,6 @@ theory BuiltIn
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "eliminate_algebraic" "no_index"
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "all"
meta "select_kept" "all"
end
theory int.Int
......
(* Why driver for first-order tptp provers supporting TFF1 *)
printer "tptp-tff1"
filename "%f-%t-%g.p"
valid "Proof found"
invalid "Completion found"
valid "^% SZS status Theorem"
valid "^% SZS status Unsatisfiable"
unknown "^% SZS status CounterSatisfiable" ""
unknown "^% SZS status Satisfiable" ""
timeout "^% SZS status Timeout"
unknown "^% SZS status GaveUp" ""
fail "^% SZS status Error" ""
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
(* to be improved *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
syntax type int "$int"
syntax type real "$real"
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "eliminate_algebraic" "no_index"
end
theory int.Int
syntax function zero "0"
syntax function one "1"
syntax function (+) "$sum(%1,%2)"
syntax function (-) "$difference(%1,%2)"
syntax function (*) "$product(%1,%2)"
syntax function (-_) "$uminus(%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
syntax predicate (>=) "$greatereq(%1,%2)"
syntax predicate (>) "$greater(%1,%2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
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
remove prop ZeroLessOne
end
theory real.Real
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "$sum(%1,%2)"
syntax function (-) "$difference(%1,%2)"
syntax function (*) "$product(%1,%2)"
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
syntax predicate (>=) "$greatereq(%1,%2)"
syntax predicate (>) "$greater(%1,%2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory int.EuclideanDivision
syntax function div "$quotient_e(%1,%2)"
syntax function mod "$remainder_e(%1,%2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
remove prop Div_inf
remove prop Div_inf_neg
remove prop Mod_0
remove prop Div_1_left
remove prop Div_minus1_left
remove prop Mod_1_left
remove prop Mod_minus1_left
end
theory tptp.Univ
syntax type iType "$i"
meta "encoding : kept" type iType
end
theory tptp.IntTrunc
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function round "$round(%1)"
syntax function to_int "$to_int(%1)"
syntax predicate is_int "$is_int(%1)"
syntax predicate is_rat "$is_rat(%1)"
end
theory tptp.IntDivT
syntax function div_t "$quotient_t(%1,%2)"
syntax function mod_t "$remainder_t(%1,%2)"
end
theory tptp.IntDivF
syntax function div_f "$quotient_f(%1,%2)"
syntax function mod_f "$remainder_f(%1,%2)"
end
theory tptp.Rat
syntax type rat "$rat"
syntax function zero "0/1"
syntax function one "1/1"
syntax function (+) "$sum(%1,%2)"
syntax function (-) "$difference(%1,%2)"
syntax function (*) "$product(%1,%2)"
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
syntax predicate (>=) "$greatereq(%1,%2)"
syntax predicate (>) "$greater(%1,%2)"
syntax function to_rat "$to_rat(%1)"
syntax predicate is_int "$is_int(%1)"
syntax predicate is_rat "$is_rat(%1)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
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
remove prop ZeroLessOne
meta "encoding : kept" type rat
end
theory tptp.RatTrunc
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function round "$round(%1)"
syntax function to_int "$to_int(%1)"
end
theory tptp.RatDivE
syntax function div "$quotient_e(%1,%2)"
syntax function mod "$remainder_e(%1,%2)"
end
theory tptp.RatDivT
syntax function div_t "$quotient_t(%1,%2)"
syntax function mod_t "$remainder_t(%1,%2)"
end
theory tptp.RatDivF
syntax function div_f "$quotient_f(%1,%2)"
syntax function mod_f "$remainder_f(%1,%2)"
end
theory tptp.Real
syntax function to_real "$to_real(%1)"
end
theory real.Truncate
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
end
theory tptp.RealTrunc
syntax function round "$round(%1)"
syntax function to_int "$to_int(%1)"
syntax predicate is_int "$is_int(%1)"
syntax predicate is_rat "$is_rat(%1)"
end
theory tptp.RealDivE
syntax function div "$quotient_e(%1,%2)"
syntax function mod "$remainder_e(%1,%2)"
end
theory tptp.RealDivT
syntax function div_t "$quotient_t(%1,%2)"
syntax function mod_t "$remainder_t(%1,%2)"
end
theory tptp.RealDivF
syntax function div_f "$quotient_f(%1,%2)"
syntax function mod_f "$remainder_f(%1,%2)"
end
theory tptp.IntToRat
syntax function to_rat "$to_rat(%1)"
end
theory tptp.IntToReal
syntax function to_real "$to_real(%1)"
end
theory tptp.RealToRat
syntax function to_rat "$to_rat(%1)"
end
theory tptp.RatToReal
syntax function to_real "$to_real(%1)"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
......@@ -22,7 +22,6 @@ transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
theory BuiltIn
syntax type int "Int"
......
......@@ -45,22 +45,55 @@ let print_pr fmt pr =
let forget_var v = forget_id ident_printer v.vs_name
let forget_tvar v = forget_id ident_printer v.tv_name
type tptp_format = FOF | TFF0 | TFF1
type info = {
info_syn : syntax_map;
info_fof : bool;
info_fmt : tptp_format;
info_srt : ty Mty.t ref;
}
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar tv -> print_tvar fmt tv
| Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_type info) fmt tl
| None -> begin match tl with
| [] -> print_symbol fmt ts.ts_name
| _ -> fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name
(print_list comma (print_type info)) tl
end
| Tyapp (ts, tl) ->
begin match query_syntax info.info_syn ts.ts_name, tl with
| Some s, _ -> syntax_arguments s (print_type info) fmt tl
| None, [] -> print_symbol fmt ts.ts_name
| None, _ when info.info_fmt = TFF0 ->
print_type info fmt (Mty.find ty !(info.info_srt))
| None, tl ->
fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name
(print_list comma (print_type info)) tl
end
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec iter_complex_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "TFF0 does not support polymorphic types"
| Tyapp (_, []) -> ()
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some _ -> List.iter (iter_complex_type info fmt) l
| None when Mty.mem ty !(info.info_srt) -> ()
| None ->
let ts = complex_type ty in
fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ $tType).@]@\n@\n"
(id_unique pr_printer ts.ts_name) print_symbol ts.ts_name;
info.info_srt := Mty.add ty (ty_app ts []) !(info.info_srt)
end
let iter_complex_type info fmt ty =
try iter_complex_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let find_complex_type info fmt f = if info.info_fmt = TFF0 then
t_ty_fold (fun () ty -> iter_complex_type info fmt ty) () f
let iter_complex_type info fmt ty = if info.info_fmt = TFF0 then
iter_complex_type info fmt ty
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = false;
......@@ -73,8 +106,7 @@ let number_format = {
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
(Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)"));
Number.def_real_support = Number.Number_unsupported
;
Number.def_real_support = Number.Number_unsupported;
}
let rec print_app info fmt ls tl oty =
......@@ -131,7 +163,7 @@ and print_fmla info fmt f = match f.t_node with
let q = match q with Tforall -> "!" | Texists -> "?" in
let vl, _tl, f = t_open_quant fq in
let print_vsty fmt vs =
if info.info_fof then fprintf fmt "%a" print_var vs
if info.info_fmt = FOF then fprintf fmt "%a" print_var vs
else fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty in
fprintf fmt "%s[%a]:@ %a" q
(print_list comma print_vsty) vl (print_fmla info) f;
......@@ -160,8 +192,9 @@ let print_fmla info fmt f =
Stv.iter forget_tvar tvs
let print_decl info fmt d = match d.d_node with
| Dtype _ when info.info_fof -> ()
| Dtype _ when info.info_fmt = FOF -> ()
| Dtype { ts_def = Some _ } -> ()
| Dtype { ts_args = _::_ } when info.info_fmt = TFF0 -> ()
| Dtype ts when query_syntax info.info_syn ts.ts_name <> None -> ()
| Dtype ts ->
let print_arg fmt _ = fprintf fmt "$tType" in
......@@ -173,9 +206,11 @@ let print_decl info fmt d = match d.d_node with
fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ %a).@]@\n@\n"
(id_unique pr_printer ts.ts_name)
print_symbol ts.ts_name print_sig ts
| Dparam _ when info.info_fof -> ()
| Dparam _ when info.info_fmt = FOF -> ()
| Dparam ls when query_syntax info.info_syn ls.ls_name <> None -> ()
| Dparam ls ->
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
let print_type = print_type info in
let print_val fmt = function
| Some ty -> print_type fmt ty
......@@ -208,30 +243,44 @@ let print_decl info fmt d = match d.d_node with
"TPTP does not support inductive predicates, use eliminate_inductive"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
| Dprop (Paxiom, pr, f) ->
let head = if info.info_fof then "fof" else "tff" in
find_complex_type info fmt f;
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, axiom,@ %a).@]@\n@\n"
head print_pr pr (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
let head = if info.info_fof then "fof" else "tff" in
find_complex_type info fmt f;
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, conjecture,@ %a).@]@\n"
head print_pr pr (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let print_task fof _env pr thpr _blacklist ?old:_ fmt task =
forget_all ident_printer;
forget_all pr_printer;
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = { info_syn = get_syntax_map task; info_fof = fof } in
fprintf fmt "@[%a@]@."
(print_list nothing (print_decl info)) (Task.task_decls task)
let () = register_printer "tptp-tff" (print_task false) ~desc:"TPTP TFF format"
let () = register_printer "tptp-fof" (print_task true) ~desc:"TPTP FOF format"
let print_decls fm =
let print_decl (sm,fm,ct) fmt d =
let info = {
info_syn = sm; info_fmt = fm; info_srt = ref ct } in
try print_decl info fmt d; (sm,fm,!(info.info_srt))
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Trans.fold print_decl ((sm,fm,Mty.empty),[]))
let print_task fm =
let print_decls = print_decls fm in
fun _env pr thpr _blacklist ?old:_ fmt task ->
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
print (snd (Trans.apply print_decls task));
pp_print_flush fmt ()
let () = register_printer "tptp-tff0" (print_task TFF0) ~desc:"TPTP TFF0 format"
let () = register_printer "tptp-tff1" (print_task TFF1) ~desc:"TPTP TFF1 format"
let () = register_printer "tptp-fof" (print_task FOF) ~desc:"TPTP FOF format"
(** DFG input format for SPASS >= 3.8
(with the help of Daniel Wand)
......@@ -364,7 +413,8 @@ let print_dfg _env pr thpr _blacklist ?old:_ fmt task =
fprintf fmt
"name({**}). author({**}). status(unknown). description({**}).@\n";
fprintf fmt "end_of_list.@\n@\n";
let info = { info_syn = get_syntax_map task; info_fof = true } in
let info = { info_syn = get_syntax_map task;
info_fmt = FOF; info_srt = ref Mty.empty } in
let dl = Task.task_decls task in
let tl = List.filter (is_type info) dl in
let fl = List.filter (is_function info) dl in
......
......@@ -266,7 +266,7 @@ let add_syntax_map td sm = match td.td_node with
let query_syntax sm id = Mid.find_opt id sm
let fold_tdecls fn acc =
let on_syntax_map fn =
Trans.on_meta meta_syntax_type (fun sts ->
Trans.on_meta meta_syntax_logic (fun sls ->
Trans.on_meta meta_remove_prop (fun spr ->
......@@ -274,27 +274,27 @@ let fold_tdecls fn acc =
let sm = List.fold_left sm_add_ts sm sts in
let sm = List.fold_left sm_add_ls sm sls in
let sm = List.fold_left sm_add_pr sm spr in
Trans.fold (fun t -> fn sm t.task_decl) acc)))
fn sm)))
let sprint_tdecls (fn : syntax_map -> tdecl pp) =
let buf = Buffer.create 512 in
let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a) =
let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in
let print sm td acc =
fun td (acc,strl) ->
Buffer.reset buf;
Format.fprintf fmt "%a@?" (fn sm) td;
Buffer.contents buf :: acc in
fold_tdecls print []
let acc = fn acc fmt td in
Format.pp_print_flush fmt ();
acc, Buffer.contents buf :: strl
let sprint_decls (fn : syntax_map -> decl pp) =
let buf = Buffer.create 512 in
let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a) =
let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in
let print sm td acc = match td.td_node with
fun td (acc,strl) -> match td.td_node with
| Decl d ->
Buffer.reset buf;
Format.fprintf fmt "%a@?" (fn sm) d;
Buffer.contents buf :: acc
| _ -> acc in
fold_tdecls print []
let acc = fn acc fmt d in
Format.pp_print_flush fmt ();
acc, Buffer.contents buf :: strl
| _ -> acc, strl
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -72,10 +72,15 @@ val syntax_arguments_typed :
(** {2 pretty-printing transformations (useful for caching)} *)
val fold_tdecls : (syntax_map -> tdecl -> 'a -> 'a) -> 'a -> 'a Trans.trans
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
val sprint_tdecls : (syntax_map -> tdecl pp) -> string list Trans.trans
val sprint_decls : (syntax_map -> decl pp) -> string list Trans.trans
val sprint_tdecl :
('a -> Format.formatter -> Theory.tdecl -> 'a) ->
Theory.tdecl -> 'a * string list -> 'a * string list
val sprint_decl :
('a -> Format.formatter -> Decl.decl -> 'a) ->
Theory.tdecl -> 'a * string list -> 'a * string list
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -251,6 +251,7 @@ let print_enum_decl fmt ts csl =
(print_list alt2 print_cs) csl
let print_ty_decl info fmt ts =
if ts.