Weight of Select/Store axioms

[shazqadeer]

I noticed a discrepancy between weight supplied for Boogie-generated Select/Store axioms in TypeDeclCollector.cs and in the code that performs type erasure. The former kicks in when the Boogie code is monomorphic and the latter kicks in when the Boogie code is polymorphic. The former does not supply a weight and the latter supplies a weight of 0. Is there a reason for this discrepancy? If it is an oversight, should the monomorphic path also supply weight of 0?

@RustanLeino : Please speak because I don't imagine anybody else has context on my question.

[RustanLeino]

The reason for having a weight of 0 for these is so the SMT solver will not be hindered in applying the axioms.

Consider a program with a very long chain of assignments to a map variable (e.g., assignments like Heap[p, x] := E;). To prove a property (say, Heap[this, f] == 100) after these assignments, the select/store axioms need to be enough times to get to the place where Heap[this, f] is assigned. If the default weight of 1 is apply with each axiom use, then you could only prove properties where the chain of assignments have length up to smt.qi.eager_threshold. Boogie used to set this threshold to 100, and Dafny still does (and if this were ever to be changed, it would be to decrease the threshold, not increase it).

The reason for having a non-0 weight is to try to say "if the SMT solver is going crazy with instantiations of this axiom, then it's probably barking up the wrong tree". From the way select/store are used, this seems unlike to ever apply to them.

In conclusion, I think it's a really good idea to set the weight of the select/store axioms to 0, also in the monomorphic path.

[shazqadeer]

Ok, I am putting up PR #386 to address this issue.

[shazqadeer]

FYI: @emmazzz, @wrwg