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

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 "@[<hov 2>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