diff --git a/drivers/yices-smt2.drv b/drivers/yices-smt2.drv new file mode 100644 index 0000000000000000000000000000000000000000..cd8284b0e94f1ce2e6877d0a8feb9351579be231 --- /dev/null +++ b/drivers/yices-smt2.drv @@ -0,0 +1,36 @@ +(* Why3 driver for Yices-smt2 solver *) + +prelude ";;; this is a prelude for Yices-smt2" +prelude "(set-logic AUFLIRA)" +(* A : Array + UF : Uninterpreted Function + LIRA : Linear Integer Reals Arithmetic +*) + +import "smt-libv2.drv" +import "discrimination.gen" + +(* specific messages from Yices-smt2 *) +unknown "feature not supported: non linear problem" "non linear arith" + +transformation "inline_trivial" + +transformation "eliminate_builtin" +transformation "eliminate_definition" +transformation "eliminate_inductive" +transformation "eliminate_algebraic" +transformation "eliminate_epsilon" + +transformation "simplify_formula" +(*transformation "simplify_trivial_quantification"*) + +transformation "encoding_smt" +transformation "encoding_sort" + + +(* +Local Variables: +mode: why3 +compile-command: "unset LANG; make -C .. bench" +End: +*) diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index 7921cd61fdc2c277994baf46bb2e33dd802f44cf..77c0cf949875ace2d5b2f40f5304b4dd078bc2ac 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -129,7 +129,7 @@ name = "Yices" exec = "yices" exec = "yices-1.0.38" version_switch = "--version" -version_regexp = "[Yices ]*\\([^ \n]+\\)" +version_regexp = "\\([^ \n]+\\)" version_ok = "1.0.38" version_old = "^1\.0\.3[0-7]$" version_old = "^1\.0\.2[5-9]$" @@ -138,15 +138,15 @@ version_old = "^1\.0\.1\.*$" command = "%l/why3-cpulimit %t %m -s %e" driver = "drivers/yices.drv" -[ATP yices2] -name = "Yices2" -exec = "yices" -exec = "yices-2.0.4" +[ATP yices-smt2] +name = "Yices" +exec = "yices-smt2" +exec = "yices-smt2-2.3.0" version_switch = "--version" -version_regexp = "[Yices ]*\\([^ \n]+\\)\." -version_ok = "^2\.0\.4" +version_regexp = "^Yices \\([^ \n]+\\)$" +version_ok = "2.3.0" command = "%l/why3-cpulimit %t %m -s %e" -driver = "drivers/yices.drv" +driver = "drivers/yices-smt2.drv" [ATP eprover] name = "Eprover"