Improve RAC

This MR covers a number of improvements to make RAC more complete for arrays.

Here is a summary of the changes:

• src/mlw/counterexample.{ml,mli}

  Keep at most one empty model when selecting

• src/mlw/pinterp.{ml,mli}

  • Choose representation of arrays as terms by environment variable

  An array in the runtime of pinterp is an OCaml array of pinterp values. An array in the Why3 logic is a private record with fields length and elts, mapping indices to values.

  A runtime array a of length n can be converted into a logical Why3 array as

  1. a sequence of updates: (make <n> undefined)[0 <- a[0]]...[n-1 <- a[n-1]]
  2. an epsilon term: (epsilon v. v.length = <n> /\ v[0] = a[0] /\ ... /\ v[n-1] = a[n-1])

  From a quick test it seems that provers can handle arrays much better as epsilon terms (because it is flatten out by transformation eliminate_epsilon.

  So by default, arrays are converted into an epsilon term, but if the environment variable WHY3PINTERPARRAY is set to update, it is converted in a sequence of updates.

  • Add option --rac-try-negate to dispatch negated goals to the prover (to refute assertions using SMT provers)

  • Take used and cloned modules into account when converting assertions into tasks

  • Store field names in pinterp values for constructors and use them for printing records

  • Partial builtins in Pinterp, which yield to cannot compute (they were left uninterpreted before)

  • Remove void value and add value undefined (as default for arrays)

• stdlib/array.mlw

  Separate logical and program function Array.make

  When defined as a val function the postcondition of the program function make is just result = make n v, referring to the logical function make. But the equality cannot be proven because array equality is not defined.

  To facilitate proofs about results of the program functions make, this commit separates the definitions of the logical function from the program function make, so that the postconditions of the program function make refer to the properties of the resulting array.

• src/tools/why3execute.ml

  Organise output channels and return values

• bench/bench

  Allow stuck and cannot compute for RAC tests (until !426 (closed))

• doc/manpages.rst

  Document option --rac-try-negate

• bench/{ce,check-ce}/oracles/**/*.oracle

  Update oracles

• bench/replay/*/{why3shapes.gz,why3session.xml}

  Update sessions

• examples/**/{why3shapes.gz,why3sessions.xml}

  Update proofs and sessions