compile it with make src/trywhy3/trywhy3.js

run it by loading src/trywhy3/index.html in your favorite browser

first issue to solve : loading of standard library

triggering VC.

- Transformation intro_vc_vars_counterexamp introduces new constant with
model labels for every variable in the term that trigger VC and axiom
that this constant is equal to the variable, finds the position of the
term that trigger VC, and saves this position in meta (for smtv2
printer).

- Transformation prepare_for_counterexmp additionally performs the
transformation intro_vc_vars_counterexamp

- smtv2 printer no longer collects the location of the term that
triggers VC and does not collect variables in this term in a special
way. Note that this functionality was not yet completely removed from
the printer. It will be done so after the transformation
intro_vc_vars_counterexmp will be tested.

The rationale:
Variables that should be displayed in counterexample are marked
by model labels ("model", "model_projected", "model_trace:*").

Variables inside the term that triggers VC should be displayed in
counterexample for that VC. However, many VCs (tasks) can be generated
for  a signle *.mlw file and only variables in the term that trigger
the VC (task) that is currently proven should be displayed. That means
that the process of selecting variables inside the term that triggers
VC for counterexample must be done while processing the task. It is
done by transformation intro_vc_vars_counterexmp. This means that smtv2
printer no longer has to find the position of the term that triggers
VC and no longer has to collect variables in this term in a special
way.

Fix Bool.v
Add TODO to Seq.v and BV_Gen.v
update queens_bv session

Add int.NumOf realization.

Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

- generation in the makefile
- proofs done
Remove complex axioms from Pow2int in bv.why.
Add guards in rotates axioms in bv.why.

p labeled with label "model_projected" for that it exists a projection
function f creates declaration of new constant c and axiom stating that
c = f p

Projection functions are functions tagged with meta "model_projection".
Function f is projection function for abstract function and predicate p
if f is tagged with meta "model_projection" and has a single argument
of the same type as is the type of p.

This transformation is needed in situations when we want to display not
value of a variable, but value of a projection function applied to a variable.

Note that since Why3 supports namespaces (different projection functions
can have the same name) and input languages of solvers typically not,
Why3 renames projection functions to avoid name clashes.
This is why it is not possible to just store the name of the projection
function in a label and than query the solver directly for the value of
the projection.
Also, it means that this transformation should thus be executed before
this renaming.