Commit 0b4a16d7 authored by MARCHE Claude's avatar MARCHE Claude

attempt to support Yices2, but it does not support quantifiers

parent bda84f14
(* 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:
*)
......@@ -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"
......
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