Commit 4f84af4d authored by MARCHE Claude's avatar MARCHE Claude

Dropped support for Alt-Ergo <= 0.92. Moved theory map.Map into common part.

parent 1586788e
......@@ -3,14 +3,20 @@
import "alt_ergo_common.drv"
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 wrongs semantics for negative arguments *)
(* 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"
......@@ -25,7 +31,9 @@ end
theory int.ComputerDivision
(* protection against wrongs semantics for negative arguments *)
(* 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"
......@@ -38,15 +46,6 @@ theory int.ComputerDivision
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
(*
Local Variables:
......
(* Driver for Alt-Ergo version <= 0.92 *)
import "alt_ergo_common.drv"
theory BuiltIn
meta "printer_option" "no_type_cast"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
......@@ -11,16 +11,6 @@ theory BuiltIn
meta "printer_option" "no_type_cast"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
(*
Local Variables:
mode: why
......
......@@ -12,16 +12,6 @@ theory BuiltIn
meta "printer_option" "no_type_cast"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
theory int.EuclideanDivision
(* protection against wrongs semantics for negative arguments *)
......
......@@ -167,3 +167,13 @@ theory algebra.AC
remove prop Comm.Comm
remove prop Assoc
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
......@@ -54,27 +54,6 @@ version_old = "0.93"
command = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_0.93.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.92.3"
exec = "alt-ergo-0.92.2"
exec = "alt-ergo-0.92.1"
exec = "alt-ergo-0.92"
exec = "alt-ergo-0.91"
exec = "alt-ergo-0.9"
exec = "alt-ergo-0.8"
exec = "ergo"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_old = "^0\.92\..+$"
version_old = "0.92"
version_old = "0.91"
version_old = "0.9"
version_old = "0.8"
command = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_0.92.drv"
# CVC4 version >= 1.4
[ATP cvc4]
name = "CVC4"
......
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