mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
968 lines
26 KiB
Plaintext
968 lines
26 KiB
Plaintext
[ATP alt-ergo]
|
|
name = "Alt-Ergo"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.6\.[0-9]$"
|
|
command = "%e --timelimit %.t %f"
|
|
command_steps = "%e --steps-bound=%S %f"
|
|
driver = "alt_ergo_26"
|
|
use_at_auto_level = 1
|
|
|
|
[ATP alt-ergo-ce]
|
|
name = "Alt-Ergo"
|
|
alternative = "counterexamples"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.6\.[0-9]$"
|
|
command = "%e --produce-models --timelimit %.t %f"
|
|
command_steps = "%e --produce-models --steps-bound=%S %f"
|
|
driver = "alt_ergo_26_ce"
|
|
|
|
[ATP alt-ergo-bv]
|
|
name = "Alt-Ergo"
|
|
alternative = "BV"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.6\.[0-9]$"
|
|
command = "%e --timelimit %.t %f"
|
|
command_steps = "%e --steps-bound=%S %f"
|
|
driver = "alt_ergo_26_bv"
|
|
|
|
[ATP alt-ergo]
|
|
name = "Alt-Ergo"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.5\.[2-9]$"
|
|
version_bad = "^2\.5\.[0-1]$"
|
|
command = "%e --frontend dolmen --timelimit %.t %f"
|
|
command_steps = "%e --frontend dolmen --steps-bound=%S %f"
|
|
driver = "alt_ergo_smt"
|
|
use_at_auto_level = 1
|
|
|
|
[ATP alt-ergo-fpa]
|
|
name = "Alt-Ergo"
|
|
alternative = "FPA"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.5\.[4-9]$"
|
|
version_bad = "^2\.5\.[0-3]$"
|
|
command = "%e --frontend dolmen --enable-theories fpa --timelimit %.t %f"
|
|
command_steps = "%e --frontend dolmen --enable-theories fpa --steps-bound=%S %f"
|
|
driver = "alt_ergo_smt"
|
|
|
|
[ATP alt-ergo-ce]
|
|
name = "Alt-Ergo"
|
|
alternative = "counterexamples"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^v?\\([0-9.]+\\)$"
|
|
version_ok = "^2\.5\.[2-9]$"
|
|
version_bad = "^2\.5\.[0-1]$"
|
|
command = "%e --frontend dolmen --produce-models --timelimit %.t %f"
|
|
command_steps = "%e --frontend dolmen --produce-models --steps-bound=%S %f"
|
|
driver = "alt_ergo_counterexamples"
|
|
|
|
[ATP alt-ergo]
|
|
name = "Alt-Ergo"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^\\([0-9.]+\\)$"
|
|
version_ok = "^2\.4\.[0-3]$"
|
|
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-fpa]
|
|
name = "Alt-Ergo"
|
|
alternative = "FPA"
|
|
exec = "alt-ergo"
|
|
version_switch = "--version"
|
|
version_regexp = "^\\([0-9.]+\\)$"
|
|
version_ok = "^2\.4\.[0-3]$"
|
|
command = "%e --use-fpa --prelude=fpa-theory-2019-06-14-11h00.ae --timelimit %.t %f"
|
|
command_steps = "%e --use-fpa --prelude=fpa-theory-2019-06-14-11h00.ae --steps-bound=%S %f"
|
|
driver = "alt_ergo_fp"
|
|
editor = "altgr-ergo"
|
|
|
|
[ATP alt-ergo]
|
|
name = "Alt-Ergo"
|
|
exec = "alt-ergo"
|
|
version_switch = "-version"
|
|
version_regexp = "^\\([0-9.]+\\)$"
|
|
version_ok = "2.3.0"
|
|
version_ok = "2.3.1"
|
|
version_ok = "2.3.2"
|
|
version_ok = "2.3.3"
|
|
command = "%e -timelimit %t %f"
|
|
command_steps = "%e -steps-bound %S %f"
|
|
driver = "alt_ergo_2_3"
|
|
editor = "altgr-ergo"
|
|
use_at_auto_level = 1
|
|
|
|
[ATP alt-ergo]
|
|
name = "Alt-Ergo"
|
|
exec = "alt-ergo"
|
|
version_switch = "-version"
|
|
version_regexp = "^\\([0-9.]+\\)$"
|
|
version_ok = "2.2.0"
|
|
version_ok = "2.1.0"
|
|
version_ok = "2.0.0"
|
|
version_bad = "1.30"
|
|
version_bad = "1.01"
|
|
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_2_2_0"
|
|
editor = "altgr-ergo"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC5 versions 1.0 to 1.2, with strings and counterexamples
|
|
[ATP cvc5-strings-ce]
|
|
name = "CVC5"
|
|
alternative = "strings+counterexamples"
|
|
exec = "cvc5"
|
|
version_switch = "--version"
|
|
version_regexp = "This is cvc5 version \\([^ \n\r]+\\)"
|
|
version_ok = "^1\.[0-2]\.[0-9]+$"
|
|
driver = "cvc5_strings_counterexample"
|
|
command = "%e --stats-internal --tlimit-per=%T --strings-exp %f"
|
|
command_steps = "%e --stats-internal --rlimit=%S --strings-exp %f"
|
|
|
|
# CVC5 versions 1.0 to 1.2, with strings
|
|
[ATP cvc5-strings]
|
|
name = "CVC5"
|
|
alternative = "strings"
|
|
exec = "cvc5"
|
|
version_switch = "--version"
|
|
version_regexp = "This is cvc5 version \\([^ \n\r]+\\)"
|
|
version_ok = "^1\.[0-2]\.[0-9]+$"
|
|
driver = "cvc5_strings"
|
|
command = "%e --stats-internal --tlimit-per=%T --strings-exp %f"
|
|
command_steps = "%e --stats-internal --rlimit=%S --strings-exp %f"
|
|
|
|
# CVC5 versions 1.0 to 1.2, with counterexamples
|
|
[ATP cvc5-ce]
|
|
name = "CVC5"
|
|
alternative = "counterexamples"
|
|
exec = "cvc5"
|
|
version_switch = "--version"
|
|
version_regexp = "This is cvc5 version \\([^ \n\r]+\\)"
|
|
version_ok = "^1\.[0-2]\.[0-9]+$"
|
|
driver = "cvc5_counterexample"
|
|
command = "%e --stats-internal --tlimit-per=%T %f"
|
|
command_steps = "%e --stats-internal --rlimit=%S %f"
|
|
|
|
# CVC5 versions 1.0 to 1.2
|
|
[ATP cvc5]
|
|
name = "CVC5"
|
|
exec = "cvc5"
|
|
version_switch = "--version"
|
|
version_regexp = "This is cvc5 version \\([^ \n\r]+\\)"
|
|
version_ok = "^1\.[0-2]\.[0-9]+$"
|
|
driver = "cvc5"
|
|
command = "%e --stats-internal --tlimit=%T %f"
|
|
command_steps = "%e --stats-internal --rlimit=%S %f"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC4 version >= 1.8, with strings and counterexamples
|
|
[ATP cvc4-strings-ce]
|
|
name = "CVC4"
|
|
alternative = "strings+counterexamples"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.8"
|
|
driver = "cvc4_18_strings_counterexample"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit-per=%T --lang=smt2 --strings-exp %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 --strings-exp %f"
|
|
|
|
# CVC4 version >= 1.8, with strings
|
|
[ATP cvc4-strings]
|
|
name = "CVC4"
|
|
alternative = "strings"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.8"
|
|
driver = "cvc4_18_strings"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit=%T --lang=smt2 --strings-exp %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 --strings-exp %f"
|
|
|
|
# CVC4 version >= 1.7, with counterexamples
|
|
[ATP cvc4-ce]
|
|
name = "CVC4"
|
|
alternative = "counterexamples"
|
|
exec = "cvc4"
|
|
exec = "cvc4-1.7"
|
|
exec = "cvc4-1.8"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.7"
|
|
version_ok = "1.8"
|
|
driver = "cvc4_17_counterexample"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit-per=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
|
|
# CVC4 version >= 1.7
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.7"
|
|
version_ok = "1.8"
|
|
driver = "cvc4_17"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC4 version 1.6, with counterexamples
|
|
[ATP cvc4-ce]
|
|
name = "CVC4"
|
|
alternative = "counterexamples"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.6"
|
|
driver = "cvc4_16_counterexample"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit-per=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
|
|
# CVC4 version 1.6
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.6"
|
|
driver = "cvc4_16"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC4 version = 1.5, with counterexamples
|
|
[ATP cvc4-ce]
|
|
name = "CVC4"
|
|
alternative = "counterexamples"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.5"
|
|
driver = "cvc4_15_counterexample"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit-per=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
|
|
# CVC4 version 1.5
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_ok = "1.5"
|
|
driver = "cvc4_15"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
command = "%e --stats --tlimit=%T --lang=smt2 %f"
|
|
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_old = "1.4"
|
|
driver = "cvc4_14"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
|
|
# cvc4 1.4 does not print steps used in --stats anyway
|
|
command = "%e --tlimit=%T --lang=smt2 %f"
|
|
use_at_auto_level = 1
|
|
|
|
# CVC4 version 1.4, not using SMTLIB bitvectors
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
alternative = "noBV"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_old = "1.4"
|
|
driver = "cvc4"
|
|
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
|
|
# to try: --inst-when=full-last-call
|
|
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
|
|
# cvc4 1.4 does not print steps used in --stats anyway
|
|
command = "%e --tlimit=%T --lang=smt2 %f"
|
|
|
|
|
|
# CVC4 version 1.0 to 1.3
|
|
[ATP cvc4]
|
|
name = "CVC4"
|
|
exec = "cvc4"
|
|
version_switch = "--version"
|
|
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
|
|
version_old = "1.3"
|
|
version_old = "1.2"
|
|
version_old = "1.1"
|
|
version_old = "1.0"
|
|
driver = "cvc4"
|
|
command = "%e --lang=smt2 %f"
|
|
|
|
|
|
# COLIBRI with counterexamples
|
|
[ATP colibri-ce]
|
|
name = "COLIBRI"
|
|
alternative = "counterexamples"
|
|
exec = "colibri"
|
|
version_switch = "--version"
|
|
version_regexp = "\\([^ \n\r]+\\)"
|
|
version_ok = "2020.9"
|
|
driver = "colibri"
|
|
command = "%e --get-steps --memlimit %m %f"
|
|
command_steps = "%e --get-steps --max-steps %S --memlimit %m %f"
|
|
|
|
# COLIBRI
|
|
[ATP colibri]
|
|
name = "COLIBRI"
|
|
exec = "colibri"
|
|
version_switch = "--version"
|
|
version_regexp = "\\([^ \n\r]+\\)"
|
|
version_ok = "2020.9"
|
|
driver = "colibri"
|
|
command = "%e --get-steps --memlimit %m %f"
|
|
command_steps = "%e --get-steps --max-steps %S --memlimit %m %f"
|
|
|
|
# COLIBRI2
|
|
[ATP colibri2]
|
|
name = "Colibri2"
|
|
exec = "colibri2"
|
|
version_switch = "--version"
|
|
version_regexp = "\\([^ \n\r]+\\)"
|
|
version_ok = "0.4"
|
|
version_bad = "0.3.3"
|
|
version_bad = "0.2"
|
|
version_bad = "0.1"
|
|
driver = "colibri2"
|
|
command = "%e --time=%ts --size=%mM --show-steps %f"
|
|
command_steps = "%e --time=%ts --size=%mM --show-steps --max-steps %S %f"
|
|
|
|
# dReal
|
|
[ATP dreal]
|
|
name = "dreal"
|
|
exec = "dreal"
|
|
version_switch = "--version"
|
|
version_regexp = "dReal v\\([0-9.]+\\)"
|
|
version_ok = "4.21.06.1"
|
|
version_ok = "4.21.06.2"
|
|
command = "%e %f"
|
|
command_steps = "%e %f"
|
|
driver = "dreal"
|
|
|
|
# Psyche version 2.x
|
|
[ATP psyche]
|
|
name = "Psyche"
|
|
exec = "psyche"
|
|
version_switch = "-version"
|
|
version_regexp = "\\([^ \n\r]+\\)"
|
|
version_ok = "2.0"
|
|
driver = "psyche"
|
|
command = "%e -gplugin dpll_wl %f"
|
|
|
|
# CVC3 versions 2.4.x
|
|
[ATP cvc3]
|
|
name = "CVC3"
|
|
exec = "cvc3"
|
|
exec = "cvc3-2.4.1"
|
|
exec = "cvc3-2.4"
|
|
version_switch = "-version"
|
|
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
|
|
version_ok = "2.4.1"
|
|
version_old = "2.4"
|
|
# the -timeout option is unreliable in CVC3 2.4.1
|
|
command = "%e -seed 42 %f"
|
|
driver = "cvc3"
|
|
|
|
# CVC3 versions 2.x
|
|
[ATP cvc3]
|
|
name = "CVC3"
|
|
exec = "cvc3"
|
|
version_switch = "-version"
|
|
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
|
|
version_old = "2.2"
|
|
version_old = "2.1"
|
|
command = "%e -seed 42 -timeout %t %f"
|
|
driver = "cvc3"
|
|
|
|
[ATP yices]
|
|
name = "Yices"
|
|
exec = "yices"
|
|
version_switch = "--version"
|
|
version_regexp = "\\([^ \n]+\\)"
|
|
version_ok = "1.0.38"
|
|
version_old = "^1\.0\.3[0-7]$"
|
|
version_old = "^1\.0\.2[5-9]$"
|
|
version_old = "^1\.0\.2[0-4]$"
|
|
version_old = "^1\.0\.1\.*$"
|
|
command = "%e"
|
|
driver = "yices"
|
|
|
|
[ATP yices-smt2]
|
|
name = "Yices"
|
|
exec = "yices-smt2"
|
|
version_switch = "--version"
|
|
version_regexp = "^Yices \\([^ \n]+\\)$"
|
|
version_ok = "2.3.0"
|
|
command = "%e"
|
|
driver = "yices-smt2"
|
|
|
|
[ATP eprover]
|
|
name = "Eprover"
|
|
exec = "eprover"
|
|
version_switch = "--version"
|
|
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
|
|
version_ok = "^3\.2\.5$"
|
|
version_ok = "^3\.[01]$"
|
|
command = "%e -s -R --cpu-limit=%t --tstp-in %f"
|
|
driver = "eprover"
|
|
use_at_auto_level = 2
|
|
|
|
[ATP eprover]
|
|
name = "Eprover"
|
|
exec = "eprover"
|
|
version_switch = "--version"
|
|
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
|
|
version_ok = "^2\.[0-6]$"
|
|
version_old = "1.9.1-001"
|
|
version_old = "1.9"
|
|
version_old = "1.8-001"
|
|
version_old = "1.7"
|
|
version_old = "1.6"
|
|
version_old = "1.5"
|
|
version_old = "1.4"
|
|
command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
|
|
driver = "eprover"
|
|
use_at_auto_level = 2
|
|
|
|
[ATP gappa]
|
|
name = "Gappa"
|
|
exec = "gappa"
|
|
version_switch = "--version"
|
|
version_regexp = "Gappa \\([^ \n]*\\)"
|
|
version_ok = "^1\.[0-4]\..+$"
|
|
version_old = "^0\.1[1-8]\..+$"
|
|
command = "%e -Eprecision=70"
|
|
driver = "gappa"
|
|
|
|
[ATP mathsat]
|
|
name = "MathSAT5"
|
|
exec = "mathsat"
|
|
version_switch = "-version"
|
|
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
|
|
version_ok = "5.2.2"
|
|
command = "%e -input=smt2 -model -random_seed=80"
|
|
driver = "mathsat"
|
|
|
|
[ATP simplify]
|
|
name = "Simplify"
|
|
exec = "Simplify"
|
|
exec = "simplify"
|
|
version_switch = "-version"
|
|
version_regexp = "Simplify version \\([^ \n,]+\\)"
|
|
version_old = "1.5.5"
|
|
version_old = "1.5.4"
|
|
command = "%e %f"
|
|
driver = "simplify"
|
|
|
|
[ATP metis]
|
|
name = "Metis"
|
|
exec = "metis"
|
|
version_switch = "-v"
|
|
version_regexp = "metis \\([^ \n,]+\\)"
|
|
version_ok = "2.3"
|
|
command = "%e --time-limit %t %f"
|
|
driver = "metis"
|
|
|
|
[ATP metitarski]
|
|
name = "MetiTarski"
|
|
exec = "metit"
|
|
version_switch = "-v"
|
|
version_regexp = "MetiTarski \\([^ \n,]+\\)"
|
|
version_ok = "2.4"
|
|
version_old = "2.2"
|
|
command = "%e --time %t %f"
|
|
driver = "metitarski"
|
|
|
|
[ATP polypaver]
|
|
name = "PolyPaver"
|
|
exec = "polypaver"
|
|
version_switch = "--version"
|
|
version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
|
|
version_ok = "0.3"
|
|
command = "%e -d 2 -m 10 --time=%t %f"
|
|
driver = "polypaver"
|
|
|
|
[ATP spass]
|
|
name = "Spass"
|
|
exec = "SPASS"
|
|
version_switch = " | grep 'SPASS V'"
|
|
version_regexp = "SPASS V \\([^ \n\t]+\\)"
|
|
version_ok = "^3.[79]$"
|
|
command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
|
|
driver = "spass"
|
|
use_at_auto_level = 2
|
|
|
|
[ATP spass]
|
|
name = "Spass"
|
|
exec = "SPASS"
|
|
version_switch = " | grep 'SPASS[^ \\n\\t]* V'"
|
|
version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)"
|
|
version_ok = "3.8ds"
|
|
command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
|
|
driver = "spass_types"
|
|
use_at_auto_level = 2
|
|
|
|
[ATP vampire]
|
|
name = "Vampire"
|
|
exec = "vampire"
|
|
version_switch = "--version"
|
|
version_regexp = "Vampire \\([0-9.]+\\)"
|
|
command = "%e --input_syntax smtlib2 --random_seed 42 -t %t"
|
|
driver = "vampire_4_5_1"
|
|
version_ok = "4.5.1"
|
|
|
|
[ATP vampire]
|
|
name = "Vampire"
|
|
exec = "vampire"
|
|
version_switch = "--version"
|
|
version_regexp = "Vampire \\([0-9.]+\\)"
|
|
command = "%e --input_syntax smtlib2 --random_seed 42 -t %t"
|
|
driver = "vampire_4_2_2"
|
|
version_ok = "4.2.2"
|
|
|
|
[ATP vampire]
|
|
name = "Vampire"
|
|
exec = "vampire"
|
|
version_switch = "--version"
|
|
version_regexp = "Vampire \\([0-9.]+\\)"
|
|
command = "%e -t %t"
|
|
driver = "vampire"
|
|
version_ok = "0.6"
|
|
|
|
[ATP princess]
|
|
name = "Princess"
|
|
exec = "princess"
|
|
# version_switch = "-h"
|
|
# version_regexp = "(CASC version \\([0-9-]+\\))"
|
|
version_regexp = "(release \\([0-9-]+\\))"
|
|
command = "%e -timeout=%t %f"
|
|
driver = "princess"
|
|
# version_ok = "2013-05-13"
|
|
version_ok = "2015-12-07"
|
|
|
|
[ATP beagle]
|
|
name = "Beagle"
|
|
exec = "beagle"
|
|
# version_switch = "-h"
|
|
version_regexp = "version \\([0-9.]+\\)"
|
|
command = "%e %f"
|
|
driver = "beagle"
|
|
version_ok = "0.4.1"
|
|
|
|
[ATP verit]
|
|
name = "veriT"
|
|
exec = "veriT"
|
|
version_switch = "--version"
|
|
version_regexp = "version \\([^ \n\r]+\\)"
|
|
command = "%e --disable-print-success %f"
|
|
driver = "verit"
|
|
version_ok = "201410"
|
|
|
|
[ATP verit]
|
|
name = "veriT"
|
|
exec = "veriT"
|
|
version_switch = "--version"
|
|
version_regexp = "version \\([^ \n\r]+\\)"
|
|
command = "%e --disable-print-success --enable-simp \
|
|
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
|
|
driver = "verit"
|
|
version_old = "201310"
|
|
|
|
# Z3 >= 4.8.7, option model_compress renamed to model.compact
|
|
[ATP z3-ce]
|
|
name = "Z3"
|
|
alternative = "counterexamples"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "^4\.14\.[0-9]+$"
|
|
version_ok = "^4\.13\.[0-9]+$"
|
|
version_ok = "^4\.12\.[0-9]+$"
|
|
version_ok = "^4\.11\.[0-9]+$"
|
|
version_ok = "^4\.10\.[0-9]+$"
|
|
version_ok = "^4\.9\.[0-9]+$"
|
|
version_ok = "^4\.8\.1[0-9]+$"
|
|
version_ok = "^4\.8\.[7-9]$"
|
|
driver = "z3_487_counterexample"
|
|
# -t sets the time limit per query
|
|
command = "%e -smt2 -t:%T sat.random_seed=42 model.compact=false nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 model.compact=false nlsat.randomize=false smt.random_seed=42 rlimit=%S -st %f"
|
|
|
|
# Z3 >= 4.8.0, with counterexamples and incremental usage
|
|
[ATP z3-ce]
|
|
name = "Z3"
|
|
alternative = "counterexamples"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.8.6"
|
|
version_ok = "4.8.5"
|
|
version_ok = "4.8.4"
|
|
version_ok = "4.8.3"
|
|
version_ok = "4.8.1"
|
|
version_ok = "4.8.0"
|
|
driver = "z3_471_counterexample"
|
|
# -t sets the time limit per query
|
|
command = "%e -smt2 -t:%T sat.random_seed=42 model_compress=false nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 model_compress=false nlsat.randomize=false smt.random_seed=42 rlimit=%S -st %f"
|
|
|
|
# Z3 = 4.7.1, with counterexamples and incremental usage
|
|
[ATP z3-ce]
|
|
name = "Z3"
|
|
alternative = "counterexamples"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.7.1"
|
|
driver = "z3_471_counterexample"
|
|
# -t sets the time limit per query
|
|
command = "%e -smt2 -t:%T sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 rlimit=%S -st %f"
|
|
|
|
# Z3 >= 4.6.0, with counterexamples and incremental usage
|
|
[ATP z3-ce]
|
|
name = "Z3"
|
|
alternative = "counterexamples"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.6.0"
|
|
version_ok = "4.5.0"
|
|
version_old = "4.4.1"
|
|
version_old = "4.4.0"
|
|
driver = "z3_440_counterexample"
|
|
# -t sets the time limit per query
|
|
command = "%e -smt2 -t:%T sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S -st %f"
|
|
|
|
# Z3 >= 4.8.7, with BV support
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "^4\.14\.[0-9]+$"
|
|
version_ok = "^4\.13\.[0-9]+$"
|
|
version_ok = "^4\.12\.[0-9]+$"
|
|
version_ok = "^4\.11\.[0-9]+$"
|
|
version_ok = "^4\.10\.[0-9]+$"
|
|
version_ok = "^4\.9\.[0-9]+$"
|
|
version_ok = "^4\.8\.1[0-9]+$"
|
|
version_ok = "^4\.8\.[7-9]$"
|
|
driver = "z3_487"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
|
|
use_at_auto_level = 1
|
|
|
|
# Z3 >= 4.7.1, with BV support
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.8.6"
|
|
version_ok = "4.8.5"
|
|
version_ok = "4.8.4"
|
|
version_ok = "4.8.3"
|
|
version_ok = "4.8.1"
|
|
version_ok = "4.8.0"
|
|
version_ok = "4.7.1"
|
|
driver = "z3_471"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
|
|
use_at_auto_level = 1
|
|
|
|
# Z3 >= 4.5.0, with BV support
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.6.0"
|
|
version_ok = "4.5.0"
|
|
driver = "z3_440"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
|
|
use_at_auto_level = 1
|
|
|
|
# Z3 = 4.4.0, with BV support
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "4.4.1"
|
|
version_old = "4.4.0"
|
|
driver = "z3_440"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
|
|
use_at_auto_level = 1
|
|
|
|
# Z3 >= 4.7.1, without BV support
|
|
[ATP z3-nobv]
|
|
name = "Z3"
|
|
alternative = "noBV"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "^4\.14\.[0-9]+$"
|
|
version_ok = "^4\.13\.[0-9]+$"
|
|
version_ok = "^4\.12\.[0-9]+$"
|
|
version_ok = "^4\.11\.[0-9]+$"
|
|
version_ok = "^4\.10\.[0-9]+$"
|
|
version_ok = "^4\.9\.[0-9]+$"
|
|
version_ok = "^4\.8\.1[0-9]+$"
|
|
version_ok = "^4\.8\.[7-9]$"
|
|
version_ok = "4.8.6"
|
|
version_ok = "4.8.5"
|
|
version_ok = "4.8.4"
|
|
version_ok = "4.8.3"
|
|
version_ok = "4.8.1"
|
|
version_ok = "4.8.0"
|
|
version_ok = "4.7.1"
|
|
driver = "z3_471_nobv"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 rlimit=%S %f"
|
|
|
|
# Z3 >= 4.4.0, without BV support
|
|
[ATP z3-nobv]
|
|
name = "Z3"
|
|
alternative = "noBV"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_ok = "4.6.0"
|
|
version_ok = "4.5.0"
|
|
version_old = "4.4.1"
|
|
version_old = "4.4.0"
|
|
driver = "z3_432"
|
|
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
|
|
|
|
# Z3 4.3.2 does not support option global option -rs anymore.
|
|
# use settings given by "z3 -p" instead
|
|
# Z3 4.3.2 supports Datatypes
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "4.3.2"
|
|
driver = "z3_432"
|
|
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
|
|
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
|
|
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "4.3.1"
|
|
version_old = "4.3.0"
|
|
version_old = "4.2"
|
|
version_old = "4.1.2"
|
|
version_old = "4.1.1"
|
|
version_old = "4.0"
|
|
driver = "z3"
|
|
command = "%e -smt2 -rs:42 %f"
|
|
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
exec = "z3-3.2"
|
|
exec = "z3-3.1"
|
|
exec = "z3-3.0"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "3.2"
|
|
version_old = "3.1"
|
|
version_old = "3.0"
|
|
driver = "z3"
|
|
# the -T is unreliable in Z3 3.2
|
|
command = "%e -smt2 -rs:42 %f"
|
|
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "^2\.2.+$"
|
|
version_old = "^2\.1[6-9]$"
|
|
driver = "z3"
|
|
command = "%e -smt2 -rs:42 \
|
|
PHASE_SELECTION=0 \
|
|
RESTART_STRATEGY=0 \
|
|
RESTART_FACTOR=1.5 \
|
|
QI_EAGER_THRESHOLD=100 \
|
|
ARITH_RANDOM_INITIAL_VALUE=true \
|
|
SORT_AND_OR=false \
|
|
CASE_SPLIT=3 \
|
|
DELAY_UNITS=true \
|
|
DELAY_UNITS_THRESHOLD=16 \
|
|
%f"
|
|
#Other Parameters given by Nikolaj Bjorner
|
|
#BV_REFLECT=true #arith?
|
|
#MODEL_PARTIAL=true
|
|
#MODEL_VALUE_COMPLETION=false
|
|
#MODEL_HIDE_UNUSED_PARTITIONS=false
|
|
#MODEL_V1=true
|
|
#ASYNC_COMMANDS=false
|
|
#NNF_SK_HACK=true
|
|
|
|
[ATP z3]
|
|
name = "Z3"
|
|
exec = "z3"
|
|
version_switch = "-version"
|
|
version_regexp = "Z3 version \\([^ \n\r]+\\)"
|
|
version_old = "^2\.1[0-5]$"
|
|
version_old = "^2\.[0-9]$"
|
|
version_old = "1.3"
|
|
command = "%e -smt %f"
|
|
driver = "z3_smtv1"
|
|
|
|
[ATP zenon]
|
|
name = "Zenon"
|
|
exec = "zenon"
|
|
version_switch = "-v"
|
|
version_regexp = "zenon version \\([^ \n\t]+\\)"
|
|
version_ok = "^0.8.[0-5]$"
|
|
version_ok = "0.7.1"
|
|
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
|
|
driver = "zenon"
|
|
|
|
[ATP zenon_modulo]
|
|
name = "Zenon Modulo"
|
|
exec = "zenon_modulo"
|
|
version_switch = "-v"
|
|
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
|
|
version_ok = "0.4.1"
|
|
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
|
|
driver = "zenon_modulo"
|
|
|
|
[ATP iprover]
|
|
name = "iProver"
|
|
exec = "iprover"
|
|
version_switch = " | grep iProver"
|
|
version_regexp = "iProver v\\([^ \n\t]+\\)"
|
|
version_ok = "0.8.1"
|
|
command = "%e --fof true --out_options none \
|
|
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
|
|
\"eprover --cnf --tstp-format \" %f"
|
|
driver = "iprover"
|
|
|
|
[ATP mathematica]
|
|
name = "Mathematica"
|
|
exec = "math"
|
|
version_switch = "-run \"Exit[]\""
|
|
version_regexp = "Mathematica \\([0-9.]+\\)"
|
|
version_ok = "9.0"
|
|
version_ok = "8.0"
|
|
version_ok = "7.0"
|
|
command = "%e -noprompt"
|
|
driver = "mathematica"
|
|
|
|
[ITP coq]
|
|
name = "Coq"
|
|
support_library = "%l/coq/version"
|
|
exec = "coqtop"
|
|
version_switch = "-v"
|
|
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
|
|
version_ok = "^8\.20\.[0-9]+$"
|
|
version_ok = "^8\.1[6-9]\.[0-9]+$"
|
|
version_bad = "^8\.1[0-5]\.[0-9]+$"
|
|
version_bad = "^8\.[7-9]\.[0-9]+$"
|
|
version_bad = "8.6.1"
|
|
version_bad = "8.6"
|
|
version_bad = "^8\.5pl[1-3]$"
|
|
version_bad = "8.5"
|
|
command = "%e -batch -R %l/coq Why3 -l %f"
|
|
driver = "coq"
|
|
editor = "coqide"
|
|
|
|
[ITP pvs]
|
|
name = "PVS"
|
|
support_library = "%l/pvs/version"
|
|
exec = "pvs"
|
|
version_switch = "-version"
|
|
version_regexp = "PVS Version \\([^ \n]+\\)"
|
|
version_ok = "6.0"
|
|
version_ok = "7.1"
|
|
version_bad = "^[0-5]\..+$"
|
|
command = "%l/why3-call-pvs %l/pvs proveit -f %f"
|
|
driver = "pvs"
|
|
in_place = true
|
|
editor = "pvs"
|
|
|
|
[ITP isabelle]
|
|
name = "Isabelle"
|
|
exec = "isabelle"
|
|
version_switch = "version"
|
|
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
|
|
version_ok = "2019"
|
|
version_ok = "2021-1"
|
|
version_ok = "2022"
|
|
version_bad = "2018"
|
|
command = "%e why3 -b %f"
|
|
driver = "isabelle"
|
|
in_place = true
|
|
editor = "isabelle-jedit"
|
|
|
|
[editor pvs]
|
|
name = "PVS"
|
|
command = "%l/why3-call-pvs %l/pvs pvs %f"
|
|
|
|
[editor coqide]
|
|
name = "CoqIDE"
|
|
command = "coqide -R %l/coq Why3 %f"
|
|
|
|
[editor proofgeneral-coq]
|
|
name = "Emacs/ProofGeneral/Coq"
|
|
command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
|
|
|
|
[editor isabelle-jedit]
|
|
name = "Isabelle/jEdit"
|
|
command = "isabelle why3 -i %f"
|