3 ms·
Compiling Scala without a SAT solver is probably too difficult. The CNF Converter is a gem. https://github.com/scala/scala/blob/v2.13.5/src/compiler/scala/too
by hackandthink 3y ago
Compiling Scala without a SAT solver is probably too difficult.
The CNF Converter is a gem.
https://github.com/scala/scala/blob/v2.13.5/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala#L50 https://github.com/scala/scala/blob/v2.13.5/src/compiler/sca...
- rwmj 3y agoCan you expand a bit on why / which bits of Scala compilation this is used for?
- hackandthink 3y agoIt is used for pattern matching. I don't know anything about the Scala compiler. A few years ago I needed a CNF Converter and I ripped their Logic Module. (performant CNF Converter are harder to find than SAT Solver)
- rwmj 3y agoNice idea! The pattern matching compiler/optimizer in OCaml doesn't do this. It's implemented using this algorithm which I've attempted to understand a few times but is a bit beyond me: Fabrice Le Fessant, Luc Maranget, Optimizing Pattern-Matching ICFP'2001 http://pauillac.inria.fr/~maranget/papers/opat/ http://pauillac.inria.fr/~maranget/papers/opat/