search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 233 forks source link

Support more than one SMT solver (Z3) #1

Closed sirinath closed 10 years ago

sirinath commented 10 years ago

Hi,

Is it possible to Open Source Z3 under ASL 2.0 so the whole F* stack is under ASL 2.0?

Suminda

nikswamy commented 10 years ago

No, Z3 is a separate tool and there are no plans currently to make it available under an Apache license. Z3 is free for academic use and you can also buy a commercial license.

You can, however, easily use F* with other SMT solvers that support the open standard smt2 input format (although, depending on the solver, your mileage may vary).

-nik

sirinath commented 10 years ago

Why don't you give some free solver option as well out of the box (which gets you full milage also)

nikswamy commented 10 years ago

Thanks for the suggestion. Can't promise, but we may do that. -Nik

sirinath commented 10 years ago

OK Great.

Framework like Why3 (http://why3.lri.fr/) and WhyML (http://why3.lri.fr/doc-0.80/manual004.html) support many backends out of the box. Taking similar route to support multiple backends would be great.

nikswamy commented 10 years ago

We are SMT2 compliant. Any solver that implements that interface will work, although it may or may not be able to prove as much/as fast as Z3.

sirinath commented 10 years ago

Great. Also is it possible to see if Z3 can also be open sourced with the new wave of open sourcing at MS