Work log 2016-09-01

quickspecBench is using MLSpec’s ‘raw’ quickspec code; i.e. it’s not doing the reduction.

We need to change the generated Haskell code to call quickSpec directly.

Done :)

Rather than calling quickSpec, which does a bunch of printing, etc. I’ve copied their definition, removed the printf stuff and told it to emit JSON rather than pretty-printing equations.

Standalone quickspecBench command now takes in smtlib data, outputs raw JSON timing info from Criterion and equations in JSON format.

Quick playing on laptop: example containing 5 definitions runs, although gave empty equations array. Example containing enture TIP dump ran out of memory. Will run on desktop and see what point it seems to die.

Now do same for MLSpec (should be straightforward; take CLUSTERS as a parameter).

Then do IsaCoSy.

Then do sampling in some kind of ‘main loop’, etc.