An interface like the web one.

Z3Prover / z3

The Z3 Theorem Prover

Other

10.29k stars 1.48k forks source link

An interface like the web one. #883

Closed k53sc closed 5 years ago

k53sc commented 7 years ago

Hi All,

Hope you all are doing well, Is there any way I can build Z3 interface like the one at http://rise4fun.com/z3/ locally at my machine, I understand there are Python and C++ etc binding but I find that while debugging in ( C++ ) It would be really helpful if we can copy paste Z3 statements ( declare-fun, assert ) and reproduce a situation.

Thanks for reading. Ayush

wintersteiger commented 7 years ago

If you use Python for other tasks, you may find it easy to use that API (see e.g. here).

Personally, I use emacs to edit SMT2 files with a customized smtlib mode. There are multiple other emacs interfaces, but I didn't try those yet (e.g. this, which also comes via MELPA package). These also allow you to run the solver within emacs, with error highlighting, etc.

NikolajBjorner commented 5 years ago