Commit 638a46fe authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Discarded support for Alt-Ergo < 0.95.2

parent 26dc2b1c
......@@ -12,6 +12,7 @@ Encodings
provers
o support for Isabelle 2015 (released May 25, 2015)
o support for Coq 8.4pl6 (released April 9, 2015)
o discarded support for Alt-Ergo versions older than 0.95.2
Version 0.86.1, May 22, 2015
============================
......
(* Driver for Alt-Ergo 0.93.
Differences wrt 0.92 are
- enumeration types
- maps
*)
import "alt_ergo_common.drv"
theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "printer_option" "no_type_cast"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
(* Driver for Alt-Ergo 0.94.
Differences wrt 0.93 are
- record types
- Euclidean division
*)
import "alt_ergo_common.drv"
theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "printer_option" "no_type_cast"
end
theory int.EuclideanDivision
(* protection against wrongs semantics for negative arguments *)
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 wrongs semantics for negative arguments *)
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:
*)
......@@ -16,67 +16,6 @@ command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95.1"
exec = "alt-ergo-0.95"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_old = "0.95.1"
version_old = "0.95"
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
# Alt-Ergo print steps but do not have an option to pass them for replay
command_steps = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.94"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_old = "0.94"
command = "%l/why3-cpulimit %t %m -s %e %f"
# Alt-Ergo print steps but do not have an option to pass them for replay
command_steps = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_0.94.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_old = "^0\.93\..+$"
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.5-prerelease
[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