Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Z3: A high-performance theorem prover from Microsoft Research

z3.codeplex.com

Post reply on HN
Print view View original

21–30 of 50 posts

Re: Z3: A high-performance theorem prover from Microsoft Research

#21

Post by microarchitect »

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving.

If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394. To make a long story short, various problems in program verification and static analysis have seen success with SMT.

/some academic navel-gazing follows.

Yices (http://yices.csl.sri.com/index.shtml) and Z3 are the two main SMT solvers used by academics today. Yices is the "original" solver and was developed by Leonardo de Moura and Bruno Dutertre at SRI in the mid-2000s. At some point towards the end of the last decade, Leonardo moved to Microsoft Research and for reasons which are unclear started working on Z3 independently. I am told that Z3 is a slightly faster solver today.

Re: Z3: A high-performance theorem prover from Microsoft Research

#22

Post by randomhunt »

DannyBee wrote: post #20
randomhunt wrote: post #13

Earlier quoted context omitted.

Commercial = I make money from using this; Non-commercial = NOT commercial (In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)

"Commercial = I make money from using this; Non-commercial = NOT commercial " False. There are cases where commercial was held to mean "any use by a for profit company, regardless if the use is research, earns money directly or indirectly", etc.

Admittedly with a European viewpoint, either common law based (UK) or administrative law based (France, Belgium), there have been cases where commercial was held to mean has the company benefited in a tangible way from its use of such licenced software.

Although if you speak to a lawyer I'm sure their training would immediately start highlighting this as a concern I don't believe it should be in the vast majority of cases. Wasn't there an article on HN a few days ago basically summarising this type of concern under "so sue me" (minus expletives)

Re: Z3: A high-performance theorem prover from Microsoft Research

#23

Post by randomhunt »

barrkel wrote: post #19
randomhunt wrote: post #13

Earlier quoted context omitted.

Commercial = I make money from using this; Non-commercial = NOT commercial (In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)

What if you don't make money from it now, but use what you learned to profit ten minutes later? How about 10 days later? Or 10 years later? Non-commercial use for something that is directly involved in the production of something else is fairly easy to determine; it depends on whether that something else is sold for money or not. But for analytical software like this prover, you could indirectly use it to improve som…

Is there a direct link between you using this software under such a licence and then gaining monetary advantage (if not money directly itself)?

Using your process of improvement for me it is quite clear there would be.

[Perhaps the solver could be used to figure the applicability of the licence]

Re: Z3: A high-performance theorem prover from Microsoft Research

#24

Post by wisty »

randomhunt wrote: post #13
vdaniuk wrote: post #8

Earlier quoted context omitted.

Yeah, I got that first time, thanks. It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?

Commercial = I make money from using this; Non-commercial = NOT commercial (In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)

So if you make money by teaching, is that commercial?

Non-commercial is a terrible term, because it's simply too vague. You can simply say "well, MS will use a bit of discretion, and not sue someone for a marginal infringement". But it does feel a little dodgy.

Re: Z3: A high-performance theorem prover from Microsoft Research

#25

Post by throwaway812 »

colanderman wrote: post #17
tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

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…

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

Re: Z3: A high-performance theorem prover from Microsoft Research

#26

Post by MichaelSalib »

colanderman wrote: post #17
tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

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…

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.

Re: Z3: A high-performance theorem prover from Microsoft Research

#27

Post by colanderman »

throwaway812 wrote: post #25
colanderman wrote: post #17

Earlier quoted context omitted.

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…

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

Sure, I see no reason to keep it private: 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.

Re: Z3: A high-performance theorem prover from Microsoft Research

#28

Post by colanderman »

MichaelSalib wrote: post #26
colanderman wrote: post #17

Earlier quoted context omitted.

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…

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.

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

Re: Z3: A high-performance theorem prover from Microsoft Research

#29

Post by colanderman »

tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

Another reply (can't edit my original reply now): what I have not done, though will if I ever have the chance again, is to prove correctness of bit-arithmetic libraries (e.g. for use with symbolic execution).

So long as you can represent your function in the SMT-LIB language (easy for this class of problem), you can prove properties of your code by asserting their respective negations in Z3 and asking it to prove satisfiability. If one of these properties doesn't hold, Z3 will tell you, and it will give you an example.

Post reply on HN