From 240085a6230da6674c818253e580aef5149bce36 Mon Sep 17 00:00:00 2001 From: marche Date: Tue, 10 Nov 2009 14:43:54 +0000 Subject: use only why-dp, support for z3 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12491 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/dp/dp.ml | 74 ++++++++++++++++++++++++++++++++++++++-------------- plugins/dp/dp.mli | 3 +-- plugins/dp/dp_why.ml | 37 ++++++++++++++++++++++---- plugins/dp/g_dp.ml4 | 4 +++ 4 files changed, 91 insertions(+), 27 deletions(-) diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 46e5b50aa..34b32c0a7 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -769,7 +769,7 @@ let tr_goal gl = hyps, c -type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy | CVC3 +type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy | CVC3 | Z3 let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ()) @@ -808,6 +808,20 @@ let timeout_or_failure c cmd out = Failure (sprintf "command %s failed with output:\n%s " cmd (file_contents out)) +let call_prover ?(opt="") file = + if !debug then Format.eprintf "calling prover on %s@." file; + let out = Filename.temp_file "out" "" in + let cmd = + sprintf "why-dp -timeout %d -batch %s > %s 2>&1" !timeout file out in + match Sys.command cmd with + 0 -> Valid None + | 1 -> Failure (sprintf "could not run why-dp\n%s" (file_contents out)) + | 2 -> Invalid + | 3 -> DontKnow + | 4 -> Timeout + | 5 -> Failure (sprintf "prover failed:\n%s" (file_contents out)) + | n -> Failure (sprintf "Unknown exit status of why-dp: %d" n) + let prelude_files = ref ([] : string list) let set_prelude l = prelude_files := l @@ -828,6 +842,7 @@ let call_simplify fwhy = in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in +(* let cmd = sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out" !timeout fsx @@ -836,6 +851,8 @@ let call_simplify fwhy = let r = if out = 0 then Valid None else if out = 1 then Invalid else Timeout in +*) + let r = call_prover fsx in if not !debug then remove_files [fwhy; fsx]; r @@ -843,36 +860,27 @@ let call_ergo fwhy = let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in - let ftrace = Filename.temp_file "ergo_trace" "" in + (*let ftrace = Filename.temp_file "ergo_trace" "" in*) + (*NB: why-dp can't handle -cctrace let cmd = if !trace then sprintf "alt-ergo -cctrace %s %s" ftrace fwhy + else sprintf "alt-ergo %s" fwhy - in - let ret,out = timeout_sys_command cmd in - let r = - if ret <> 0 then - timeout_or_failure ret cmd out - else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then - Valid (if !trace then Some ftrace else None) - else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then - DontKnow - else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then - Invalid - else - Failure ("command failed: " ^ cmd) - in - if not !debug then remove_files [fwhy; out]; + in*) + let r = call_prover fwhy in + if not !debug then remove_files [fwhy; (*out*)]; r let call_zenon fwhy = let cmd = - sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy) + sprintf "why --no-zenon-prelude --zenon %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in +(* why-dp won't let us having coqterm... let out = Filename.temp_file "dp_out" "" in let cmd = sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out @@ -888,7 +896,23 @@ let call_zenon fwhy = let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in if c = 0 then Valid (Some out) else Invalid end + *) + let r = call_prover fznn in + if not !debug then remove_files [fwhy; fznn]; + r + +let call_smt ~smt fwhy = + let cmd = + sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in + let opt = "-smt-solver " ^ smt in + let r = call_prover ~opt fsmt in + if not !debug then remove_files [fwhy; fsmt]; + r +(* let call_yices fwhy = let cmd = sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) @@ -922,6 +946,7 @@ let call_cvc3 fwhy = in if not !debug then remove_files [fwhy; fsmt]; r +*) let call_cvcl fwhy = let cmd = @@ -929,6 +954,7 @@ let call_cvcl fwhy = in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in +(* let cmd = sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out" !timeout fcvc @@ -937,6 +963,8 @@ let call_cvcl fwhy = let r = if out = 0 then Valid None else if out = 1 then Invalid else Timeout in +*) + let r = call_prover fcvc in if not !debug then remove_files [fwhy; fcvc]; r @@ -946,6 +974,7 @@ let call_harvey fwhy = in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in +(* let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed"); let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in @@ -964,6 +993,9 @@ let call_harvey fwhy = if Sys.command cmd = 0 then Valid None else Invalid in if not !debug then remove_files [fwhy; frv; outf]; +*) + let r = call_prover frv in + if not !debug then remove_files [fwhy; frv]; r let call_gwhy fwhy = @@ -991,8 +1023,9 @@ let call_prover prover q = match prover with | Simplify -> call_simplify fwhy | Ergo -> call_ergo fwhy - | CVC3 -> call_cvc3 fwhy - | Yices -> call_yices fwhy + | CVC3 -> call_smt ~smt:"cvc3" fwhy + | Yices -> call_smt ~smt:"yices" fwhy + | Z3 -> call_smt ~smt:"z3" fwhy | Zenon -> call_zenon fwhy | CVCLite -> call_cvcl fwhy | Harvey -> call_harvey fwhy @@ -1022,6 +1055,7 @@ let simplify = tclTHEN intros (dp Simplify) let ergo = tclTHEN intros (dp Ergo) let cvc3 = tclTHEN intros (dp CVC3) let yices = tclTHEN intros (dp Yices) +let z3 = tclTHEN intros (dp Z3) let cvc_lite = tclTHEN intros (dp CVCLite) let harvey = dp Harvey let zenon = tclTHEN intros (dp Zenon) diff --git a/plugins/dp/dp.mli b/plugins/dp/dp.mli index 7c648ce6b..f40f86885 100644 --- a/plugins/dp/dp.mli +++ b/plugins/dp/dp.mli @@ -10,6 +10,7 @@ val cvc_lite : tactic val harvey : tactic val zenon : tactic val gwhy : tactic +val z3: tactic val dp_hint : reference list -> unit val dp_timeout : int -> unit @@ -17,5 +18,3 @@ val dp_debug : bool -> unit val dp_trace : bool -> unit val dp_prelude : string list -> unit val dp_predefined : reference -> string -> unit - - diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml index 4a1d70d41..9a62f39d0 100644 --- a/plugins/dp/dp_why.ml +++ b/plugins/dp/dp_why.ml @@ -48,6 +48,8 @@ let rec print_typ fmt = function | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x +let print_arg fmt (id,typ) = fprintf fmt "%a: %a" ident id print_typ typ + let rec print_term fmt = function | Cst n -> fprintf fmt "%s" (Big_int.string_of_big_int n) @@ -109,7 +111,30 @@ let rec print_predicate fmt p = | Exists (id, t, p) -> fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p +let rec remove_iff args = function + Forall (id,t,p) -> remove_iff ((id,t)::args) p + | Iff(_,b) -> List.rev args, b + | _ -> raise Not_found + let print_query fmt (decls,concl) = + let find_declared_preds l = + function + DeclPred (id,_,args) -> (id,args) :: l + | _ -> l + in + let find_defined_preds declared l = function + Axiom(id,f) -> + (try + let _decl = List.assoc id declared in + (id,remove_iff [] f)::l + with Not_found -> l) + | _ -> l + in + let declared_preds = + List.fold_left find_declared_preds [] decls in + let defined_preds = + List.fold_left (find_defined_preds declared_preds) [] decls + in let print_dtype = function | DeclType (id, 0) -> fprintf fmt "@[type %a@]@\n@\n" ident id @@ -130,15 +155,19 @@ let print_query fmt (decls,concl) = | DeclFun (id, _, l, t) -> fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" ident id (print_list comma print_typ) l print_typ t - | DeclPred (id, _, []) -> + | DeclPred (id, _, []) when not (List.mem_assoc id defined_preds) -> fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id - | DeclPred (id, _, l) -> + | DeclPred (id, _, l) when not (List.mem_assoc id defined_preds) -> fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" ident id (print_list comma print_typ) l - | DeclType _ | Axiom _ -> + | DeclType _ | Axiom _ | DeclPred _ -> () in let print_assert = function + | Axiom(id,_) when List.mem_assoc id defined_preds -> + let args, def = List.assoc id defined_preds in + fprintf fmt "@[predicate %a(%a) =@\n%a@]@\n" ident id + (print_list comma print_arg) args print_predicate def | Axiom (id, f) -> fprintf fmt "@[axiom %a:@ %a@]@\n@\n" ident id print_predicate f | DeclType _ | DeclFun _ | DeclPred _ -> @@ -155,5 +184,3 @@ let output_file f q = fprintf fmt "include \"real.why\"@."; fprintf fmt "@[%a@]@." print_query q; close_out c - - diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 index 505b07a14..82f86cd81 100644 --- a/plugins/dp/g_dp.ml4 +++ b/plugins/dp/g_dp.ml4 @@ -28,6 +28,10 @@ TACTIC EXTEND CVC3 [ "cvc3" ] -> [ cvc3 ] END +TACTIC EXTEND Z3 + [ "z3" ] -> [ z3 ] +END + TACTIC EXTEND CVCLite [ "cvcl" ] -> [ cvc_lite ] END -- cgit v1.2.3