benchsuite: compile with MProvable and MSatisfiable

[doyougnu]

Hey Levent,

I think I have #649 sorted out. My hunch was right about the Existential:

data Problem = forall a . (U.Provable a, U.Satisfiable a) => Problem a

That existential basically allows the benchsuite to abstract over how the code is run. Without it, I'm not sure how we would be able to right benchmarks that are run in different ways like in BenchSuite.Uninterpreted.Multiply:

benchmarks :: Runner
benchmarks = rGroup
  [ run "synthMul22" synthMul22 `using` runner satWith
  , run "Correctness" correct `using` runner proveWith
  ]

But now we have a different problem. Because I changed the constraints on Problem we have a lot of Benchmarks that now require a Provable instance over Goal. So I get a handful of these kinds of errors now:

SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs:25:5: error:
    • No instance for (sbv-10.0:Data.SBV.Provers.Prover.MProvable
                         IO Goal)
        arising from a use of ‘run’
    • In the first argument of ‘using’, namely
        ‘run "synthMul22" synthMul22’
      In the expression:
        run "synthMul22" synthMul22 `using` runner satWith
      In the first argument of ‘rGroup’, namely
        ‘[run "synthMul22" synthMul22 `using` runner satWith,
          run "Correctness" correct `using` runner proveWith]’
   |
25 |   [ run "synthMul22" synthMul22 `using` runner satWith

This instance is required because run does not know if we'll be proving or checking sat. That is determined with the using combinator and the fooWith functions exported from SBV, so we have to require both constraints on run unless we want to re-architect the benchmark suite (which I don't really have time to do, but could be a good first contributor ticket).

So I think we have two paths forward:

1) bite the bullet and just disable the benchmarks that require the Provable Goal instance. We're looking at around 8-10 benchmarks here. The larger problem is that then the benchmark suite would not be testing these code paths! 2) We could move the Provable Goal instance into the benchmark suite just as a hack. This way it wouldn't need to be a part of the public API. The only catch is that this would mean exporting the ExtractIO module so that I can import it in the benchmark suite and write the bad instance.

I'm somewhat partial to (2), what do you think?

[doyougnu]

Marking as draft until we have the path forward figured out.

[LeventErkok]

You nailed it! My entire motivation to separate Provable/Satisfiable was precisely to disallow proving goal's. (It's very confusing to be able to prove "pure ()".)

Yes; the cheating instance for "Provable Goal" is fine, so long as it's in the benchmark suite only. But why do we need to export 'ExtractIO' module? We can export it from Data.SBV.Internals and you can get it through there, no?

[doyougnu]

But why do we need to export 'ExtractIO' module?

The instance we want to write is

-- instance ExtractIO m => MProvable m (SymbolicT m ())  -- NO INSTANCE ON PURPOSE; don't want to prove goals

(which I rather like the comment :P), anyway we I think we need access to the ExtractIO name in order to write that particular instance...but now that I think about it. All we need is

-- instance MProvable IO (SymbolicT IO ())  -- NO INSTANCE ON PURPOSE; don't want to prove goals

So perhaps it'll be fine. MProvable isn't exported from Data.SBV or Data.SBV.Internals?

[LeventErkok]

MProvable isn't exported on purpose. But go ahead and export it from Data.SBV.Internals; the proverbial kitchen-sink

[doyougnu]

all done. You can test with

cabal bench --test-options='--quiet'

marking as ready.

[doyougnu]

FYI we get one test where the missing method on the MProvable is problematic:

      Nested.Example:                         FAIL
        Exception: Solver said unknown!
        CallStack (from HasCallStack):
          error, called at ./Documentation/SBV/Examples/Lists/Nested.hs:41:52 in sbv-10.0-inplace:Documentation.SBV.Examples.Lists.Nested
        Use -p '/Nested.Example/' to rerun this test only.

[LeventErkok]

Thanks!

[LeventErkok]

@doyougnu

FYI we get one test where the missing method on the MProvable is problematic:

      Nested.Example:                         FAIL
        Exception: Solver said unknown!
        CallStack (from HasCallStack):
          error, called at ./Documentation/SBV/Examples/Lists/Nested.hs:41:52 in sbv-10.0-inplace:Documentation.SBV.Examples.Lists.Nested
        Use -p '/Nested.Example/' to rerun this test only.

Yes, I'm aware of this: https://github.com/LeventErkok/sbv/blob/cba3886c704a4d11face1c0c09406342c4b8ac91/Documentation/SBV/Examples/Lists/Nested.hs#L26-L30

It's been turned off in the regular tests since z3 no longer can handle it. (Was reported to them, but I don't think they've the bandwidth to fix it.)

I guess it doesn't hurt to leave it in the benchmark suite; up to you if you want to "turn it off" there too.

Thanks for the quick patch!