Fix Bugs and Make Z3 easier to Use

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`

slm.toml

@@ -1,6 +1,6 @@
 
 name = "slm-z3"
-version = "0.1.1"
+version = "0.2.0"
 
 [dependencies]
 

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
+

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

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<Context>
@@ -68,6 +69,6 @@ public lostanza defn serialize-to-string (g:ref<Goal>) -> ref<String> :
   val ret = w_Z3_goal_to_string(g.ctx.value, g.value)
   return String(ret)
 
-public lostanza defn serialize-to-DIMACS-string (g:ref<Goal>) -> ref<String> :
-  val ret = w_Z3_goal_to_dimacs_string(g.ctx.value, g.value)
+public lostanza defn serialize-to-DIMACS-string (g:ref<Goal>, include-names:ref<True|False>) -> ref<String> :
+  val ret = w_Z3_goal_to_dimacs_string(g.ctx.value, g.value, to-byte(include-names))
   return String(ret)

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
+
+
+
+
+
+
+
+
+
+
+
+
+
+