Just for completeness sake: There is also the "boolean expression simplifier" [1] library implementing the Quine-McCluskey algorithm (and friends) in pure OCaml.
I'd guess that a decent SMT solver will solve the "raw" expression much faster than running it through the simplifier and then solving it (with the same solver).
regards
Markus
[1] http://bes.forge.ocamlcore.org/--
On 2015-04-02 19:16, Kenneth Adam Miller wrote:
Is there a library somewhere where I can represent and simplify simple bit
operation expressions? Add, subtract, exclusive or, or, and, divide,
multiply, modulus, composed recursively, and operations on the expression
type, such as simplify?
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs