Repeating destructor name causes long verification times

[jaylorch]

Using the same destructor name in multiple constructors seems to blow up verification time. Moreover, this happens even for verification conditions that don't concern the datatype!

The example below has a datatype D with 500 constructors, all with destructor n. (I use ellipses to abbreviate.) The lemmas are trivial but take about 24, 12, and 12 seconds to verify. The former high time is presumably due to initial Boogie processing, but the latter ones show that, even after pre-processing is over, verifications still take a while.

Looking at the Boogie file, it seems that every canCall, for every instance of IsZeroD, is invoking the definitions of all the constructors. But, this shouldn't be necessary since each IsZeroD uses a discriminator to specify that it's talking about a specific constructor before it uses a destructor.

The massive quantity of canCall terms is presumably what's slowing down Boogie's VC construction and Z3. I determined that Z3 accounts for about 1/3 of the total time by having Boogie print its prover log and submitting that to Z3; Z3 took about 15 seconds to give unsat three times.

module Dependencies
{
  import Defs

  lemma True()
    ensures true
  { }

  lemma True2()
    ensures true
  { }

  lemma True3()
    ensures true
  { }
}

module Defs
{
  datatype D = D0(n:int) | D1(n:int) | ... | D499(n:int)

  predicate IsZeroD0(d:D)
  {
    d.D0? ==> d.n == 0
  }

  predicate IsZeroD1(d:D)
  {
    d.D1? ==> d.n == 0
  }

 ...

  predicate IsZeroD499(d:D)
  {
    d.D499? ==> d.n == 0
  }
}

[RustanLeino]

500 constructors! 😮 Here's a thought I had, but it seems not relevant to the example. Nevertheless, I'm recording the thought here:

One property of a datatype is that each of its values comes from some constructor of the datatype. This "exhaustiveness" property (or "Depth-one case-split axiom" as the verifier calls it) has the form

$IsA#D(d) ==> D0?(d) || D1?(d) || ...

and can be very expensive, even with just a few constructors. I thought, perhaps this axiom gets instantiated, introduces the 500 cases, and then ends up taking time for Z3 to prune it down.

Since the exhaustiveness property is expensive, Dafny makes it available only in certain places. One of those places for given in-parameters. But when I now look at the implementation, I see that the verifier uses it only for methods, not functions.

So much for that thought.