5 ms·

Last week I wrote a fun tool using it (actually, any SMT-LIB 2 compatible solver, of which Z3 seems to be the only open-source-ish one that works out of the box

Last week I wrote a fun tool using it (actually, any SMT-LIB 2 compatible solver, of which Z3 seems to be the only open-source-ish one that works out of the box) to search for optimal branch-free load-free C implementations of small integer lookup tables (i.e. something the compiler should do but doesn't). It's really a minimal use of an SMT solver, but it saved me from having to think of a more clever algorithm than brute force.

MichaelSalib 13y ago
I'd also love to see this; or, if it would be easier for you, I'd love to see a longer comment where you explain it in more detail.
- colanderman 13y ago
  See my reply to throwaway812 (which I'm updating with an explanation).
throwaway812 13y ago
Did you publish the source anywhere, and if not, are you willing and able to? I'd love to see it.
- colanderman 13y ago
  Sure, I see no reason to keep it private: http://hub.darcs.net/squirrel/luts http://hub.darcs.net/squirrel/luts (Note: it's a very hacked-together Prolog script. I wrote it in about 15 minutes in a fit of inspiration and free time. If it's useful to anyone I'll clean it up and add the features I enumerated in the README.) How it works: The input to the algorithm is the look-up table you want to optimize. I've mostly tested with a half-dozen or so pairs of small (1 or 2 digit) integers, as that is my use case. (Anything else is probably better served by an actual look-up table or binary branch tree.) Input values left out of the this table are considered "don't care" (i.e. there's no "default" output). The Prolog portion just generates, via iterative-deepening, bit-arithmetic expressions. These expressions have as terminals the input variable (in theory, there could be multiple input variables; haven't tried this) and arbitrary (i.e. symbolic) named constants. The expressions are, in turn, fed as-is to Z3 as a function over bit-vectors (note the constants are still arbitrary). The look-up table is fed to Z3 as a set of assertions about this function. Z3 is asked to prove (un)satisfiability; if the problem is satisfiable, (this is the important part!) it returns the values of the constants which make it satisfiable. These values are substituted in the original expression, which is then returned by the Prolog script as a solution.
psuter 13y ago
In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices. [1] http://cvc4.cs.nyu.edu/ http://cvc4.cs.nyu.edu/
- colanderman 13y ago
  Thanks! Last I checked (maybe a year back), something-or-other about CVC4 didn't work for me (I wholly forget what it was). I will try it out again. I don't know if you are associated with CVC4 at all, but unfortunately the hashes of the amd64 Debian stable packages (cvc4, libcvc4-1, and libcvc4parser1) don't seem to match? It is probably just a package error however it makes me hesitant to install the packages…
  - psuter 13y ago
    I am not associated with CVC4 directly (or Z3 for that matter). Something that is true for all these tools is that they evolve very quickly. As a result, you're better off building from source. In both cases, that means running `make` and nothing else.

MichaelSalib 13y ago

I'd also love to see this; or, if it would be easier for you, I'd love to see a longer comment where you explain it in more detail.

colanderman 13y ago
See my reply to throwaway812 (which I'm updating with an explanation).

throwaway812 13y ago

Did you publish the source anywhere, and if not, are you willing and able to? I'd love to see it.

colanderman 13y ago
Sure, I see no reason to keep it private: http://hub.darcs.net/squirrel/luts http://hub.darcs.net/squirrel/luts (Note: it's a very hacked-together Prolog script. I wrote it in about 15 minutes in a fit of inspiration and free time. If it's useful to anyone I'll clean it up and add the features I enumerated in the README.) How it works: The input to the algorithm is the look-up table you want to optimize. I've mostly tested with a half-dozen or so pairs of small (1 or 2 digit) integers, as that is my use case. (Anything else is probably better served by an actual look-up table or binary branch tree.) Input values left out of the this table are considered "don't care" (i.e. there's no "default" output). The Prolog portion just generates, via iterative-deepening, bit-arithmetic expressions. These expressions have as terminals the input variable (in theory, there could be multiple input variables; haven't tried this) and arbitrary (i.e. symbolic) named constants. The expressions are, in turn, fed as-is to Z3 as a function over bit-vectors (note the constants are still arbitrary). The look-up table is fed to Z3 as a set of assertions about this function. Z3 is asked to prove (un)satisfiability; if the problem is satisfiable, (this is the important part!) it returns the values of the constants which make it satisfiable. These values are substituted in the original expression, which is then returned by the Prolog script as a solution.

psuter 13y ago

In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices. [1] http://cvc4.cs.nyu.edu/ http://cvc4.cs.nyu.edu/

colanderman 13y ago
Thanks! Last I checked (maybe a year back), something-or-other about CVC4 didn't work for me (I wholly forget what it was). I will try it out again. I don't know if you are associated with CVC4 at all, but unfortunately the hashes of the amd64 Debian stable packages (cvc4, libcvc4-1, and libcvc4parser1) don't seem to match? It is probably just a package error however it makes me hesitant to install the packages…
- psuter 13y ago
  I am not associated with CVC4 directly (or Z3 for that matter). Something that is true for all these tools is that they evolve very quickly. As a result, you're better off building from source. In both cases, that means running `make` and nothing else.