Previous Up Next

Chapter 9  Technical Informations

9.1  Structure of Session Files

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 (theory*)> <!ATTLIST file name CDATA #REQUIRED> <!ATTLIST file verified CDATA #IMPLIED> <!ATTLIST file proved CDATA #IMPLIED> <!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>

9.2  Prover Detection

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.2.0" exec = "alt-ergo-2.1.0" exec = "alt-ergo-2.0.0" 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" 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" 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 --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" 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 --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.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.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.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.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.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.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\.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"

9.3  The why3.conf Configuration File

One can use a custom configuration file. The Why3 tools look for it in the following order:

  1. the file specified by the -C or --config options,
  2. the file specified by the environment variable WHY3CONFIG if set,
  3. the file $HOME/.why3.conf ($USERPROFILE/.why3.conf under Windows) or, in the case of local installation, why3.conf in the top directory of Why3 sources.

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.

9.4  Drivers for External Provers

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]

9.5  Transformations

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

9.5.1  Inlining definitions

Those transformations generally amount to replace some applications of function or predicate symbols with its definition.

inline_trivial
expands and removes definitions of the form
function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k)
when each ei is either a ground term or one of the xj, and each x1xn occurs at most once in all the ei.
inline_goal
expands all outermost symbols of the goal that have a non-recursive definition.
inline_all
expands all non-recursive definitions.

9.5.2  Induction Transformations

induction_ty_lex
performs structural, lexicographic induction on goals involving universally quantified variables of algebraic data types, such as lists, trees, etc. For instance, it transforms the following goal
goal G: forall l: list 'a. length l >= 0
into this one:
goal G : forall l:list 'a. match l with | Nil -> length l >= 0 | Cons a l1 -> length l1 >= 0 -> length l >= 0 end
When induction can be applied to several variables, the transformation picks one heuristically. The [@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
induction will be applied on l1. If this attribute is attached to several variables, a lexicographic induction is performed on these variables, from left to right.

9.5.3  Simplification by Computation

These transformations simplify the goal by applying several kinds of simplification, described below. The transformations differ only by the kind of rules they apply:

compute_in_goal
aggressively applies all known computation/simplification rules.
compute_specified
performs rewriting using only built-in operators and user-provided rules.

The kinds of simplification are as follows.

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.

Bound on the number of reductions

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.

9.5.4  Other Non-Splitting Transformations

eliminate_algebraic
replaces algebraic data types by first-order definitions [10].
eliminate_builtin
removes definitions of symbols that are declared as builtin in the driver, i.e. with a “syntax” rule.
eliminate_definition_func
replaces all function definitions with axioms.
eliminate_definition_pred
replaces all predicate definitions with axioms.
eliminate_definition
applies both transformations above.
eliminate_mutual_recursion
replaces mutually recursive definitions with axioms.
eliminate_recursion
replaces all recursive definitions with axioms.
eliminate_if_term
replaces terms of the form if formula then t2 else t3 by lifting them at the level of formulas. This may introduce if then else in formulas.
eliminate_if_fmla
replaces formulas of the form if f1 then f2 else f3 by an equivalent formula using implications and other connectives.
eliminate_if
applies both transformations above.
eliminate_inductive
replaces inductive predicates by (incomplete) axiomatic definitions, i.e. construction axioms and an inversion axiom.
eliminate_let_fmla
eliminates let by substitution, at the predicate level.
eliminate_let_term
eliminates let by substitution, at the term level.
eliminate_let
applies both transformations above.
encoding_smt
encodes polymorphic types into monomorphic types [3].
encoding_tptp
encodes theories into unsorted logic.
introduce_premises
moves antecedents of implications and universal quantifications of the goal into the premises of the task.
simplify_array
automatically rewrites the task using the lemma Select_eq of theory map.Map.
simplify_formula
reduces trivial equalities t=t to true and then simplifies propositional structure: removes true, false, simplifies ff to f, etc.
simplify_recursive_definition
reduces mutually recursive definitions if they are not really mutually recursive, e.g.
function f : ... = ... g ... with g : ... = e
becomes
function g : ... = e function f : ... = ... g ...
if f does not occur in e.
simplify_trivial_quantification
simplifies quantifications of the form
forall x, x = t -> P(x)
into
P(t)
when x does not occur in t. More generally, this simplification is applied whenever x=t or t=x appears in negative position.
simplify_trivial_quantification_in_goal
is the same as above but it applies only in the goal.
split_premise
replaces axioms in conjunctive form by an equivalent collection of axioms. In absence of case analysis attributes (see split_goal for details), the number of axiom generated per initial axiom is linear in the size of that initial axiom.
split_premise_full
is similar to split_premise, but it also converts the axioms to conjunctive normal form. The number of axioms generated per initial axiom may be exponential in the size of the initial axiom.

9.5.5  Other Splitting Transformations

simplify_formula_and_task
is the same as simplify_formula but it also removes the goal if it is equivalent to true.
split_goal
changes conjunctive goals into the corresponding set of subgoals. In absence of case analysis attributes, the number of subgoals generated is linear in the size of the initial goal.
Behavior on asymmetric connectives and by/so

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:

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:

Attributes controlling the transformation

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.

split_all
performs both split_premise and split_goal.
split_intro
performs both split_goal and introduce_premises.
split_goal_full
has a behavior similar to split_goal, but also converts the goal to conjunctive normal form. The number of subgoals generated may be exponential in the size of the initial goal.
split_all_full
performs both split_premise and split_goal_full.

9.6  Proof Strategies

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

Split
is bound to the 1-line strategy
t split_goal_wp exit
Auto level 0
is bound to
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
The 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.
Auto level 1
is bound to
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 4000
The 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.
Auto level 2
is bound to
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 4000
Notice 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.

Previous Up Next