From 1b635766cf95e7fbe3229ada6a2b77fe601316ef Mon Sep 17 00:00:00 2001 From: Carl Allendorph Date: Fri, 28 Jun 2024 21:12:54 -0700 Subject: [PATCH 1/4] [Bugfix] Fixed missing import and invalid function call --- src/Goals.stanza | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Goals.stanza b/src/Goals.stanza index 04fa84c..42124ab 100644 --- a/src/Goals.stanza +++ b/src/Goals.stanza @@ -4,6 +4,7 @@ defpackage z3/Goals : import z3/Context import z3/Utils import z3/AST + import z3/Enums public lostanza deftype Goal : ctx:ref @@ -68,6 +69,6 @@ public lostanza defn serialize-to-string (g:ref) -> ref : val ret = w_Z3_goal_to_string(g.ctx.value, g.value) return String(ret) -public lostanza defn serialize-to-DIMACS-string (g:ref) -> ref : - val ret = w_Z3_goal_to_dimacs_string(g.ctx.value, g.value) +public lostanza defn serialize-to-DIMACS-string (g:ref, include-names:ref) -> ref : + val ret = w_Z3_goal_to_dimacs_string(g.ctx.value, g.value, to-byte(include-names)) return String(ret) From 8a71fcfd42d22b222004c03815b3d40e1aa89ad1 Mon Sep 17 00:00:00 2001 From: Carl Allendorph Date: Fri, 28 Jun 2024 21:18:12 -0700 Subject: [PATCH 2/4] Updated the top level z3.stanza to make import easier. This updates the z3.stanza to forward all packages in the library so that we can more easily use this in an application. User should be able to just run: ``` import z3 ``` And access all symbols now. --- src/AST.stanza | 11 +++++++++++ src/Enums.stanza | 12 ++++++++++++ src/z3.stanza | 38 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+) create mode 100644 src/AST.stanza create mode 100644 src/Enums.stanza diff --git a/src/AST.stanza b/src/AST.stanza new file mode 100644 index 0000000..3c8cb70 --- /dev/null +++ b/src/AST.stanza @@ -0,0 +1,11 @@ +defpackage z3/AST: + forward z3/AST/AST + forward z3/AST/BVOps + forward z3/AST/Complex + forward z3/AST/Functions + forward z3/AST/Numerals + forward z3/AST/Operators + forward z3/AST/Quantifiers + forward z3/AST/Sets + forward z3/AST/Vector + diff --git a/src/Enums.stanza b/src/Enums.stanza new file mode 100644 index 0000000..8b689c1 --- /dev/null +++ b/src/Enums.stanza @@ -0,0 +1,12 @@ +defpackage z3/Enums: + forward z3/Enums/Z3_ast_kind + forward z3/Enums/Z3_ast_print_mode + forward z3/Enums/Z3_decl_kind + forward z3/Enums/Z3_error_code + forward z3/Enums/Z3_goal_prec + forward z3/Enums/Z3_lbool + forward z3/Enums/Z3_param_kind + forward z3/Enums/Z3_parameter_kind + forward z3/Enums/Z3_search_failure + forward z3/Enums/Z3_sort_kind + forward z3/Enums/Z3_symbol_kind \ No newline at end of file diff --git a/src/z3.stanza b/src/z3.stanza index 6595aeb..6e59ba2 100644 --- a/src/z3.stanza +++ b/src/z3.stanza @@ -3,3 +3,41 @@ defpackage z3: import collections forward z3/Context + + ; This is not working yet. + ; forward z3/Algebraic + forward z3/Constrainable + forward z3/DataTypes + forward z3/EnumSort + forward z3/Errors + forward z3/Goals + forward z3/ListSort + forward z3/Misc + forward z3/Model + forward z3/Optimize + forward z3/Parameters + forward z3/Probes + forward z3/Shellable + forward z3/Solver + forward z3/Sorts + forward z3/Statistics + forward z3/Symbols + forward z3/Tactics + forward z3/TupleSort + forward z3/Utils + forward z3/AST + forward z3/Enums + + + + + + + + + + + + + + From 155953c54c436274bc7235eeda57dfd260a6ba37 Mon Sep 17 00:00:00 2001 From: Carl Allendorph Date: Tue, 2 Jul 2024 20:43:17 -0700 Subject: [PATCH 3/4] Updated the README for the current state of the build. --- README.md | 39 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 335eeef..55cd2e8 100644 --- a/README.md +++ b/README.md @@ -47,10 +47,43 @@ Vin -> 24.0 Where R2 = 100k / 3.0 == 33.3k. This creates a voltage divider with an output of 6.0V when there is an input of 24V. -# Setup +# How to use in JITX -This project uses [conan](https://conan.io/) to manage compiling the Z3 library dependency for -the current platform. To build the Z3 dependencies: +Add the following to your `slm.toml` file: + +``` +[dependencies.slm-z3] +pkg="slm-z3" +version="0.1.1" +type="conan" +options.shared = "True" +options.linux.fPIC = "True" +options.macos.fPIC = "True" +``` + +Then run `$SLM clean`. On next build, the dependency will be downloaded and you will be able to `import z3` to use in your project. + +# Dev Setup + +This project uses [conan](https://conan.io/) to manage compiling the Z3 library dependency for the current platform. + +Currently the process is: + +1. Create a venv and install the dependencies + 1. `python -m venv venv` + 2. `source venv/bin/activate` + 3. `pip install -r requirements.txt` +2. Run Conan using the `Makefile` + 1. `make` + +This will construct a conan package that includes the stanza wrappers around Z3 +and will download the `Z3` library dependency when installed with `slm` + +NOTE: The unit tests currently cannot be run because the conan package build only provides the shared library versions. This leaves no method to build the tests and run them. + +**OLD instructions** + +To build the Z3 dependencies: 1. Setup a compiler on the `$PATH` 1. Ubuntu: `sudo apt install build-essential` From aac2b5fe47e1ef24aaa62cf105d3b3a996656932 Mon Sep 17 00:00:00 2001 From: Carl Allendorph Date: Tue, 2 Jul 2024 20:44:21 -0700 Subject: [PATCH 4/4] [Bump] Increment to version 0.2.0 --- slm.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/slm.toml b/slm.toml index cb154bc..9c67372 100644 --- a/slm.toml +++ b/slm.toml @@ -1,6 +1,6 @@ name = "slm-z3" -version = "0.1.1" +version = "0.2.0" [dependencies]