tactique yices

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9645 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 44 insertions, 17 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index a41997780..49d1c20d1 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -639,7 +639,7 @@ let tr_goal gl =
   hyps, c
 
 
-type prover = Simplify | Ergo | CVCLite | Harvey | Zenon
+type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon
 
 let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
 
@@ -692,8 +692,23 @@ let call_zenon fwhy =
     if c = 0 then Valid (Some out) else Invalid
   end
 
+let call_yices fwhy =
+  let cmd = sprintf "why -smtlib --encoding sstrat %s" fwhy in
+  if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+  let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
+  let cmd = 
+    sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out" 
+      !timeout fsmt
+  in
+  let out = Sys.command cmd in
+  let r = 
+    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+  in
+  if not !debug then remove_files [fwhy; fsmt];
+  r
+
 let call_cvcl fwhy =
-  let cmd = sprintf "why --cvcl %s" fwhy in
+  let cmd = sprintf "why --cvcl --encoding sstrat %s" 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 = 
@@ -738,6 +753,7 @@ let call_prover prover q =
   match prover with
     | Simplify -> call_simplify fwhy
     | Ergo -> call_ergo fwhy
+    | Yices -> call_yices fwhy
     | Zenon -> call_zenon fwhy
     | CVCLite -> call_cvcl fwhy
     | Harvey -> call_harvey fwhy
@@ -760,6 +776,7 @@ let dp prover gl =
 
 let simplify = tclTHEN intros (dp Simplify)
 let ergo = tclTHEN intros (dp Ergo)
+let yices = tclTHEN intros (dp Yices)
 let cvc_lite = tclTHEN intros (dp CVCLite)
 let harvey = dp Harvey
 let zenon = tclTHEN intros (dp Zenon)
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 5fa4a6d57..181df6b37 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -4,6 +4,7 @@ open Proof_type
 
 val simplify : tactic
 val ergo : tactic
+val yices : tactic
 val cvc_lite : tactic
 val harvey : tactic
 val zenon : tactic
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 1100d7dc1..46ae400d2 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -20,6 +20,10 @@ TACTIC EXTEND Ergo
   [ "ergo" ] -> [ ergo ]
 END
 
+TACTIC EXTEND Yices
+  [ "yices" ] -> [ yices ]
+END
+
 TACTIC EXTEND CVCLite
   [ "cvcl" ] -> [ cvc_lite ]
 END
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 26cb2823c..984d66c8f 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -2,13 +2,14 @@
 Require Import ZArith.
 Require Import Classical.
 
+Require Export zenon.
+
 (* First example with the 0 and the equality translated *)
 
 Goal 0 = 0.
 zenon.
 Qed.
 
-
 (* Examples in the Propositional Calculus
    and theory of equality *)
 
@@ -38,12 +39,13 @@ Goal ((((A -> C) -> A) -> A) -> C) -> C.
 zenon.
 Qed.
 
+Dp_debug.
 
 (* Arithmetic *)
 Open Scope Z_scope.
 
 Goal 1 + 1 = 2.
-simplify.
+yices.
 Qed.
 
 
@@ -57,13 +59,12 @@ Qed.
 
 Goal (forall (x y : Z), x = y) -> 0=1.
 try zenon.
+ergo.
 Qed.
 
 Goal forall (x: nat), (x + 0 = x)%nat.
 
-induction x0.
-zenon.
-zenon.
+induction x0; ergo.
 Qed.
 
 
@@ -105,7 +106,7 @@ Inductive even : Z -> Prop :=
    unlike CVC Lite *)
 
 Goal even 4.
-cvcl.
+ergo.
 Qed.
 
 
@@ -114,8 +115,7 @@ Definition skip_z (z : Z) (n : nat) := n.
 Definition skip_z1 := skip_z.
 
 Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
-
-zenon.
+yices.
 Qed.
 
 
@@ -132,7 +132,7 @@ Dp_hint add_S.
    unlike zenon *)
 
 Goal forall n : nat, add n 0 = n.
-induction n ; simplify.
+induction n ; yices.
 Qed.
 
 
@@ -142,8 +142,8 @@ Definition pred (n : nat) : nat := match n with
 end.
 
 Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
-
-zenon.
+yices.
+(*zenon.*)
 Qed.
 
 
@@ -155,7 +155,7 @@ end.
 
 Goal forall n : nat, plus n 0%nat = n.
 
-induction n; zenon.
+induction n; ergo.
 Qed.
 
 
@@ -171,8 +171,11 @@ with odd_b (n : nat) : bool := match n with
 end.
 
 Goal even_b (S (S O)) = true.
-
+ergo.
+(*
+simplify.
 zenon.
+*)
 Qed.
 
 
@@ -182,7 +185,8 @@ Parameter foo : Set.
 Parameter ff : nat -> foo -> foo -> nat.
 Parameter g : foo -> foo.
 Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
-zenon.
+yices.
+(*zenon.*)
 Qed.
 
 
@@ -192,7 +196,8 @@ Qed.
 Parameter poly_f : forall A:Set, A->A.
 
 Goal forall x:nat, poly_f nat x = poly_f nat x.
-zenon.
+ergo.
+(*zenon.*)
 Qed.