The proof session state is stored in an XML file named <dir>/why3session.xml, where <dir> is the directory of the project. The XML file follows the DTD given in share/why3session.dtd and reproduced below.
<!ELEMENT why3session (prover*, file*)> <!ATTLIST why3session shape_version CDATA #IMPLIED> <!ELEMENT prover EMPTY> <!ATTLIST prover id CDATA #REQUIRED> <!ATTLIST prover name CDATA #REQUIRED> <!ATTLIST prover version CDATA #REQUIRED> <!ATTLIST prover alternative CDATA #IMPLIED> <!ATTLIST prover timelimit CDATA #IMPLIED> <!ATTLIST prover memlimit CDATA #IMPLIED> <!ATTLIST prover steplimit CDATA #IMPLIED> <!ELEMENT file (path*, theory*)> <!ATTLIST file name CDATA #IMPLIED> <!ATTLIST file verified CDATA #IMPLIED> <!ATTLIST file proved CDATA #IMPLIED> <!ELEMENT path EMPTY> <!ATTLIST path name CDATA #REQUIRED> <!ELEMENT theory (label*,goal*)> <!ATTLIST theory name CDATA #REQUIRED> <!ATTLIST theory verified CDATA #IMPLIED> <!ATTLIST theory proved CDATA #IMPLIED> <!ELEMENT goal (label*, proof*, transf*)> <!ATTLIST goal name CDATA #REQUIRED> <!ATTLIST goal expl CDATA #IMPLIED> <!ATTLIST goal sum CDATA #IMPLIED> <!ATTLIST goal shape CDATA #IMPLIED> <!ATTLIST goal proved CDATA #IMPLIED> <!ELEMENT proof (result|undone|internalfailure|unedited)> <!ATTLIST proof prover CDATA #REQUIRED> <!ATTLIST proof timelimit CDATA #IMPLIED> <!ATTLIST proof memlimit CDATA #IMPLIED> <!ATTLIST proof steplimit CDATA #IMPLIED> <!ATTLIST proof edited CDATA #IMPLIED> <!ATTLIST proof obsolete CDATA #IMPLIED> <!ELEMENT result EMPTY> <!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|steplimitexceeded|failure|highfailure) #REQUIRED> <!ATTLIST result time CDATA #IMPLIED> <!ATTLIST result steps CDATA #IMPLIED> <!ELEMENT undone EMPTY> <!ELEMENT unedited EMPTY> <!ELEMENT internalfailure EMPTY> <!ATTLIST internalfailure reason CDATA #REQUIRED> <!ELEMENT transf (goal*)> <!ATTLIST transf name CDATA #REQUIRED> <!ATTLIST transf proved CDATA #IMPLIED> <!ATTLIST transf arg1 CDATA #IMPLIED> <!ATTLIST transf arg2 CDATA #IMPLIED> <!ATTLIST transf arg3 CDATA #IMPLIED> <!ATTLIST transf arg4 CDATA #IMPLIED> <!ELEMENT label EMPTY> <!ATTLIST label name CDATA #REQUIRED> |
The data configuration for the automatic detection of
installed provers is stored in the file
provers-detection-data.conf typically located in directory
/usr/local/share/why3
after installation. The content of this
file is reproduced below.
[ATP alt-ergo] name = "Alt-Ergo" exec = "alt-ergo" exec = "alt-ergo-2.3.0" 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" 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" editor = "altgr-ergo" use_at_auto_level = 1 # CVC4 version >= 1.6, with counterexamples [ATP cvc4-ce] name = "CVC4" alternative = "counterexamples" exec = "cvc4" exec = "cvc4-1.6" exec = "cvc4-1.7" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.6" version_ok = "1.7" 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 --tlimit-per=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" # CVC4 version >= 1.6 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.6" exec = "cvc4-1.7" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.6" version_ok = "1.7" 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 --tlimit=%t000 --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" exec = "cvc4-1.5" 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 --tlimit-per=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" # CVC4 version 1.5 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.5" 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 --tlimit=%t000 --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" exec = "cvc4-1.4" 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=%t000 --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version 1.4, not using SMTLIB bitvectors [ATP cvc4] name = "CVC4" alternative = "noBV" exec = "cvc4" exec = "cvc4-1.4" 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=%t000 --lang=smt2 %f" # CVC4 version 1.0 to 1.3 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.3" exec = "cvc4-1.2" exec = "cvc4-1.1" exec = "cvc4-1.0" 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" # Psyche version 2.x [ATP psyche] name = "Psyche" exec = "psyche" exec = "psyche-2.02" 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" exec = "cvc3-2.2" exec = "cvc3-2.1" 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" exec = "yices-1.0.38" 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" exec = "yices-smt2-2.3.0" version_switch = "--version" version_regexp = "^Yices \\([^ \n]+\\)$" version_ok = "2.3.0" command = "%e" driver = "yices-smt2" [ATP eprover] name = "Eprover" exec = "eprover" exec = "eprover-2.0" exec = "eprover-1.9.1" exec = "eprover-1.9" exec = "eprover-1.8" exec = "eprover-1.7" exec = "eprover-1.6" exec = "eprover-1.5" exec = "eprover-1.4" version_switch = "--version" version_regexp = "E \\([-0-9.]+\\) [^\n]+" version_ok = "2.0" 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" exec = "gappa-1.3.2" exec = "gappa-1.3.0" exec = "gappa-1.2.2" exec = "gappa-1.2.0" exec = "gappa-1.1.1" exec = "gappa-1.1.0" exec = "gappa-1.0.0" exec = "gappa-0.16.1" exec = "gappa-0.14.1" version_switch = "--version" version_regexp = "Gappa \\([^ \n]*\\)" version_ok = "^1\.[0-3]\..+$" version_old = "^0\.1[1-8]\..+$" command = "%e -Eprecision=70" driver = "gappa" [ATP mathsat] name = "MathSAT5" exec = "mathsat" exec = "mathsat-5.2.2" 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" exec = "Simplify-1.5.4" exec = "Simplify-1.5.5" 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" exec = "metit-2.4" exec = "metit-2.2" 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" exec = "polypaver-0.3" 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" exec = "SPASS-3.7" version_switch = " | grep 'SPASS V'" version_regexp = "SPASS V \\([^ \n\t]+\\)" version_ok = "3.7" command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f" driver = "spass" use_at_auto_level = 2 [ATP spass] name = "Spass" exec = "SPASS" exec = "SPASS-3.8ds" 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" exec = "vampire-0.6" version_switch = "--version" version_regexp = "Vampire \\([0-9.]+\\)" command = "%e -t %t" driver = "vampire" version_ok = "0.6" [ATP princess] name = "Princess" exec = "princess" exec = "princess-2015-12-07" # 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" exec = "beagle-0.4.1" # version_switch = "-h" version_regexp = "version \\([0-9.]+\\)" command = "%e %f" driver = "beagle" version_ok = "0.4.1" [ATP verit] name = "veriT" exec = "veriT" exec = "veriT-201410" 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" exec = "veriT-201310" 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.6.0, with counterexamples and incremental usage [ATP z3-ce] name = "Z3" alternative = "counterexamples" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" 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.7.1" 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:%t000 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.4.0, with BV support [ATP z3] name = "Z3" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" 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.7.1" version_ok = "4.6.0" version_ok = "4.5.0" 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.4.0, without BV support [ATP z3-nobv] name = "Z3" alternative = "noBV" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" 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.7.1" 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-4.3.2" 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" exec = "z3-4.3.1" exec = "z3-4.3.0" exec = "z3-4.2" exec = "z3-4.1.2" exec = "z3-4.1.1" exec = "z3-4.0" 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" exec = "z3-2.19" exec = "z3-2.18" exec = "z3-2.17" exec = "z3-2.16" 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" exec = "z3-2.2" exec = "z3-2.1" exec = "z3-1.3" 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" exec = "zenon-0.8.0" exec = "zenon-0.7.1" version_switch = "-v" version_regexp = "zenon version \\([^ \n\t]+\\)" version_ok = "0.8.0" 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" exec = "iprover-0.8.1" 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\.9\.[0-1]$" version_ok = "^8\.8\.[0-2]$" version_ok = "^8\.7\.[0-2]$" version_ok = "8.6.1" version_ok = "8.6" version_old = "^8\.5pl[1-3]$" version_old = "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_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 = "2018" version_bad = "2017" version_bad = "2016-1" command = "%e why3 -b %f" driver = "isabelle2018" in_place = true editor = "isabelle-jedit" [ITP isabelle] name = "Isabelle" exec = "isabelle" version_switch = "version" version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)" version_ok = "2017" version_bad = "2018" version_bad = "2016-1" command = "%e why3 -b %f" driver = "isabelle2017" in_place = true editor = "isabelle-jedit" [editor pvs] name = "PVS" command = "%l/why3-call-pvs %l 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" [editor altgr-ergo] name = "AltGr-Ergo" command = "altgr-ergo %f" [shortcut shortcut1] name="Alt-Ergo" shortcut="altergo" |
One can use a custom configuration file. The Why3 tools look for it in the following order:
If none of these files exist, a built-in default configuration is used.
A section begins with a header inside square brackets and ends at the beginning of the next section. The header of a section can be a single identifier, e.g. [main], or it can be composed by a family name and a single family argument, e.g. [prover alt-ergo].
Sections contain associations key=value. A value is either an integer (e.g. -555), a boolean (true, false), or a string (e.g. "emacs"). Some specific keys can be attributed multiple values and are thus allowed to occur several times inside a given section. In that case, the relative order of these associations matters.
Drivers for external provers are readable files from directory drivers. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals.
[TO BE COMPLETED LATER]
This section documents the available transformations. We first describe the most important ones, and then we provide a quick documentation of the others, first the non-splitting ones, e.g. those which produce exactly one goal as result, and the others which produce any number of goals.
Notice that the set of available transformations in your own installation is given by
why3 --list-transforms
Those transformations generally amount to replace some applications of function or predicate symbols with its definition.
function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k) |
goal G: forall l: list 'a. length l >= 0 |
goal G : forall l:list 'a. match l with | Nil -> length l >= 0 | Cons a l1 -> length l1 >= 0 -> length l >= 0 end |
[@induction]
attribute can be used to
force induction over one particular variable, e.g. with
goal G: forall l1 [@induction] l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 |
l1
. If this attribute is attached to
several variables, a lexicographic induction is performed on these
variables, from left to right.These transformations simplify the goal by applying several kinds of simplification, described below. The transformations differ only by the kind of rules they apply:
The kinds of simplification are as follows.
true
and the transformations thus does not produce any sub-goal.
For example, a goal
like 6*7=42
is solved by those transformations.
inline_goal
. Transformation
compute_in_goal
unfolds all definitions, including recursive ones.
For compute_specified
, the user can enable unfolding of a specific
logic symbol by attaching the meta rewrite_def
to the symbol.
function sqr (x:int) : int = x * x meta "rewrite_def" function sqr |
axiom a: forall ... t1 = t2 |
axiom a: forall ... f1 <-> f2 |
meta "rewrite" prop a |
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the [@rewrite]
attribute on the axiom name or
on the axiom itself, e.g.:
axiom a [@rewrite]: forall ... t1 = t2 lemma b: [@rewrite] forall ... f1 <-> f2 |
The second form allows some form of local rewriting, e.g.
lemma l: forall x y. ([@rewrite] x = y) -> f x = f y |
can be proved by introduce_premises
followed by compute_specified
.
The computations performed by these transformations can take an arbitrarily large number of steps, or even not terminate. For this reason, the number of steps is bounded by a maximal value, which is set by default to 1000. This value can be increased by another meta, e.g.
meta "compute_max_steps" 1_000_000 |
When this upper limit is reached, a warning is issued, and the partly-reduced goal is returned as the result of the transformation.
Select_eq
of theory map.Map
.
function f : ... = ... g ... with g : ... = e |
function g : ... = e function f : ... = ... g ... |
forall x, x = t -> P(x) |
P(t) |
The transformation treats specially asymmetric and
by/so connectives. Asymmetric conjunction
A && B
in goal position is handled as syntactic sugar for
A /\ (A -> B)
. The conclusion of the first subgoal can then
be used to prove the second one.
Asymmetric disjunction A || B
in hypothesis position is handled as
syntactic sugar for A \/ ((not A) /\ B)
.
In particular, a case analysis on such hypothesis would give the negation of
the first hypothesis in the second case.
The by connective is treated as a proof indication. In
hypothesis position, A by B
is treated as if it were
syntactic sugar for its regular interpretation A
. In goal
position, it is treated as if B
was an intermediate step for
proving A
. A by B
is then replaced by B
and the
transformation also generates a side-condition subgoal B -> A
representing the logical cut.
Although splitting stops at disjunctive points like symmetric disjunction and left-hand sides of implications, the occurrences of the by connective are not restricted. For instance:
goal G : (A by B) && C |
goal G1 : B goal G2 : A -> C goal G3 : B -> A (* side-condition *) |
goal G : (A by B) \/ (C by D) |
goal G1 : B \/ D goal G2 : B -> A (* side-condition *) goal G3 : D -> C (* side-condition *) |
goal G : (A by B) || (C by D) |
goal G1 : B || D goal G2 : B -> A (* side-condition *) goal G3 : B || (D -> C) (* side-condition *) |
goal G : exists x. P x by x = 42 |
goal G1 : exists x. x = 42 goal G2 : forall x. x = 42 -> P x (* side-condition *) |
The so connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, A so B
is treated as if it were syntactic sugar for its regular interpretation A
. In hypothesis position, it is treated as if both A
and B
were true because B
is a consequence of A
. A so B
is replaced by A /\ B
and the transformation also generates a side-condition subgoal A -> B
corresponding to the consequence relation between formula.
As with the by connective, occurrences of so are unrestricted. For instance:
goal G : (((A so B) \/ C) -> D) && E |
goal G1 : ((A /\ B) \/ C) -> D goal G2 : (A \/ C -> D) -> E goal G3 : A -> B (* side-condition *) |
goal G : A by exists x. P x so Q x so R x by T x (* reads: A by (exists x. P x so (Q x so (R x by T x))) *) |
goal G1 : exists x. P x goal G2 : forall x. P x -> Q x (* side-condition *) goal G3 : forall x. P x -> Q x -> T x (* side-condition *) goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *) goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *) |
A
: There exists a x
for which P
holds. Then,
for that witness Q
and R
also holds. The last one holds
because T
holds as well. And from those three conditions on
x
, we can deduce A
.
The transformations in the split family can be controlled by using attributes on formulas.
The [@stop_split]
attribute can be used to block the splitting of a
formula. The attribute is removed after blocking, so applying the
transformation a second time will split the formula. This is can be
used to decompose the splitting process in several steps. Also, if a
formula with this attribute is found in non-goal position, its
by/so proof indication will be erased by the
transformation. In a sense, formulas tagged by [@stop_split]
are
handled as if they were local lemmas.
The [@case_split]
attribute can be used to force case analysis on hypotheses.
For instance, applying split_goal on
goal G : ([@case_split] A \/ B) -> C |
generates the subgoals
goal G1 : A -> C goal G2 : B -> C |
Without the attribute, the transformation does nothing because undesired case analysis may easily lead to an exponential blow-up.
Note that the precise behavior of splitting transformations in presence of
the [@case_split]
attribute is not yet specified
and is likely to change in future versions.
As seen in Section 5.3, the IDE provides a few buttons that trigger the run of simple proof strategies on the selected goals. Proof strategies can be defined using a basic assembly-style language, and put into the Why3 configuration file. The commands of this basic language are:
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the why3 config --detect
command
t split_goal_wp exit
c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000The three provers are tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. This is a perfect strategy for a first attempt to discharge a new goal.
start: c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000 t split_goal_wp start c Z3,4.5.0, 10 4000 c Alt-Ergo,1.30, 10 4000 c CVC4,1.5, 10 4000The three provers are first tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the provers are tried again with a larger limits.
start: c Z3,4.5.0, 1 1000 c Eprover,2.0, 1 1000 c Spass,3.7, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000 t split_goal_wp start c Z3,4.5.0, 5 2000 c Eprover,2.0, 5 2000 c Spass,3.7, 5 2000 c Alt-Ergo,1.30, 5 2000 c CVC4,1.5, 5 2000 t introduce_premises afterintro afterintro: t inline_goal afterinline g trylongertime afterinline: t split_goal_wp start trylongertime: c Z3,4.5.0, 30 4000 c Eprover,2.0, 30 4000 c Spass,3.7, 30 4000 c Alt-Ergo,1.30, 30 4000 c CVC4,1.5, 30 4000Notice that now 5 provers are used. The provers are first tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the prover are tried again with limits of 5 s and 2 Gb. If all fail, we attempt the transformation of introduction of premises in the context, followed by an inlining of the definitions in the goals. We then attempt a split again, if the split succeeds, we restart from the beginning, if it fails then provers are tried again with 30s and 4 Gb.