Commit 8f0d49d0 authored by Andrei Paskevich's avatar Andrei Paskevich

trywhy3: update the alt-ergo driver

parent 55c3f770
...@@ -8,26 +8,35 @@ printer "alt-ergo" ...@@ -8,26 +8,35 @@ printer "alt-ergo"
filename "%f-%t-%g.why" filename "%f-%t-%g.why"
(* Try Why3 doesn't need these (* Try Why3 doesn't need these
valid "Valid" valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "Invalid" invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "I don't know" "" unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "Timeout" timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
steplimitexceeded "Steps limit reached" timeout "^Timeout$"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
outofmemory "Fatal error: out of memory" outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow" outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1" fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "Valid (%s)"
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"
*) *)
(* FIXME: remaining of this file should be shared with regular Alt-Ergo driver *) (* FIXME: remaining of this file should be shared with regular Alt-Ergo driver *)
transformation "inline_trivial" transformation "inline_trivial"
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_recursion" transformation "eliminate_recursion"
transformation "eliminate_inductive" transformation "eliminate_inductive"
transformation "eliminate_algebraic" transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon" transformation "eliminate_epsilon"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "split_premise_right" transformation "split_premise_right"
transformation "simplify_formula" transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*) (*transformation "simplify_trivial_quantification_in_goal"*)
...@@ -37,6 +46,10 @@ theory BuiltIn ...@@ -37,6 +46,10 @@ theory BuiltIn
syntax type real "real" syntax type real "real"
syntax predicate (=) "(%1 = %2)" syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end end
theory int.Int theory int.Int
...@@ -82,6 +95,26 @@ theory int.Int ...@@ -82,6 +95,26 @@ theory int.Int
end end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory int.ComputerDivision
prelude "logic comp_div: int, int -> int"
prelude "axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y"
prelude "logic comp_mod: int, int -> int"
prelude "axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y"
syntax function div "comp_div(%1,%2)"
syntax function mod "comp_mod(%1,%2)"
end
theory real.Real theory real.Real
...@@ -175,56 +208,3 @@ theory map.Map ...@@ -175,56 +208,3 @@ theory map.Map
remove prop Select_eq remove prop Select_eq
remove prop Select_neq remove prop Select_neq
end end
theory BuiltIn
(* Alt-Ergo >= 0.95 supports enumerated datatypes and records *)
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.EuclideanDivision
(* protection against wrong semantics for negative arguments
last checked on 0.99.1: this is still needed
*)
prelude "logic safe_eucl_div: int, int -> int"
prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
prelude "logic safe_eucl_mod: int, int -> int"
prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
syntax function div "safe_eucl_div(%1,%2)"
syntax function mod "safe_eucl_mod(%1,%2)"
end
theory int.ComputerDivision
(* protection against wrong semantics for negative arguments
last checked on 0.99.1: this is still needed
*)
prelude "logic safe_comp_div: int, int -> int"
prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
prelude "logic safe_comp_mod: int, int -> int"
prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
syntax function div "safe_comp_div(%1,%2)"
syntax function mod "safe_comp_mod(%1,%2)"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment