Previous Up Next

Chapter 10  Technical Informations

10.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 expanded CDATA #IMPLIED> <!ATTLIST file verified CDATA #IMPLIED> <!ELEMENT theory (label*,goal*)> <!ATTLIST theory name CDATA #REQUIRED> <!ATTLIST theory expanded CDATA #IMPLIED> <!ATTLIST theory verified CDATA #IMPLIED> <!ATTLIST theory sum CDATA #IMPLIED> <!ATTLIST theory locfile CDATA #IMPLIED> <!ATTLIST theory loclnum CDATA #IMPLIED> <!ATTLIST theory loccnumb CDATA #IMPLIED> <!ATTLIST theory loccnume CDATA #IMPLIED> <!ELEMENT goal (label*, proof*, transf*, metas*)> <!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> <!ATTLIST goal expanded CDATA #IMPLIED> <!ATTLIST goal locfile CDATA #IMPLIED> <!ATTLIST goal loclnum CDATA #IMPLIED> <!ATTLIST goal loccnumb CDATA #IMPLIED> <!ATTLIST goal loccnume 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> <!ATTLIST proof archived 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 expanded CDATA #IMPLIED> <!ATTLIST transf proved CDATA #IMPLIED> <!ELEMENT label EMPTY> <!ATTLIST label name CDATA #REQUIRED> <!ELEMENT metas (ts_pos*,ls_pos*,pr_pos*,meta*,goal)> <!ATTLIST metas expanded CDATA #IMPLIED> <!ATTLIST metas proved CDATA #IMPLIED> <!ELEMENT ts_pos (ip_library*,ip_qualid+)> <!ATTLIST ts_pos name CDATA #REQUIRED> <!ATTLIST ts_pos arity CDATA #REQUIRED> <!ATTLIST ts_pos id CDATA #REQUIRED> <!ATTLIST ts_pos ip_theory CDATA #REQUIRED> <!ELEMENT ls_pos (ip_library*,ip_qualid+)> <!ATTLIST ls_pos name CDATA #REQUIRED> <!ATTLIST ls_pos id CDATA #REQUIRED> <!ATTLIST ls_pos ip_theory CDATA #REQUIRED> <!ELEMENT pr_pos (ip_library*,ip_qualid+)> <!ATTLIST pr_pos name CDATA #REQUIRED> <!ATTLIST pr_pos id CDATA #REQUIRED> <!ATTLIST pr_pos ip_theory CDATA #REQUIRED> <!ELEMENT ip_library EMPTY> <!ATTLIST ip_library name CDATA #REQUIRED> <!ELEMENT ip_qualid EMPTY> <!ATTLIST ip_qualid name CDATA #REQUIRED> <!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*, meta_arg_pr*, meta_arg_str*, meta_arg_int*)> <!ATTLIST meta name CDATA #REQUIRED> <!ELEMENT meta_args_ty (ty_var|ty_app)> <!ELEMENT ty_var EMPTY> <!ATTLIST ty_var id CDATA #REQUIRED> <!ELEMENT ty_app (ty_var*,ty_app*)> <!ATTLIST ty_app id CDATA #REQUIRED> <!ELEMENT meta_arg_ts EMPTY> <!ATTLIST meta_arg_ts id CDATA #REQUIRED> <!ELEMENT meta_arg_ls EMPTY> <!ATTLIST meta_arg_ls id CDATA #REQUIRED> <!ELEMENT meta_arg_pr EMPTY> <!ATTLIST meta_arg_pr id CDATA #REQUIRED> <!ELEMENT meta_arg_str EMPTY> <!ATTLIST meta_arg_str val CDATA #REQUIRED> <!ELEMENT meta_arg_int EMPTY> <!ATTLIST meta_arg_int val CDATA #REQUIRED>

10.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-1.30" exec = "alt-ergo-1.20.prv" exec = "alt-ergo-1.10.prv" exec = "alt-ergo-1.01" exec = "alt-ergo-1.00.prv" version_switch = "-version" version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$" version_ok = "1.30" version_ok = "1.20.prv" version_ok = "1.10.prv" version_ok = "1.01" version_ok = "1.00.prv" # %T means timelimit+1 command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f" # %U means 2*timelimit+1 command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f" driver = "drivers/alt_ergo.drv" editor = "altgr-ergo" [ATP alt-ergo] name = "Alt-Ergo" exec = "alt-ergo" exec = "alt-ergo-0.99.1" exec = "alt-ergo-0.95.2" version_switch = "-version" version_regexp = "^\\([0-9.]+\\)$" version_ok = "0.99.1" version_ok = "0.95.2" # %T means timelimit+1 command = "%l/why3-cpulimit %T %m -s %e -no-rm-eq-existential -timelimit %t %f" # %U means 2*timelimit+1 command_steps = "%l/why3-cpulimit %U %m -s %e -no-rm-eq-existential -steps-bound %S %f" driver = "drivers/alt_ergo.drv" editor = "altgr-ergo" # CVC4 version 1.5-prerelease [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.5-prerelease" exec = "cvc4-1.5" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.5-prerelease" version_ok = "1.5" driver = "drivers/cvc4_15.drv" # --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f" command_steps = "%l/why3-cpulimit %U %m -s %e --stats --rlimit=%S --lang=smt2 %f" # 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_ok = "1.4" driver = "drivers/cvc4_14.drv" # --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 = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f" # 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_ok = "1.4" driver = "drivers/cvc4.drv" # --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 .14 does not print steps used in --stats anyway command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%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 = "drivers/cvc4.drv" command = "%l/why3-cpulimit %t %m -s %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 = "drivers/psyche.drv" command = "%l/why3-cpulimit %t %m -s %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 = "%l/why3-cpulimit %t %m -s %e -seed 42 %f" driver = "drivers/cvc3.drv" # 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 = "%l/why3-cpulimit %T %m -s %e -seed 42 -timeout %t %f" driver = "drivers/cvc3.drv" [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 = "%l/why3-cpulimit %t %m -s %e" driver = "drivers/yices.drv" [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 = "%l/why3-cpulimit %t %m -s %e" driver = "drivers/yices-smt2.drv" [ATP eprover] name = "Eprover" exec = "eprover" 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 = "1.8-001" version_old = "1.7" version_old = "1.6" version_old = "1.5" version_old = "1.4" command = "%l/why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f" driver = "drivers/eprover.drv" [ATP gappa] name = "Gappa" exec = "gappa" exec = "gappa-1.3.2" exec = "gappa-1.3.0" 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 = "%l/why3-cpulimit %t %m -s %e -Eprecision=70" driver = "drivers/gappa.drv" [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 = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f" driver = "drivers/mathsat.drv" [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 = "%l/why3-cpulimit %t %m -s %e %f" driver = "drivers/simplify.drv" [ATP metis] name = "Metis" exec = "metis" version_switch = "-v" version_regexp = "metis \\([^ \n,]+\\)" version_ok = "2.3" # %U means 2*timelimit+1. Required because Metis tends to # react very slowly to the time limit given, hence answers # oscillate between Timeout and Unknown command = "%l/why3-cpulimit %U %m -s %e --time-limit %t %f" driver = "drivers/metis.drv" [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 = "%l/why3-cpulimit %T %m -s %e --time %t %f" driver = "drivers/metitarski.drv" [ATP polypaver] name = "PolyPaver" exec = "polypaver" exec = "polypaver-0.3" version_switch = "--version" version_regexp = "PolyPaver \\([0-9.]+\\) (c)" version_ok = "0.3" command = "%l/why3-cpulimit %T %m -s %e -d 2 -m 10 --time=%t %f" driver = "drivers/polypaver.drv" [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 = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f" driver = "drivers/spass.drv" [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 = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f" driver = "drivers/spass_types.drv" [ATP vampire] name = "Vampire" exec = "vampire" exec = "vampire-0.6" version_switch = "--version" version_regexp = "Vampire \\([0-9.]+\\)" command = "%l/why3-cpulimit %T %m -s %e -t %t" driver = "drivers/vampire.drv" version_ok = "0.6" [ATP princess] name = "Princess" exec = "princess" # version_switch = "-h" version_regexp = "(CASC version \\([0-9-]+\\))" command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f" driver = "drivers/princess.drv" version_ok = "2013-05-13" [ATP beagle] name = "Beagle" exec = "beagle" exec = "beagle-0.4.1" # version_switch = "-h" version_regexp = "version \\([0-9.]+\\)" command = "%l/why3-cpulimit %t 0 -s %e %f" driver = "drivers/beagle.drv" version_ok = "0.4.1" [ATP verit] name = "veriT" exec = "veriT" exec = "veriT-201410" version_switch = "--version" version_regexp = "version \\([^ \n\r]+\\)" command = "%l/why3-cpulimit %t %m -s %e --disable-print-success %f" driver = "drivers/verit.drv" version_ok = "201410" [ATP verit] name = "veriT" exec = "veriT" exec = "veriT-201310" version_switch = "--version" version_regexp = "version \\([^ \n\r]+\\)" command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \ --enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f" driver = "drivers/verit.drv" version_old = "201310" # Z3 >= 4.4.0, with BV support [ATP z3] name = "Z3" exec = "z3" 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.5.0" version_ok = "4.4.1" version_ok = "4.4.0" driver = "drivers/z3_440.drv" command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" # Z3 >= 4.4.0, without BV support [ATP z3] name = "Z3" alternative = "noBV" exec = "z3" 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.5.0" version_ok = "4.4.1" version_ok = "4.4.0" driver = "drivers/z3_432.drv" command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%l/why3-cpulimit %U %m -s %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_ok = "4.3.2" driver = "drivers/z3_432.drv" command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%l/why3-cpulimit %U %m -s %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 = "drivers/z3.drv" command = "%l/why3-cpulimit %t %m -s %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 = "drivers/z3.drv" # the -T is unreliable in Z3 3.2 command = "%l/why3-cpulimit %t %m -s %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 = "drivers/z3.drv" command = "%l/why3-cpulimit %t %m -s %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 = "%l/why3-cpulimit %t %m -s %e -smt %f" driver = "drivers/z3_smtv1.drv" [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 = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f" driver = "drivers/zenon.drv" [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 = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f" driver = "drivers/zenon_modulo.drv" [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 = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \ --time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \ \"eprover --cnf --tstp-format \" %f" driver = "drivers/iprover.drv" [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 = "%l/why3-cpulimit %t %m -s %e -noprompt" driver = "drivers/mathematica.drv" # Coq 8.6: do not limit memory [ITP coq] name = "Coq" compile_time_support = true exec = "coqtop -batch" version_switch = "-v" version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" version_ok = "8.6" command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f" driver = "drivers/coq.drv" editor = "coqide" # Coq 8.5: do not limit memory [ITP coq] name = "Coq" compile_time_support = true exec = "coqtop -batch" version_switch = "-v" version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" version_ok = "8.5pl3" version_ok = "8.5pl2" version_ok = "8.5pl1" version_ok = "8.5" command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f" driver = "drivers/coq.drv" editor = "coqide" [ITP coq] name = "Coq" compile_time_support = true exec = "coqtop -batch" version_switch = "-v" version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" version_ok = "^8\.4pl[1-6]$" version_ok = "8.4" command = "%l/why3-cpulimit 0 %m -s %e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f" driver = "drivers/coq.drv" editor = "coqide" [ITP pvs] name = "PVS" compile_time_support = true exec = "pvs" version_switch = "-version" version_regexp = "PVS Version \\([^ \n]+\\)" version_ok = "6.0" version_bad = "^[0-5]\..+$" # not why3-cpulimit 0 %m because 'proveit' allocates 8Gb at start-up command = "%l/why3-cpulimit 0 0 -s %l/why3-call-pvs %l proveit -f %f" driver = "drivers/pvs.drv" in_place = true editor = "pvs" [ITP isabelle] name = "Isabelle" exec = "isabelle" version_switch = "version" version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)" version_ok = "2016-1" version_bad = "2016" version_bad = "2015" # not why3-cpulimit 0 %m because isabelle needs more memory at start-up command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f" driver = "drivers/isabelle2016-1.drv" in_place = true editor = "isabelle-jedit" [ITP isabelle] name = "Isabelle" exec = "isabelle" version_switch = "version" version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)" # not why3-cpulimit 0 %m because isabelle needs more memory at start-up command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f" version_ok = "2016" version_bad = "2016-1" version_bad = "2015" driver = "drivers/isabelle2016.drv" 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-tactic Why3 -R %l/coq Why3 %f" [editor proofgeneral-coq] name = "Emacs/ProofGeneral/Coq" command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq-tactic\\\" \\\"Why3\\\") \ (\\\"%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"

10.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.

The configuration file is a human-readable text file, which consists of association pairs arranged in sections. Below is an example of configuration file.

[main]
loadpath = "/usr/local/share/why3/theories"
loadpath = "/usr/local/share/why3/modules"
magic = 14
memlimit = 0
plugin = "/usr/local/lib/why3/plugins/tptp"
plugin = "/usr/local/lib/why3/plugins/genequlin"
plugin = "/usr/local/lib/why3/plugins/hypothesis_selection"
running_provers_max = 4
timelimit = 2

[ide]
default_editor = "editor %f"
error_color = "orange"
goal_color = "gold"
iconset = "fatcow"
intro_premises = true
premise_color = "chartreuse"
print_labels = false
print_locs = false
print_time_limit = false
saving_policy = 2
task_height = 404
tree_width = 512
verbose = 0
window_height = 1173
window_width = 1024

[prover]
command = "'why3-cpulimit' 0 %m -s coqtop -batch -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
in_place = false
interactive = true
name = "Coq"
shortcut = "coq"
version = "8.3pl4"

[prover]
command = "'why3-cpulimit' %t %m -s alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo_0.93.drv"
editor = ""
in_place = false
interactive = false
name = "Alt-Ergo"
shortcut = "altergo"
shortcut = "alt-ergo"
version = "0.93.1"

[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
name = "CoqIDE"

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 only one identifier, main and ide in the example, or it can be composed by a family name and one family argument, prover is one family name, coq and alt-ergo are the family argument.

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 matter.

10.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]

10.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

10.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.

10.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. A label "induction" 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 label is attached to several variables, a lexicographic induction is performed on these variables, from left to right.

10.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 label "rewrite" 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.

10.5.4  Other Non-Splitting Transformations

eliminate_algebraic
replaces algebraic data types by first-order definitions [7].
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 [2].
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 labels (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.

10.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 labels, 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:

Labels controlling the transformation

The transformations in the split family can be controlled by using labels on formulas.

The label "stop_split" can be used to block the splitting of a formula. The label 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 label 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 label "case_split" 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 label, 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" label 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.

Previous Up Next