Commit a8ab6cc1 authored by Andrei Paskevich's avatar Andrei Paskevich

Merge branch 'no_t_vars'

parents c76541ab 3b84117c
(* 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
......
......@@ -28,18 +28,12 @@ trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*)
(* this is sound as long as int is the only kept type *)
transformation "encoding_smt"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(EQ %1 %2)"
meta "encoding : kept" type int
(* no symbol discrimination, no kept types *)
meta "select_inst" "none"
meta "select_lskept" "none"
meta "select_lsinst" "none"
meta "select_kept" "none"
meta "encoding : base" type int
end
theory int.Int
......
(* 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 "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"
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
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,46 @@ 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;
info_urg : string list ref;
}
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 print_type info fmt ty = match ty.ty_node with
| Tyvar _ when info.info_fmt = TFF0 ->
unsupported "TFF0 does not support polymorphic types"
| 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
| 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 ->
begin match Mty.find_opt ty !(info.info_srt) with
| Some ty -> print_type info fmt ty
| None ->
let ts = complex_type ty in let cty = ty_app ts [] in
let us = sprintf "@[<hov 2>tff(%s, type,@ %a:@ $tType).@]@\n@\n"
(id_unique pr_printer ts.ts_name) print_symbol ts.ts_name in
info.info_srt := Mty.add ty cty !(info.info_srt);
info.info_urg := us :: !(info.info_urg);
print_type info fmt cty
end
| None, tl ->
fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name
(print_list comma (print_type info)) tl
end
let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = false;
......@@ -73,8 +97,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 +154,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 +183,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,7 +197,7 @@ 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 ->
let print_type = print_type info in
......@@ -208,30 +232,43 @@ 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
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
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;
let print_decls fm =
let print_decl (sm,fm,ct) fmt d =
let info = { info_syn = sm; info_fmt = fm;
info_srt = ref ct; info_urg = ref [] } in
try print_decl info fmt d;
(sm,fm,!(info.info_srt)), !(info.info_urg)
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 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 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 +401,11 @@ 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_urg = ref [];
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
......
......@@ -649,7 +649,7 @@ let typecheck lib path ast =
let f,_ = fmla denv env impl (Some pol) [] e in
let f = if strict then f else
let q = if pol then Texists else Tforall in
let vl = Mvs.keys f.t_vars in
let vl = Mvs.keys (t_vars f) in
t_quant_close q vl [] f in
let env,uc = flush_impl ~strict env uc impl in
......
......@@ -30,7 +30,7 @@ type logic_decl = lsymbol * ls_defn
exception UnboundVar of vsymbol
let check_fvs f =
Mvs.iter (fun vs _ -> raise (UnboundVar vs)) f.t_vars;
t_v_fold (fun _ vs -> raise (UnboundVar vs)) () f;
t_prop f
let check_vl ty v = ty_equal_check ty v.vs_ty
......
......@@ -356,8 +356,8 @@ let quant_vars ~strict env vl =
let acc, vl = Lists.map_fold_left add Mstr.empty vl in
Mstr.set_union acc env, vl
let check_used_var vars vs =
if not (Mvs.mem vs vars) then
let check_used_var t vs =
if t_v_occurs vs t = 0 then
let s = vs.vs_name.id_string in
if not (String.length s > 0 && s.[0] = '_') then
Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s
......@@ -389,26 +389,26 @@ let term ~strict ~keep_loc env dt =
let v = create_vsymbol id (t_type t) in
let env = Mstr.add (preid_name id) v env in
let f = get uloc env df in
check_used_var f.t_vars v;
check_used_var f v;
t_let_close v t f
| DTcase (dt,bl) ->
let branch (dp,df) =
let env, p = pattern ~strict env dp in
let f = get uloc env df in
Svs.iter (check_used_var f.t_vars) p.pat_vars;
Svs.iter (check_used_var f) p.pat_vars;
t_close_branch p f in
t_case (get uloc env dt) (List.map branch bl)
| DTeps (id,dty,df) ->
let v = create_vsymbol id (ty_of_dty ~strict dty) in
let env = Mstr.add (preid_name id) v env in
let f = get uloc env df in
check_used_var f.t_vars v;
check_used_var f v;
t_eps_close v f
| DTquant (q,vl,dll,df) ->
let env, vl = quant_vars ~strict env vl in
let trl = List.map (List.map (get uloc env)) dll in
let f = get uloc env df in
List.iter (check_used_var f.t_vars) vl;
List.iter (check_used_var f) vl;
check_exists_implies q f;
t_quant_close q vl trl f
| DTbinop (op,df1,df2) ->
......
......@@ -39,8 +39,8 @@ let create_label s = Hslab.hashcons {
}
let lab_equal : label -> label -> bool = (==)
let lab_hash (lab : label) = lab.lab_tag
let lab_hash lab = lab.lab_tag
let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
(** Identifiers *)
......@@ -64,8 +64,8 @@ module Wid = Id.W
type preid = ident
let id_equal : ident -> ident -> bool = (==)
let id_hash id = Weakhtbl.tag_hash id.id_tag
let id_compare id1 id2 = Pervasives.compare (id_hash id1) (id_hash id2)
(* constructors *)
......
......@@ -23,6 +23,7 @@ type label = private {
module Mlab : Extmap.S with type key = label
module Slab : Extset.S with module M = Mlab
val lab_compare : label -> label -> int
val lab_equal : label -> label -> bool
val lab_hash : label -> int
......@@ -42,8 +43,8 @@ module Sid : Extset.S with module M = Mid
module Hid : Exthtbl.S with type key = ident
module Wid : Weakhtbl.S with type key = ident
val id_compare : ident -> ident -> int
val id_equal : ident -> ident -> bool
val id_hash : ident -> int
(* a user-created type of unregistered identifiers *)
......
......@@ -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 ->