Introduce our own TreeT monad

[serras]

This PR completely removes WeightedList in favor of our own TreeT. This data type has been engineering to completely fit our purposes:

• at each node we keep track of the state, so we can see how it changes,
• when we branch we can attach a tag, so we can later see how it's used (for example, in symbolic evaluation we tag what is the constructor we use).

[serras]

I've rebased this PR on top of the latest changes in dev, so it merges cleanly.

[serras]

A few comments before merging this:

• For some reason when parallelism is introduced (via withStrategy) and we have some threads, some operations don't finish. This may be related to the locking mechanism of the new pure SMT interface.
• The O'Hearn Peano test doesn't end, but I have no clear explanation why. My gut feeling is that because we're now saving every intermediate step, and those are big, we may have some problems. On the other hand, a preliminary investigation removing the tag from the Branch constructor of Tree didn't solve the problem.

[lucaspena]

On my end, the O'Hearn Peano test successfully terminates in 60-75 seconds (I ran it a few times). So it seems the tree is making the test take much longer, but it looks like it is terminating at least.

[VictorCMiraldo]

I just noticed the existence of the gr/unstate branch from @0xd34df00d. How does the work in these two branches relate? It's good to communicate to make sure we're not overlapping work.

[lucaspena]

I did some investigation on the runtime of this problematic O'Hearn Peano test in this branch and in dev. I tested it with varying bounds for sestConsumedFuel, both with the wrong triple (where the test should terminate more quickly after finding a counterexample) and with the correct triple (where the test will only terminate once the bound is reached). The numbers are below, 13 is the lowest number where the counterexample is found so that's the lowest bound checked.

• treet branch

  • correct triple
  • sestConsumedFuel > 50: 407.23s
  • sestConsumedFuel > 35: 66.49s
  • sestConsumedFuel > 25: 9.32s
  • sestConsumedFuel > 13: 0.10s
  • wrong triple
  • sestConsumedFuel > 50: 65.70s
  • sestConsumedFuel > 35: 18.67s
  • sestConsumedFuel > 25: 5.91s
  • sestConsumedFuel > 13: 0.43s

• dev branch

  • correct triple
  • sestConsumedFuel > 50: 419.04s
  • sestConsumedFuel > 35: 68.19s
  • sestConsumedFuel > 25: 10.02s
  • sestConsumedFuel > 13: 0.11s
  • wrong triple
  • sestConsumedFuel > 50: 0.20s
  • sestConsumedFuel > 35: 0.21s
  • sestConsumedFuel > 25: 0.20s
  • sestConsumedFuel > 13: 0.21s

So my original hypothesis that the treet branch was exploring until the fuel threshold is reached appears to be false. Still, when forced to explore that much, the treet branch takes no longer than the dev branch. It's unclear why with the wrong triple, the treet branch takes so much longer. Perhaps it is exploring some additional states (though not all) before checking if the triple is violated? Regardless, since exploring up to the fuel threshold results in similar times on both branches, it doesn't appear that the changes in the treet branch can improve runtime (but ideally it also should not lose time either, assuming this bug can be fixed).

[VictorCMiraldo]

Great stuff @lucaspena, thank you! Besides having empirical evidence that the treet branch is doing additional work, it reinforces the idea that currently, in dev we are returning the first counterexample we find and looking no further! (#97)

[VictorCMiraldo]

The work of #137 will supersede this; this PR is stale and we decided not to move forward with it.