Not done: double_wp/logic and avl/table.
The subgoal pairing changed in verifythis_2017_tree_buffer
in an unrelated VC (see the diff for why3session.xml). FIXME?
In a chain "e1 op1 e2 op2 e3 op3 e4", each relation symbol is either:
- an infix symbol "=" or "<>", or
- a binary symbol whose value type is Bool.bool or Prop (for lsymbols)
and whose arguments' types are not Bool.bool.
In other words, we interpret a chain as a conjunction only if there
is no possibility(*) to interpret it as a superposition. The exception
is only made for "=" and "<>", which are _always_ considered as
chainable, even if they are redefined with some bogus type signatures.
Notice that redefining "<>" has no effect whatsoever, since "<>" is
always treated as negated "=".
As for the evaluation order, the chain above would be equivalent to:
let x2 = e2 in
(e1 op1 x2) &&
let x3 = e3 in
(x2 op2 x3) &&
(x3 op3 e4)
This is due to the fact that lazy conjunctions are evaluated from
left to right, function arguments are evaluated from right to left,
and no expression should be evaluated twice.
[*] well, not really, since we consider symbols ('a -> 'b -> bool)
as chainable, even though such chains could be interpreted as
superpositions(**). We could treat such symbols as unchainable,
but that would make equality and disequality doubly special cases,
and I don't like it. We'll see if the current conditions are not
enough.
[**] what also bothers me is dynamic types of locally defined
infix symbols, which can be type variables or Bool.bool depending
on the order of operations in Mlw_typing. Currently, I can't come
up with any example of bad behaviour -- we are somewhat saved by
not being able to write "let (==) = ... in ...").
- all programs with sessions are in examples/
- all programs without sessions are in examples/in_progress/
(if you have private sessions for those, just move them there)
- all pure logical problems are in logic/
(to simplify bench scripts and gallery building; they are few anyway)
- all OCaml programs are in examples/use_api/
- all strange stuff is in examples/misc/
(most of it should probably go)
- Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
(why do we need two sets of solutions for quite simple problems?)
- hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/
Bench scripts and documentation are updated.
Also, bench/bench is simplified a little bit.
