Commit d56ea2e4 authored by François Bobot's avatar François Bobot

For Alt-Ergo <= 2.2.0 still rewrite let in formula

parent 5c6ca455
(* Driver for Alt-Ergo versions >= 0.95.2 *)
(* Driver for Alt-Ergo versions >= 2.3.0 *)
prelude "(* this is the prelude for Alt-Ergo, version >= 2.3.0 *)"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let_term"
transformation "split_premise_right"
transformation "simplify_formula"
import "alt_ergo_common.drv"
import "no-bv.gen"
......
(* Driver for Alt-Ergo versions >= 0.95.2 *)
prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 and <= 2.2.0 *)"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "split_premise_right"
transformation "simplify_formula"
import "alt_ergo_common.drv"
import "no-bv.gen"
(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"
(* Why drivers for Alt-Ergo: common part *)
prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)"
printer "alt-ergo"
filename "%f-%t-%g.why"
......@@ -20,21 +18,6 @@ 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"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let_term"
transformation "split_premise_right"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
syntax type int "int"
syntax type real "real"
......
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "split_premise_right"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
import "alt_ergo_common.drv"
import "no-bv.gen"
......
......@@ -2,12 +2,23 @@
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.3.0"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "2.3.0"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
use_at_auto_level = 1
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.2.0"
exec = "alt-ergo-2.1.0"
exec = "alt-ergo-2.0.0"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "2.3.0"
version_ok = "2.2.0"
version_ok = "2.1.0"
version_ok = "2.0.0"
......@@ -17,7 +28,7 @@ version_bad = "0.99.1"
version_bad = "0.95.2"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
driver = "alt_ergo_2_2_0"
editor = "altgr-ergo"
use_at_auto_level = 1
......
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