3 ms·

Z3py (Z3 bindings for Python) is a much better interface for Z3 IMO. http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm http://www.cs.tau.ac.i

Z3py (Z3 bindings for Python) is a much better interface for Z3 IMO. http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examp...

MereInterest 10y ago
And an amazing example of why operator overloading is not the evil that people make it out to be.
- rdtsc 10y ago
  I don't know why you've been downvoted. The interface does look neat. They did a good job with it. Other example of such thing is Numberjack -- a constraint solve with multiple backends: http://numberjack.ucc.ie/ http://numberjack.ucc.ie/ Here is a send-more-money example solved in it: http://numberjack.ucc.ie/examples/sendmoremoney http://numberjack.ucc.ie/examples/sendmoremoney Sudoku: https://github.com/eomahony/Numberjack/blob/master/examples/Sudoku.py https://github.com/eomahony/Numberjack/blob/master/examples/...
eggy 10y ago
I like the Lisp/Scheme syntax better, but that is because I have studied Lisps far longer than Python, and I just find them easier for phrasing logic. The Python looks clean and familiar too. F* the theorem-proving, program-verification language from MS is ML-like, and exports to OCaml and F#. Can the Z3 SMT solver be used for F*'s SMT needs? I haven't found a link yet.
- ergl 10y ago
  Yes, afaik F* uses Z3 internally. I don't have any links, but I know a guy working on formalizing the translation from F* to Z3
  - eggy 10y ago
    I guess since F* is similar to F# or ML you could have a pretty cohesive solver to production toolchain. Having OCaml as an output option is great too. I was looking at Idris with the C backend as a way of formalizing my programming for production programming. This makes another set to evaluate before deciding. I realize they are quite different, but I am just experimenting at this moment.
- pron 10y ago
  Z3 (as well as other SMT solvers) is used by TLA+ (also MSR)

MereInterest 10y ago

And an amazing example of why operator overloading is not the evil that people make it out to be.

rdtsc 10y ago
I don't know why you've been downvoted. The interface does look neat. They did a good job with it. Other example of such thing is Numberjack -- a constraint solve with multiple backends: http://numberjack.ucc.ie/ http://numberjack.ucc.ie/ Here is a send-more-money example solved in it: http://numberjack.ucc.ie/examples/sendmoremoney http://numberjack.ucc.ie/examples/sendmoremoney Sudoku: https://github.com/eomahony/Numberjack/blob/master/examples/Sudoku.py https://github.com/eomahony/Numberjack/blob/master/examples/...

eggy 10y ago

I like the Lisp/Scheme syntax better, but that is because I have studied Lisps far longer than Python, and I just find them easier for phrasing logic. The Python looks clean and familiar too. F* the theorem-proving, program-verification language from MS is ML-like, and exports to OCaml and F#. Can the Z3 SMT solver be used for F*'s SMT needs? I haven't found a link yet.

ergl 10y ago
Yes, afaik F* uses Z3 internally. I don't have any links, but I know a guy working on formalizing the translation from F* to Z3
- eggy 10y ago
  I guess since F* is similar to F# or ML you could have a pretty cohesive solver to production toolchain. Having OCaml as an output option is great too. I was looking at Idris with the C backend as a way of formalizing my programming for production programming. This makes another set to evaluate before deciding. I realize they are quite different, but I am just experimenting at this moment.
pron 10y ago
Z3 (as well as other SMT solvers) is used by TLA+ (also MSR)