Merge commit '0a191c7b' into counter-examples

Makefile.in

@@ -866,7 +866,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
 COQLIBS_SET_FILES = Set
 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
 
-COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection
+COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
 COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
 
 COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
@@ -1148,7 +1148,7 @@ ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/number/, $(ISAB
 ISABELLELIBS_SET_FILES = Set Fset
 ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELIBS_SET_FILES)))
 
-ISABELLELIBS_MAP_FILES = Map Occ MapPermut MapInjection
+ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
 ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES)))
 
 ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
@@ -1270,7 +1270,8 @@ clean::
 # Ocaml realizations
 #######################
 
-OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array
+OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array \
+	          why3__Matrix
 
 OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
 

ROADMAP

@@ -155,19 +155,24 @@ Release Notes (details in file CHANGES):
 
 == TODO ==
 
+* Document src/core/trans.mli, and fill the paragraph on
+  transformations in the tutorial: doc/api.tex, section 4.7 "Applying
+  transformations"
+
 * fix bug 18953 : (<>) not allowed as prefix form
 
 * finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
 
 * integrate server feature done by Johannes
 
-* Coq realization of bitvector theory
+* DONE Coq realization of bitvector theory
 
 * make counter-examples feature more robust
 
-* support for both isabelle 2014 and 2015
+* DONE support for both isabelle 2014 and 2015
+  + bugfix for installation
 
-* review support for division operators by SMT provers
+* DONE review support for division operators by SMT provers
 
 * take some time to fix some bugs of the BTS: 18029 at least
 
@@ -176,7 +181,7 @@ Release Notes (details in file CHANGES):
   alt-ergo -replay <file>.agr
 
 * make the strategy feature public and documented. Possibly generate
-  default stratregies dynamically at the time of why3 config --detect,
+  default strategies dynamically at the time of why3 config --detect,
   using the provers detected : for that, we can annotated the provers in
   prover-detection-data.conf to tell if they should be used in the strategies,
   with which priority
@@ -187,7 +192,7 @@ Release Notes (details in file CHANGES):
 
   . or, on the contrary, favor splitting
 
-  . or, favor timelimt increase...
+  . or, favor timelimit increase...
 
 
 

bench/programs/bad-typing/variant3.mlw

+
+(* Different instances of a polymorphic relation. *)
+
+module M
+  
+  use import list.List
+  
+  predicate rel (a b:list 'a)
+  
+  let rec aux (a:list int) : unit
+    variant { a with rel }
+  = aux2 Nil
+  
+  with aux2 (a:list unit) : unit
+    variant { a with rel }
+  = aux Nil
+  
+end
+

check.sh

 # useful script for git bisect
 
-make || exit 125 ; bin/why3config --detect && bin/why3replay examples/bellman_ford.mlw
+(autoconf && ./configure --enable-local --disable-coq-libs --disable-isabelle-libs && make) || exit 125 ; bin/why3config --detect && bin/why3replay examples/linear_probing.mlw

drivers/coq-ssreflect.drv

+
+prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
+prelude "(* Beware! Only edit allowed sections below    *)"
+
+printer "coq-ssr"
+filename "%t.v"
+
+valid 0
+unknown "Error: \\(.*\\)$" "\\1"
+fail "Syntax error: \\(.*\\)$" "\\1"
+time "why3cpulimit time : %s s"
+
+transformation "inline_trivial"
+transformation "eliminate_non_struct_recursion"
+transformation "eliminate_if"
+transformation "eliminate_non_lambda_set_epsilon"
+transformation "eliminate_projections"
+transformation "simplify_formula"
+
+
+theory BuiltIn
+
+  prelude "
+Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.
+Require Import ssrint ssrwhy3.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+"
+
+  syntax type int "int"
+  syntax type real "R"
+  syntax predicate  (=)   "(%1 = %2)"
+
+end
+
+theory HighOrd
+  syntax type func "(%1 -> %2)"
+  syntax type pred "(%1 -> bool)"
+  syntax function (@)  "(%1 %2)"
+end
+
+theory Bool
+
+  syntax type bool   "bool"
+
+  syntax function True  "true"
+  syntax function False "false"
+end
+
+theory bool.Bool
+
+  syntax function andb  "(Init.Datatypes.andb %1 %2)"
+  syntax function orb   "(Init.Datatypes.orb %1 %2)"
+  syntax function xorb  "(Init.Datatypes.xorb %1 %2)"
+  syntax function notb  "(Init.Datatypes.negb %1)"
+  syntax function implb "(Init.Datatypes.implb %1 %2)"
+
+end
+
+theory map.Map
+  syntax type     map "(%1 -> %2)%type"
+  syntax function get "(%1 %2)"
+end
+
+theory map.Const
+  remove prop Const
+end
+
+theory int.Int
+
+  prelude "
+Require Import ssralg ssrnum.
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope."
+
+  syntax function zero "0%:Z"
+  syntax function one  "1%:Z"
+
+  syntax function (+)  "(%1 + %2)%R"
+  syntax function (-)  "(%1 - %2)%R"
+  syntax function ( * )  "(%1 * %2)%R"
+  syntax function (-_) "(-%1)%R"
+
+  syntax predicate (<=) "(%1 <= %2)%R"
+  syntax predicate (<)  "(%1 < %2)%R"
+  syntax predicate (>=) "(%1 >= %2)%R"
+  syntax predicate (>)  "(%1 > %2)%R"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc
+  remove prop CommutativeGroup.Unit_def_l
+  remove prop CommutativeGroup.Unit_def_r
+  remove prop CommutativeGroup.Inv_def_l
+  remove prop CommutativeGroup.Inv_def_r
+  remove prop Assoc.Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop ZeroLessOne
+
+end
+
+theory array.Array
+
+  syntax type array "(array %1)"
+
+  syntax function get "(get %1 %2)"
+  syntax function length "(size %1 : int)"
+  syntax function elts "(get %1)"
+  syntax function set "(set %1 %2 %3)"
+(* does not exist anymore
+  syntax function make "(make %1 %2)"
+*)
+
+end
+
+theory matrix.Matrix
+
+  syntax type matrix "(matrix %1)"
+
+  syntax function get "(matrix_get %1 %2 %3)"
+  syntax function rows "(nrows %1 : int)"
+  syntax function columns "(ncols %1 : int)"
+  syntax function elts "(matrix_get_curry %1)"
+  syntax function set "(matrix_set %1 %2 %3)"
+(* does not exist anymore
+  syntax function make "(matrix_make %1 %2)"
+*)
+
+end

drivers/isabelle-common.gen

@@ -134,7 +134,11 @@ theory map.Map
   syntax function ([]) "<app>%1%2</app>"
   syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
   syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
+end
+
+theory map.Const
   syntax function const "<app><const name=\"_type_constraint_\"><fun>%t0%t0</fun></const><abs name=\"\"><type name=\"dummy\"/>%1</abs></app>"
+
 end
 
 theory set.SetGen

drivers/mathsat.drv

@@ -170,10 +170,13 @@ theory map.Map
   syntax type map "(Array %1 %2)"
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
-  meta "encoding : lskept" function const
 
   syntax function get   "(select %1 %2)"
   syntax function set   "(store %1 %2 %3)"
+end
+
+theory map.Const
+  meta "encoding : lskept" function const
 (*  syntax function const "(const[%t0] %1)" *)
 end
 

drivers/ocaml-gen.drv

@@ -119,6 +119,23 @@ module array.Array
   syntax val blit          "Why3__Array.blit"
 end
 
+module matrix.Matrix
+  syntax type matrix "(%1 Why3__Matrix.t)"
+
+  syntax function get "(Why3__Matrix.get %1 %2)"
+
+  syntax exception OutOfBounds "Why3__Matrix.OutOfBounds"
+
+  syntax val get           "Why3__Matrix.get"
+  syntax val set           "Why3__Matrix.set"
+  syntax val rows          "Why3__Matrix.rows"
+  syntax val columns       "Why3__Matrix.columns"
+  syntax val defensive_get "Why3__Matrix.defensive_get"
+  syntax val defensive_set "Why3__Matrix.defensive_set"
+  syntax val make          "Why3__Matrix.make"
+  syntax val copy          "Why3__Matrix.copy"
+end
+
 module mach.int.Int
   syntax val ( / ) "Why3__BigInt.computer_div"
   syntax val ( % ) "Why3__BigInt.computer_mod"

drivers/ocaml-unsafe-int.drv

 
 (** OCaml driver with Why3 type int being mapped to OCaml type int.
 
-    This is of course unsafe, yet useful to run your code is you
-    have an independant argument regarding the absence of arithmetic
+    This is of course unsafe, yet useful to run your code when you
+    have an independent argument for the absence of arithmetic
     overflows. *)
 
-printer "ocaml"
+printer "ocaml-unsafe-int"
 
 theory BuiltIn
   syntax type int "int"
-  (* meta "ocaml arithmetic" "unsafe int" *)
   syntax predicate  (=)   "(%1 = %2)"
 end
 
@@ -127,6 +126,23 @@ module array.Array
   syntax val blit          "Array.blit"
 end
 
+module matrix.Matrix
+  syntax type matrix "(%1 array array)"
+
+  syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
+
+  syntax function rows     "(Array.length %1)"
+  syntax function columns  "(Array.length %1.(0))"
+  syntax val rows          "Array.length"
+  syntax val columns       "(fun m -> Array.length m.(0))"
+  syntax val get           "(fun m i j -> m.(i).(j))"
+  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val defensive_get "(fun m i j -> m.(i).(j))"
+  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val make          "Array.make_matrix"
+  syntax val copy          "(Array.map Array.copy)"
+end
+
 module mach.int.Int31
   syntax val       of_int   "(fun x -> x)"
   syntax converter of_int   "%1"
@@ -147,6 +163,37 @@ module mach.int.Int31
   syntax val      (>=)      "(>=)"
   syntax val      (>)       "(>)"
 end
+module mach.int.Int63
+  syntax val       of_int   "(fun x -> x)"
+  syntax converter of_int   "%1"
+
+  syntax function to_int "(%1)"
+
+  syntax type     int63     "int"
+  syntax val      ( + )     "( + )"
+  syntax val      ( - )     "( - )"
+  syntax val      (-_)      "( ~- )"
+  syntax val      ( * )     "( * )"
+  syntax val      ( / )     "( / )"
+  syntax val      ( % )     "(mod)"
+  syntax val      eq        "(=)"
+  syntax val      ne        "(<>)"
+  syntax val      (<=)      "(<=)"
+  syntax val      (<)       "(<)"
+  syntax val      (>=)      "(>=)"
+  syntax val      (>)       "(>)"
+end
+module mach.int.Refint63
+  syntax val incr "Pervasives.incr"
+  syntax val decr "Pervasives.decr"
+  syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
+  syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
+  syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
+end
+module mach.int.MinMax63
+  syntax val min "Pervasives.min"
+  syntax val max "Pervasives.max"
+end
 
 (* TODO
    other mach.int.XXX modules *)
@@ -165,6 +212,36 @@ module mach.array.Array31
   syntax val  blit   "Array.blit"
   syntax val  self_blit "Array.blit"
 end
+module mach.array.Array63
+  syntax type array63 "(%1 array)"
+
+  syntax val  make   "Array.make"
+  syntax val  ([])   "Array.get"
+  syntax val  ([]<-) "Array.set"
+  syntax val  length "Array.length"
+  syntax val  append "Array.append"
+  syntax val  sub    "Array.sub"
+  syntax val  copy   "Array.copy"
+  syntax val  fill   "Array.fill"
+  syntax val  blit   "Array.blit"
+  syntax val  self_blit "Array.blit"
+end
+module mach.matrix.Matrix63
+  syntax type matrix "(%1 array array)"
+
+  syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
+
+  syntax function rows     "(Array.length %1)"
+  syntax function columns  "(Array.length %1.(0))"
+  syntax val rows          "Array.length"
+  syntax val columns       "(fun m -> Array.length m.(0))"
+  syntax val get           "(fun m i j -> m.(i).(j))"
+  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val defensive_get "(fun m i j -> m.(i).(j))"
+  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val make          "Array.make_matrix"
+  syntax val copy          "(Array.map Array.copy)"
+end
 
 (* TODO
 module string.Char

drivers/ocaml64.drv

@@ -85,6 +85,17 @@ module mach.int.Int63
 (*  syntax val      to_bv     "(fun x -> x)"
   syntax val      of_bv     "(fun x -> x)"*)
 end
+module mach.int.Refint63
+  syntax val incr "Pervasives.incr"
+  syntax val decr "Pervasives.decr"
+  syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
+  syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
+  syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
+end
+module mach.int.MinMax63
+  syntax val min "Pervasives.min"
+  syntax val max "Pervasives.max"
+end
 
 module mach.int.Int64
   syntax val of_int "Why3__BigInt.to_int64"
@@ -186,7 +197,7 @@ module mach.array.Array32
 end
 
 module mach.array.Array63
-  syntax type array  "(%1 array)"
+  syntax type array63 "(%1 array)"
 
   syntax val  make   "Array.make"
   syntax val  ([])   "Array.get"
@@ -199,3 +210,33 @@ module mach.array.Array63
   syntax val  blit   "Array.blit"
   syntax val  self_blit "Array.blit"
 end
+module mach.array.Array63
+  syntax type array63 "(%1 array)"
+
+  syntax val  make   "Array.make"
+  syntax val  ([])   "Array.get"
+  syntax val  ([]<-) "Array.set"
+  syntax val  length "Array.length"
+  syntax val  append "Array.append"
+  syntax val  sub    "Array.sub"
+  syntax val  copy   "Array.copy"
+  syntax val  fill   "Array.fill"
+  syntax val  blit   "Array.blit"
+  syntax val  self_blit "Array.blit"
+end
+module mach.matrix.Matrix63
+  syntax type matrix "(%1 array array)"
+
+  syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
+
+  syntax function rows     "(Array.length %1)"
+  syntax function columns  "(Array.length %1.(0))"
+  syntax val rows          "Array.length"
+  syntax val columns       "(fun m -> Array.length m.(0))"
+  syntax val get           "(fun m i j -> m.(i).(j))"
+  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val defensive_get "(fun m i j -> m.(i).(j))"
+  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
+  syntax val make          "Array.make_matrix"
+  syntax val copy          "(Array.map Array.copy)"
+end

drivers/pvs-common.gen

@@ -38,6 +38,9 @@ theory map.Map
   remove prop Select_eq
   remove prop Select_neq
 
+end
+
+theory map.Const
   syntax function const "(LAMBDA (x:%v0): %1)"
   remove prop Const
 end
@@ -263,7 +266,7 @@ end
 
 theory list.Mem
   syntax predicate mem "member(%1, %2)"
-  
+
 end
 
 theory list.Nth

drivers/smt-libv2-bv.gen

@@ -55,6 +55,9 @@ theory bv.BV64
 
   syntax function nth_bv
     "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
+(* possible alternative definition :
+    "(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
+*)
 
   syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
   syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"

drivers/smt-libv2.drv

@@ -142,11 +142,24 @@ end
 
 theory map.Map
   syntax type map "(Array %1 %2)"
-  meta "encoding : lskept" function get
-  meta "encoding : lskept" function set
-  meta "encoding : lskept" function const
+  meta "encoding:ignore_polymorphism_ts" type map
 
   syntax function get   "(select %1 %2)"
   syntax function set   "(store %1 %2 %3)"
+  meta "encoding : lskept" function get
+  meta "encoding : lskept" function set
+  meta "encoding:ignore_polymorphism_ls" function get
+  meta "encoding:ignore_polymorphism_ls" function ([])
+  meta "encoding:ignore_polymorphism_ls" function set
+  meta "encoding:ignore_polymorphism_ls" function ([<-])
+
+  meta "encoding:ignore_polymorphism_pr" prop Select_eq
+  meta "encoding:ignore_polymorphism_pr" prop Select_neq
+  remove prop Select_eq
+  remove prop Select_neq
+end
+
+theory map.Const
+  meta "encoding : lskept" function const
 (*  syntax function const "(const[%t0] %1)" *)
 end

drivers/why3.drv

@@ -3,17 +3,8 @@
 printer "why3"
 filename "%f-%t-%g.why"
 
-(* transformation "detect_polymorphism" *)
-
 theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax predicate (=)  "(%1 = %2)"
-  (* meta "encoding:ignore_polymorphism_ls" predicate (=) *)
-end
-
-(*
-theory list.List
-  meta "encoding:ignore_polymorphism_ts" type list
 end
-*)

drivers/why3_smt.drv

@@ -4,20 +4,30 @@ printer "why3"
 filename "%f-%t-%g.why"
 
 transformation "inline_trivial"
-
 transformation "eliminate_builtin"
-transformation "eliminate_recursion"
+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"
+transformation "eliminate_algebraic_if_poly"
 transformation "eliminate_epsilon"
 
-transformation "discriminate"
-transformation "encoding_smt"
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
 
 theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax predicate (=)  "(%1 = %2)"
+  meta "encoding:ignore_polymorphism_ls" predicate (=)
 
   meta "encoding : kept" type int
   meta "encoding : kept" type real
@@ -26,7 +36,17 @@ end
 theory map.Map
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
-  meta "encoding : lskept" function const
+
+  meta "encoding:ignore_polymorphism_ts" type map
+  meta "encoding:ignore_polymorphism_ls" function get
+  meta "encoding:ignore_polymorphism_ls" function ([])
+  meta "encoding:ignore_polymorphism_ls" function set
+  meta "encoding:ignore_polymorphism_ls" function ([<-])
+  meta "encoding:ignore_polymorphism_pr" prop Select_eq
+  meta "encoding:ignore_polymorphism_pr" prop Select_neq
+
+  remove prop Select_eq
+  remove prop Select_neq
 end