diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv index 1ea216f8b20c5c9c36254b91236e2ac9c53aa3ea..2ed721d5e3ef525fc9115c2b4ece47cd2585de2d 100644 --- a/drivers/alt_ergo.drv +++ b/drivers/alt_ergo.drv @@ -1,4 +1,22 @@ -(* 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" diff --git a/drivers/alt_ergo_2_2_0.drv b/drivers/alt_ergo_2_2_0.drv new file mode 100644 index 0000000000000000000000000000000000000000..98539f65c776cc1fc3d6a19b64750de20140904f --- /dev/null +++ b/drivers/alt_ergo_2_2_0.drv @@ -0,0 +1,25 @@ +(* 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$" diff --git a/drivers/alt_ergo_common.drv b/drivers/alt_ergo_common.drv index 6fda8759713dab49bc9e22fa73ab48bc066005d6..cea33a813bf7a20adfd8079d3ebd6fd81b8e15ef 100644 --- a/drivers/alt_ergo_common.drv +++ b/drivers/alt_ergo_common.drv @@ -1,7 +1,5 @@ (* 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" diff --git a/drivers/alt_ergo_fp.drv b/drivers/alt_ergo_fp.drv index a0512459fad4cfdd061c80a1da06e201bba22b24..bcb4f655ccc9eac25a2e47aa9259333d08549423 100644 --- a/drivers/alt_ergo_fp.drv +++ b/drivers/alt_ergo_fp.drv @@ -1,3 +1,18 @@ +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" diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index 20765bb7567092b2bf50f1b7995a712745e1ea9e..dfe4e2cac0dad45def601f3633edf633f426ff34 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -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