Can't compile SBVBench

[LeventErkok]

@doyougnu

Hi Jeffrey,

I'm doing some refactoring on SBV; and I got into a situation where SBVBench no longer compiles. The crux of the issue is that there's now two separate classes Provable and Satisfiable; whereas there used to be just one in the past (called Provable). Essentially, I took a bunch of methods from Provable and made them into a class of their own, motivated by some usability issues.

Everything is pushed onto the master.

Anyhow, your SBVBench code has some polymorphic code that no longer loads:

SBVBenchSuite/BenchSuite/Bench/Bench.hs:147:22: error:
    • Could not deduce (sbv-10.0:Data.SBV.Provers.Prover.MSatisfiable
                          IO a1)
        arising from a use of ‘U.satWith’
      from the context: U.Provable a
        bound by the type signature for:
                   runWith :: forall a.
                              U.Provable a =>
                              U.SMTConfig -> String -> a -> Runner
        at SBVBenchSuite/BenchSuite/Bench/Bench.hs:146:1-63
      or from: U.Provable a1
        bound by a type expected by the context:
                   forall a1. U.Provable a1 => U.SMTConfig -> a1 -> IO U.SatResult
        at SBVBenchSuite/BenchSuite/Bench/Bench.hs:147:22-30
    • In the first argument of ‘run'’, namely ‘U.satWith’
      In the expression: run' U.satWith c d (Problem p)
      In an equation for ‘runWith’:
          runWith c d p = run' U.satWith c d (Problem p)
    |
147 | runWith c d p = run' U.satWith c d (Problem p)
    |                      ^^^^^^^^^

I understand the error; because satWith is now in the Satisfiable class.

I gave it a shot to fix it; but got quickly mired in bench-testing code that I'm not familiar with. I hope this won't be too onerous for you to get it back to compile?

Thanks!

[doyougnu]

sure I'll have a look!

[doyougnu]

My bet is that it'll be pretty straightforward and most of the errors will be around the Existential I used for that benchmarking code