Commit 92341bd0 authored by David Hauzar's avatar David Hauzar

Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

Conflicts:
	src/printer/smtv2.ml
parents cecd6d8c 503a2ee6
......@@ -256,7 +256,8 @@ pvsbin/
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
/examples/in_progress/prover/build/*__*.ml
/examples/in_progress/prover/.depend
# modules
/modules/string/
......
(* Why driver for first-order tptp provers *)
printer "tptp-tff1"
filename "%f-%t-%g.p"
valid "PROOF-FOUND"
timeout "Zenon error: could not find a proof within the time limit"
outofmemory "Zenon error: could not find a proof within the memory size limit"
unknown "NO-PROOF" "no proof found"
time "why3cpulimit time : %s s"
(* to be improved *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
import "discrimination.gen"
......@@ -55,7 +55,7 @@ module PrimeNumbers
(** Bertrand's postulate, admitted as an axiom
(the label is there to suppress the warning issued by Why3) *)
axiom Bertrand_postulate "W:conservative_extension:N" :
axiom Bertrand_postulate "W:non_conservative_extension:N" :
forall p: int. prime p -> not (no_prime_in p (2*p))
(** [prime_numbers m] returns an array containing the first [m]
......
......@@ -57,6 +57,7 @@ type info = {
info_num : tptp_number;
info_srt : ty Mty.t ref;
info_urg : string list ref;
info_rules : Decl.Spr.t;
}
let complex_type = Wty.memoize 3 (fun ty ->
......@@ -247,22 +248,34 @@ 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_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
(*
Format.eprintf "Dprop for %s: rewrite rules:" pr.pr_name.id_string;
Spr.iter (fun pr -> Format.eprintf " %s" pr.pr_name.id_string) info.info_rules;
Format.eprintf "@.";
*)
let annotation = if Spr.mem pr info.info_rules then ",rewrite" else "" in
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, axiom,@ %a%s).@]@\n@\n"
head print_pr pr (print_fmla info) f annotation
| Dprop (Pgoal, pr, 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_decls fm nm =
let print_decls fm nm rew_rules =
(*
Format.eprintf "rewrite rules:";
Spr.iter (fun pr -> Format.eprintf " %s" pr.pr_name.id_string) rew_rules;
Format.eprintf "@.";
*)
let print_decl (sm,fm,ct) fmt d =
let info = { info_syn = sm;
info_fmt = fm;
info_num = nm;
info_srt = ref ct;
info_urg = ref [] } in
info_urg = ref [];
info_rules = rew_rules } in
try print_decl info fmt d;
(sm,fm,!(info.info_srt)), !(info.info_urg)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
......@@ -272,7 +285,6 @@ let print_decls fm nm =
Trans.fold print_decl ((sm,fm,Mty.empty),[]))
let print_task fm nm =
let print_decls = print_decls fm nm in
fun args ?old:_ fmt task ->
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
......@@ -281,7 +293,10 @@ let print_task fm nm =
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
print (snd (Trans.apply print_decls task));
let print_decls_with_meta =
Trans.on_tagged_pr Compute.meta_rewrite (print_decls fm nm)
in
print (snd (Trans.apply print_decls_with_meta task));
pp_print_flush fmt ()
let () =
......@@ -429,7 +444,9 @@ let print_dfg args ?old:_ fmt task =
info_fmt = FOF;
info_num = TPTP;
info_urg = ref [];
info_srt = ref Mty.empty } in
info_srt = ref Mty.empty ;
info_rules = Spr.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
......
......@@ -444,6 +444,15 @@ version_ok = "0.7.1"
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon.drv"
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
version_ok = "0.4.0"
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon_modulo.drv"
[ATP iprover]
name = "iProver"
exec = "iprover"
......
......@@ -304,20 +304,21 @@ let rec print_term info fmt t =
| Tif (f1,t1,t2) ->
fprintf fmt "@[(ite %a@ %a@ %a)@]"
(print_fmla info) f1 (print_term info) t1 (print_term info) t2
| Tcase({t_node = Tvar v}, bl) ->
print_branches info v print_term fmt bl
| Tcase(t, bl) ->
let ty = t_type t in
begin
match ty.ty_node with
| Tyapp (ts,_) when ts_equal ts ts_bool ->
print_boolean_branches info t fmt bl
print_boolean_branches info t print_term fmt bl
| _ ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_branches info subject print_term) bl;
forget_var subject
match t.t_node with
| Tvar v -> print_branches info v print_term fmt bl
| _ ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_branches info subject print_term) bl;
forget_var subject
end
| Teps _ -> unsupportedTerm t
"smtv2: you must eliminate epsilon"
......@@ -385,19 +386,27 @@ and print_fmla info fmt f =
fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v
| Tcase({t_node = Tvar v}, bl) ->
print_branches info v print_fmla fmt bl
| Tcase(t, bl) ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_branches info subject print_fmla) bl;
forget_var subject
let ty = t_type t in
begin
match ty.ty_node with
| Tyapp (ts,_) when ts_equal ts ts_bool ->
print_boolean_branches info t print_fmla fmt bl
| _ ->
match t.t_node with
| Tvar v -> print_branches info v print_fmla fmt bl
| _ ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_branches info subject print_fmla) bl;
forget_var subject
end
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
check_exit_vc_line f
and print_boolean_branches info subject fmt bl =
and print_boolean_branches info subject pr fmt bl =
let error () = unsupportedTerm subject
"smtv2: bad pattern-matching on Boolean (compile_match missing?)"
in
......@@ -408,11 +417,12 @@ and print_boolean_branches info subject fmt bl =
begin
match p1.pat_node with
| Papp(cs,_) ->
let csname = if ls_equal cs fs_bool_true then "true" else "false" in
fprintf fmt "@[(ite (= %a %s) %a %a)@]"
(print_term info) subject
(String.lowercase cs.ls_name.id_string) (* dirty hack, sorry *)
(print_term info) t1
(print_term info) t2
csname
(pr info) t1
(pr info) t2
| _ -> error ()
end
| _ -> error ()
......
......@@ -9,3 +9,5 @@
(* *)
(********************************************************************)
val meta_rewrite : Theory.meta
module M
use import int.Int
let f (x:int) (ghost y:int) : int
ensures { x = y }
= x
let g (z:int) = f z 0
end
\ No newline at end of file
theory T
use import set.Set
meta "rewrite" prop mem_empty
meta "rewrite" prop add_def1
goal g: mem 1 (add 2 (add 1 (add 0 empty)))
end
module M
use import bool.Bool
let f (a b : bool)
ensures {
(andb (orb a b) (notb (andb a b)) = True)
<->
( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
}
= ()
let g (a b : bool)
ensures {
(xorb a b = True)
<->
( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
}
= ()
end
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