Commit 6e3a01ae authored by David Hauzar's avatar David Hauzar

Merge commit '46e48687' into counter-examples

parents 74d2b385 46e48687
......@@ -256,7 +256,8 @@ pvsbin/
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
/examples/in_progress/prover/build/*__*.ml
/examples/in_progress/prover/.depend
# modules
/modules/string/
......
* marks an incompatible change
library
* improved bitvectors theories
Encodings
* When a task has no polymorphic object (except for the special
cases of equality and maps) then the translation to SMT-LIB
format is direct
provers
o support for Isabelle 2015 (released May 25, 2015)
o support for Coq 8.4pl6 (released April 9, 2015)
Version 0.86.1, May 22, 2015
============================
......
......@@ -120,11 +120,6 @@ CLEANDIRS =
CLEANLIBS =
GENERATED =
install_local::
ln -s -n -f ../drivers share/drivers
ln -s -n -f ../modules share/modules
ln -s -n -f ../theories share/theories
##############
# Why3 library
##############
......@@ -158,6 +153,7 @@ LIB_PARSER = ptree glob parser typing lexer
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
detect_polymorphism \
reduction_engine compute \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate encoding encoding_select \
......@@ -168,7 +164,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
reduction_engine compute induction_pr prop_curry
induction_pr prop_curry
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
......@@ -555,6 +551,17 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@
install_local:: share/drivers share/modules share/theories
share/drivers:
ln -snf ../drivers share/drivers
share/modules:
ln -snf ../modules share/modules
share/theories:
ln -snf ../theories share/theories
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(TOOLSDEP)
endif
......@@ -946,7 +953,7 @@ ifeq (@enable_coq_fp_libs@,yes)
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq headers-coq
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv headers-coq
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -1601,12 +1608,10 @@ MODULESTODOC = \
util/weakhtbl util/stdlib util/rc util/debug \
core/ident core/ty core/term core/decl core/theory \
core/env core/task \
driver/whyconf driver/driver \
driver/whyconf driver/call_provers driver/driver \
session/session session/session_tools session/session_scheduler \
whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
whyml/mlw_main
# transform/introduction \
# ide/db
whyml/mlw_wp
FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
......
theory BuiltIn
meta "select_inst" "goal"
meta "select_lskept" "goal"
meta "select_lsinst" "goal"
meta "select_kept" "all"
meta "select_inst_default" "goal"
meta "select_lskept_default" "goal"
meta "select_lsinst_default" "goal"
meta "select_kept_default" "all"
end
......@@ -5,7 +5,7 @@
printer "ocaml"
theory BuiltIn
syntax type int "Why3__BigInt.t"
syntax type int "Why3extract.Why3__BigInt.t"
syntax predicate (=) "(%1 = %2)"
end
......@@ -14,6 +14,7 @@ import "ocaml-no-arith.drv"
(* int *)
theory int.Int
prelude "open Why3extract"
syntax constant zero "Why3__BigInt.zero"
syntax constant one "Why3__BigInt.one"
......@@ -29,38 +30,46 @@ theory int.Int
end
theory int.Abs
prelude "open Why3extract"
syntax function abs "(Why3__BigInt.abs %1)"
end
theory int.MinMax
prelude "open Why3extract"
syntax function min "(Why3__BigInt.min %1 %2)"
syntax function max "(Why3__BigInt.max %1 %2)"
end
theory int.Lex2
prelude "open Why3extract"
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
theory int.EuclideanDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
end
theory int.ComputerDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.computer_div %1 %2)"
syntax function mod "(Why3__BigInt.computer_mod %1 %2)"
end
theory int.Power
prelude "open Why3extract"
syntax function power "(Why3__BigInt.power %1 %2)"
end
theory int.Fact
prelude "open Why3extract"
syntax function fact "(Why3__IntAux.fact %1)"
end
theory int.Fibonacci
prelude "open Why3extract"
syntax function fib "(Why3__IntAux.fib %1)"
end
......@@ -69,6 +78,7 @@ end
(* WhyML *)
module stack.Stack
prelude "open Why3extract"
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
syntax val push "Stack.push"
......@@ -84,6 +94,7 @@ module stack.Stack
end
module queue.Queue
prelude "open Why3extract"
syntax type t "(%1 Queue.t)"
syntax val create "Queue.create"
syntax val push "Queue.push"
......@@ -100,6 +111,7 @@ module queue.Queue
end
module array.Array
prelude "open Why3extract"
syntax type array "(%1 Why3__Array.t)"
syntax function ([]) "(Why3__Array.get %1 %2)"
......@@ -120,6 +132,7 @@ module array.Array
end
module matrix.Matrix
prelude "open Why3extract"
syntax type matrix "(%1 Why3__Matrix.t)"
syntax function get "(Why3__Matrix.get %1 %2)"
......@@ -137,16 +150,17 @@ module matrix.Matrix
end
module mach.int.Int
prelude "open Why3extract"
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
end
module mach.int.Int31
(* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int31 "int"
syntax val ( + ) "( + )"
......@@ -165,6 +179,7 @@ end
module mach.int.UInt64
(* no OCaml library for unsigned 64-bit integers => we use BigInt *)
prelude "open Why3extract"
syntax val of_int "(fun x -> x)"
syntax converter of_int "(Why3__BigInt.of_string \"%1\")"
......@@ -202,6 +217,7 @@ end
module string.Char
prelude "open Why3extract"
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
......@@ -211,13 +227,13 @@ end
module io.StdIO
prelude "open Why3extract"
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
prelude "open Why3extract"
syntax val random_int "Why3__BigInt.random_int"
end
......@@ -47,32 +47,26 @@ theory int.MinMax
syntax function max "(Pervasives.max %1 %2)"
end
(* FIXME
theory int.Lex2
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
theory int.EuclideanDivision
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
end
(* TODO
- int.EuclideanDivision
- number.Gcd
*)
theory int.Power
syntax function power "(Why3__BigInt.power %1 %2)"
prelude "let rec power x n = if n = 0 then 1 else x * power x (n-1)"
syntax function power "(power %1 %2)"
end
theory int.Fact
syntax function fact "(Why3__IntAux.fact %1)"
prelude "let rec fact n = if n <= 1 then 1 else n * fact (n-1)"
syntax function fact "(fact %1)"
end
theory int.Fibonacci
syntax function fib "(Why3__IntAux.fib %1)"
prelude "let rec fib n = if n <= 1 then n else fib (n-2) + fib (n-1)"
syntax function fib "(fib %1)"
end
TODO number.Gcd
*)
(* WhyML *)
module stack.Stack
......@@ -243,24 +237,3 @@ module mach.matrix.Matrix63
syntax val copy "(Array.map Array.copy)"
end
(* TODO
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
syntax function uppercase "Char.uppercase"
syntax function lowercase "Char.lowercase"
end
module io.StdIO
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
syntax val random_int "Why3__BigInt.random_int"
end
*)
......@@ -15,10 +15,10 @@ import "ocaml-gen.drv"
end*)
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int32"
syntax val of_int "Why3extract.Why3__BigInt.to_int32"
syntax converter of_int "%1l"
syntax function to_int "(Why3__BigInt.of_int32 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int32 %1)"
syntax type int32 "Int32.t"
syntax val (+) "Int32.add"
......@@ -39,10 +39,10 @@ module mach.int.Int32
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax constant zero_unsigned "0L"
syntax type uint32 "Int64.t"
......@@ -78,10 +78,10 @@ module mach.int.UInt32
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int63 "Int64.t"
syntax val (+) "Int64.add"
......@@ -99,10 +99,10 @@ module mach.int.Int63
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
......
......@@ -6,10 +6,10 @@ import "ocaml-gen.drv"
(** Machine arithmetic *)
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int32 "int"
syntax val ( + ) "( + )"
......@@ -27,10 +27,10 @@ module mach.int.Int32
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax constant zero_unsigned "0"
syntax type uint32 "int"
......@@ -63,10 +63,10 @@ module mach.int.UInt32
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int63 "int"
syntax val ( + ) "( + )"
......@@ -98,10 +98,10 @@ module mach.int.MinMax63
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
......@@ -120,7 +120,7 @@ end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val to_int "Why3extract.Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
......@@ -135,7 +135,7 @@ module mach.peano.Peano
syntax val add "(fun x y _ _ -> x+y)"
syntax val sub "(fun x y _ _ -> x-y)"
syntax val mul "(fun x y _ _ -> x*y)"
syntax val of_int "(fun n _ _ -> Why3__BigInt.to_int n)"
syntax val of_int "(fun n _ _ -> Why3extract.Why3__BigInt.to_int n)"
syntax val div "(/)"
syntax val mod "(mod)"
syntax val max "max"
......@@ -144,7 +144,7 @@ end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val to_int "Why3extract.Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
......
......@@ -19,10 +19,12 @@ theory bv.BV_Gen
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop eq_sub_equiv
remove prop Extensionality
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
......
......@@ -130,6 +130,7 @@ end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
(* not uniformly interpreted by provers
......
(* Why driver for first-order tptp provers *)
printer "tptp-tff1"
filename "%f-%t-%g.p"
valid "PROOF-FOUND"
timeout "Zenon error: could not find a proof within the time limit"
outofmemory "Zenon error: could not find a proof within the memory size limit"
unknown "NO-PROOF" "no proof found"
time "why3cpulimit time : %s s"
(* to be improved *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
import "discrimination.gen"
......@@ -8,83 +8,83 @@
<file name="../avl.mlw" expanded="true">
<theory name="SelectionTypes" sum="8ee3f641805a143e052f3881ea88fc8c">
<goal name="rebuild_aternative_def">
<proof prover="1" memlimit="0"><result status="valid" time="0.07"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.07" steps="116"/></proof>
</goal>
</theory>
<theory name="AVL" sum="e2c89c7fa1275fb01905418f8ee272f9" expanded="true">
<theory name="AVL" sum="fdbe08c09e5612ee8e8842441915e743" expanded="true">
<goal name="M.M.assoc">
<proof prover="1" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="M.M.neutral">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter real_height_nonnegative" expl="VC for real_height_nonnegative">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="rotation_preserve_model">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter height" expl="VC for height">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter total" expl="VC for total">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter node" expl="VC for node">
<proof prover="1" memlimit="0"><result status="valid" time="0.16"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.16" steps="98"/></proof>
</goal>
<goal name="WP_parameter singleton" expl="VC for singleton">
<proof prover="1" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.04" steps="87"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1" memlimit="0"><result status="valid" time="0.13"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.13" steps="78"/></proof>
</goal>
<goal name="WP_parameter view" expl="VC for view">
<proof prover="1" memlimit="0"><result status="valid" time="0.07"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.07" steps="241"/></proof>
</goal>
<goal name="WP_parameter balance" expl="VC for balance">
<transf name="split_goal_wp">
<goal name="WP_parameter balance.1" expl="1. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter balance.2" expl="2. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter balance.3" expl="3. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter balance.4" expl="4. unreachable point">
<proof prover="1" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.04" steps="55"/></proof>
</goal>
<goal name="WP_parameter balance.5" expl="5. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.05"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.05" steps="62"/></proof>
</goal>
<goal name="WP_parameter balance.6" expl="6. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.06"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.06" steps="72"/></proof>
</goal>
<goal name="WP_parameter balance.7" expl="7. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="WP_parameter balance.8" expl="8. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.19"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.19" steps="162"/></proof>
</goal>
<goal name="WP_parameter balance.9" expl="9. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.33"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.33" steps="283"/></proof>
</goal>
<goal name="WP_parameter balance.10" expl="10. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.33"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.33" steps="292"/></proof>
</goal>
<goal name="WP_parameter balance.11" expl="11. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter balance.12" expl="12. unreachable point">
<proof prover="1" memlimit="0"><result status="valid" time="0.22"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.22" steps="196"/></proof>
</goal>
<goal name="WP_parameter balance.13" expl="13. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.62"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.62" steps="550"/></proof>
</goal>
<goal name="WP_parameter balance.14" expl="14. precondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.11"/></proof>
......@@ -99,37 +99,37 @@
<proof prover="0" timelimit="2"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter balance.18" expl="18. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.03"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.03" steps="7"/></proof>
</goal>
<goal name="WP_parameter balance.19" expl="19. unreachable point">
<proof prover="1" memlimit="0"><result status="valid" time="0.09"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.09" steps="57"/></proof>
</goal>
<goal name="WP_parameter balance.20" expl="20. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.12"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.12" steps="71"/></proof>
</goal>