Maciej Bendkowski
Maciej Bendkowski
The current paganini input specification is rather unpleasant and difficult to debug, especially for larger systems. Keeping track of appropriate indexes is not a task which should be delegated to...
Consider the following specification: > Nat = S Nat [0.3] | Z. > Term = App Nat [Term] | Var Nat. and the corresponding paganini specification generated by boltzmann-brain: >...
Using the `-f` flag it is possible to disable well-foundedness checks. Consequently, the constructed paganini specification might not be sensible. In one such case (see the `examples/ill-founded.in` example) the optimisation...
_Boltzmann brain_ should support the automatic generation of samplers for Pólya structures involving admissible constructors such as the `MSet` or `Cycle` constructions.
The current pull request upgrades the `goal_runner` to support `z3` version `4.8.7`. Essentially, it uses `z3`'s new API to parse SMT files, cf. https://github.com/Z3Prover/z3/issues/2798. In addition, it proposes two lesser...