From c56d7aaad742faa515035cfc333d3a951f668f96 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 11 Apr 2011 15:52:51 +0200 Subject: [PATCH] Alt-ergo has no input syntax for triggers on existential quantifiers --- CHANGES | 2 +- examples/programs/tortoise_hare.mlw | 73 +++++++++++++++++++++++++++++ src/printer/alt_ergo.ml | 8 ++-- 3 files changed, 79 insertions(+), 4 deletions(-) create mode 100644 examples/programs/tortoise_hare.mlw diff --git a/CHANGES b/CHANGES index 35f8d954e..5d67c0e45 100644 --- a/CHANGES +++ b/CHANGES @@ -1,7 +1,7 @@ * marks an incompatible change - + o fixed Alt-ergo output: no triggers for "exists" quantifier o [IDE] tool "Replay" works o [IDE] does not use Threads anymore, thanks to Call_provers.query_call o VC gen produces explanations in a suitable form for IDE diff --git a/examples/programs/tortoise_hare.mlw b/examples/programs/tortoise_hare.mlw new file mode 100644 index 000000000..605283352 --- /dev/null +++ b/examples/programs/tortoise_hare.mlw @@ -0,0 +1,73 @@ + +(* Floyd's ``the tortoise and the hare'' algorithm. *) + +module TortoiseHare + + use import int.Int + + (* We consider a function f over an abstract type t *) + + type t + + logic f t : t + + (* Given some x0 in t, we consider the sequence of the repeated calls + to f starting from x0. *) + + logic x int : t + + axiom xdef: forall n:int. n >= 0 -> x (n+1) = f (x n) + + logic x0 : t = x 0 + + (* If t is finite, this sequence will eventually end up on a cycle. + Let us simply assume the existence of this cycle, that is + x (i + lambda) = x i, for some lambda > 0 and i large enough. *) + + logic mu : int + axiom mu: mu >= 0 + + logic lambda : int + axiom lambda: lambda >= 1 + + axiom cycle: forall i:int. mu <= i -> x (i + lambda) = x i + + lemma cycle_gen: + forall i:int. mu <= i -> forall k:int. 0 <= k -> x (i + lambda * k) = x i + + (* The challenge is to prove that the recursive function + + let rec run x1 x2 = if x1 <> x2 then run (f x1) (f (f x2)) + + terminates when called on x0 and (f x0). + *) + + logic dist int int : int + + axiom dist_def1: + forall n m: int. 0 <= n <= m -> + x (n + dist n m) = x m + axiom dist_def2: + forall n m: int. 0 <= n <= m -> + forall k: int. x (n + k) = x m -> dist n m <= k + + logic r (x12 : (t, t)) (x'12 : (t, t)) = + let x1, x2 = x12 in + let x'1, x'2 = x'12 in + exists m:int. + x1 = x (m+1) and x2 = x (2*m+2) and x'1 = x m and x'2 = x (2*m) and + m < mu or (mu <= m and dist (m+1) (2*m+2) < dist m (2*m)) + + let rec run x1 x2 variant { (x1, x2) } with r = + { exists m:int [x m]. x1 = x m and x2 = x (2*m) } + if x1 <> x2 then + run (f x1) (f (f x2)) + { } + +end + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_hare.gui" +End: +*) diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index ee6428813..31887efdb 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -102,8 +102,11 @@ let rec print_fmla info fmt f = match f.f_node with (print_list comma (print_term info)) tl end | Fquant (q, fq) -> - let q = match q with Fforall -> "forall" | Fexists -> "exists" in let vl, tl, f = f_open_quant fq in + let q, tl = match q with + | Fforall -> "forall", tl + | Fexists -> "exists", [] (* Alt-ergo has no triggers for exists *) + in let forall fmt v = fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type info) v.vs_ty in @@ -141,8 +144,7 @@ and print_triggers info fmt tl = | Term _ -> true | Fmla {f_node = Fapp (ps,_)} -> not (ls_equal ps ps_equ) | _ -> false in - let tl = List.map (List.filter filter) - tl in + let tl = List.map (List.filter filter) tl in let tl = List.filter (function [] -> false | _::_ -> true) tl in if tl = [] then () else fprintf fmt "@ [%a]" (print_list alt (print_list comma (print_expr info))) tl -- GitLab