diff options
Diffstat (limited to 'contrib/dp')
-rw-r--r-- | contrib/dp/dp.ml | 21 | ||||
-rw-r--r-- | contrib/dp/dp.mli | 1 | ||||
-rw-r--r-- | contrib/dp/g_dp.ml4 | 4 | ||||
-rw-r--r-- | contrib/dp/tests.v | 35 |
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. |