Commit 76b65d70 authored by Clément Fumex's avatar Clément Fumex

Merge branch 'master' into new_float

parents 788027d2 0a6d4f21
......@@ -164,7 +164,12 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Why3_Bool.thy
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Int.thy
/lib/isabelle/Why3_List.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......@@ -207,6 +212,13 @@ pvsbin/
/plugins/tptp/tptp_parser.conflicts
/plugins/parser/dimacs.ml
# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
/plugins/python/py_parser.conflicts
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
......@@ -219,6 +231,8 @@ pvsbin/
/tests/test-and/
/tests/test-extraction/*
!/tests/test-extraction/main.ml
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz
# /examples/
/examples/in_progress/course/
......@@ -279,14 +293,18 @@ pvsbin/
/modules/pqueue/
/modules/mach/array/
/modules/mach/int/
/modules/python/
# Try Why3
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.map
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/alt_ergo_worker.map
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/why3_worker.map
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
......
......@@ -17,6 +17,7 @@ S plugins/parser
S plugins/printer
S plugins/transform
S plugins/tptp
S plugins/python
B src/util
B src/core
......@@ -37,6 +38,7 @@ B plugins/parser
B plugins/printer
B plugins/transform
B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
......@@ -8,6 +8,20 @@ Tools
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.3, January ??, 2017
=================================
bug fixes
o
Provers
o support for Alt-Ergo 1.30 (released ??, 2016)
o support for Coq 8.6 (released ?, 2016)
o support for Gappa 1.3 (released ?, 2016)
* discarded support for Isabelle 2015
o support for Isabelle 2016-1 (released Dec 2016)
o support for Z3 4.5.0 (released ? 2016)
Version 0.87.2, September 1, 2016
=================================
......
This diff is collapsed.
......@@ -176,8 +176,8 @@ OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION"
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.*|4.00.*)
AC_MSG_ERROR(You need Objective Caml 4.01.0 or higher);;
0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.[[0-2]])
AC_MSG_ERROR(You need Objective Caml 4.02.3 or higher);;
esac
# Ocaml library path
......@@ -522,11 +522,16 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.5*|trunk)
8.5*)
coq_compat_version="COQ85"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.6*|trunk)
coq_compat_version="COQ86"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
......@@ -638,9 +643,9 @@ else
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEDETECTEDVERSION in
2015*)
2016-1*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
ISABELLEVERSION=2016-1
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2016*)
......@@ -651,8 +656,8 @@ else
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2015)"
AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016)"
;;
esac
fi
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
You need version Isabelle2015 or Isabelle2016. Former versions are not
supported. We assume below that your version is 2016, please replace
2016 by 2015 otherwise.
You need version Isabelle2016 or Isabelle2016-1. Former versions are not
supported. We assume below that your version is 2016-1, please replace
2016-1 by 2016 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -22,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2016/etc/components
.isabelle/Isabelle2016-1/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
......@@ -209,9 +209,9 @@ Report any bug to the \why Bug Tracking System:
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, Leon Gondelman, Johannes Kanig, St\'ephane
Clochard, Simon Cruanes, L\'eon Gondelman, Johannes Kanig, St\'ephane
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
\cleardoublepage
......
......@@ -274,6 +274,18 @@ meta "rewrite" prop a
from left to right. Beware that there is no check for termination
nor for confluence of the set of rewrite rules declared.
\end{itemize}
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the label \verb|"rewrite"| on the axiom name or
on the axiom itself, e.g.:
\begin{whycode}
axiom a "rewrite": forall ... t1 = t2
lemma b: "rewrite" forall ... f1 <-> f2
\end{whycode}
The second form allows some form of local rewriting, e.g.
\begin{whycode}
lemma l: forall x y. ("rewrite" x = y) -> f x = f y
\end{whycode}
can be proved by \verb|introduce_premises| followed by \verb|"compute_specified"|.
\paragraph{Bound on the number of reductions}
The computations performed by these transformations can take an
......
......@@ -9,6 +9,7 @@ valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
timeout "^Timeout$"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
......@@ -19,13 +20,13 @@ steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -4,9 +4,9 @@ unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "eliminate_literal"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
......
......@@ -14,13 +14,12 @@ outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
timeout "self-timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -16,6 +16,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -27,6 +27,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -3,20 +3,20 @@
theory bv.BV64
syntax converter of_int "(_ bv%1 64)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV32
syntax converter of_int "(_ bv%1 32)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV16
syntax converter of_int "(_ bv%1 16)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV8
syntax converter of_int "(_ bv%1 8)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Fields.inverse_class.divide\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
......@@ -6,6 +6,7 @@ valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if_fmla"
transformation "eliminate_let_fmla"
......@@ -163,14 +164,15 @@ theory number.Gcd
syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
end
theory real.Real
syntax function zero "<number val=\"0\"><type name=\"Real.real\"/></number>"
syntax function one "<number val=\"1\"><type name=\"Real.real\"/></number>"
......
......@@ -7,4 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2015.gen"
import "isabelle-2016-1.gen"
......@@ -8,7 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2015.gen"
import "isabelle-2016-1.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -12,9 +12,7 @@ outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
......@@ -10,9 +10,7 @@ invalid "^NOT PROVABLE"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
......@@ -62,8 +62,10 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_uint_of_int
remove prop Of_int_zeros
remove prop Of_int_ones
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
(** Arithmetic operators *)
......
......@@ -48,8 +48,10 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop Of_int_zeros
remove prop Of_int_ones
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
remove prop to_uint_add
remove prop to_uint_add_bounded
......@@ -76,40 +78,60 @@ theory bv.BV_Gen
end
theory bv.BV64
meta "literal:keep" type t
syntax literal t "#x%16x"
syntax type t "(_ BitVec 64)"
syntax function zeros "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function one "#x0000000000000001"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function size_bv "(_ bv64 64)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end
theory bv.BV32
meta "literal:keep" type t
syntax literal t "#x%8x"
syntax type t "(_ BitVec 32)"
syntax function zeros "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function one "#x00000001"
syntax function ones "#xFFFFFFFF"
syntax function size_bv "(_ bv32 32)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end
theory bv.BV16
meta "literal:keep" type t
syntax literal t "#x%4x"
syntax type t "(_ BitVec 16)"
syntax function zeros "#x0000"
syntax function ones "#xFFFF"
syntax function one "#x0001"
syntax function ones "#xFFFF"
syntax function size_bv "(_ bv16 16)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end
theory bv.BV8
meta "literal:keep" type t
syntax literal t (* "#b%8b" *) "#x%2x"
syntax type t "(_ BitVec 8)"
syntax function zeros "#x00"
syntax function ones "#xFF"
syntax function one "#x01"
syntax function ones "#xFF"
syntax function size_bv "(_ bv8 8)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
......
......@@ -11,9 +11,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
(** Why3 driver for Z3 >= 4.3.2 *)
(* Do not set any logic, let z3 choose by itself
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
......@@ -7,7 +7,6 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "no-bv.gen"
import "discrimination.gen"
......@@ -23,6 +22,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -23,6 +23,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......@@ -81,7 +82,7 @@ end
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -89,7 +90,7 @@ end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -97,7 +98,7 @@ end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -105,7 +106,7 @@ end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"