From 6b5961ac1eaff2fa0123d6634b7d53d96da13f22 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 26 Jul 2019 15:47:24 -0700 Subject: [PATCH] update readme Signed-off-by: Nikolaj Bjorner --- README.md | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index d5a343bb8..060bb9d5a 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Z3 -Z3 is a theorem prover from Microsoft Research. It is licensed -under the [MIT license](LICENSE.txt). +Z3 is a theorem prover from Microsoft Research. +It is licensed under the [MIT license](LICENSE.txt). If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background). @@ -194,3 +194,21 @@ See [``examples/python``](examples/python) for examples. ### ``Web Assembly`` [WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel. + +## System + +[!System Diagram](https://github.com/Z3Prover/doc/blob/master/programmingz3/images/Z3Overall.jpg) + +## Resources + +* Default input format is [SMTLIB2](/http://smtlib.cs.uiowa.edu) + +* Other native foreign function interfaces: + * C + * C++ + * Python + * Java + * C# + * OCaml + +