Merge pull request #29 from elsoroka/dev

Release v0.1.1 with improvements and bugfixes

Project.toml

@@ -1,7 +1,7 @@
 name = "Satisfiability"
 uuid = "160ab843-0bc6-4ba4-9585-b7478b70f443"
 authors = ["Emi Soroka <[email protected]>, Mykel Kochenderfer, Sanjay Lall"]
-version = "0.1.0"
+version = "0.1.1"
 
 [compat]
 julia = "1"

README.md

@@ -75,4 +75,4 @@ println(status) # if status is UNSAT we proved it.
 ```
 
 ## Development status
-Release 0.1.0 is out! You can install it with the command `using Pkg; Pkg.add("Satisfiability")`. Please help make the Julia ecosystem better for everyone by opening a GitHub issue if you have feedback or find a bug.
+Release 0.1.1 is out! You can install it with the command `using Pkg; Pkg.add("Satisfiability")`. Please help make the Julia ecosystem better for everyone by opening a GitHub issue if you have feedback or find a bug.

docs/make.jl

@@ -33,7 +33,8 @@ pages = [
         ],
         "Library" => [
         "functions.md"
-        ]
+        ],
+        "release_notes.md"
     ],
 format=fmt,
 )

docs/src/release_notes.md

@@ -0,0 +1,13 @@
+# Release Notes
+```@contents
+Pages = ["release_notes.md"]
+Depth = 3
+```
+# Version 0.1.1 (December 15, 2023)
+* Fixed bugs in issues #21 and #26.
+* Added remaining operators defined in SMT-LIB QF_BV (bitvector) specification (issue #22)
+* Add `^` for square
+* Correctly promote expressions containing mixed `BoolExpr`, `IntExpr` and `RealExpr` types. When a Boolean variable `z` is used in an arithmetic expression, it is rewritten to `ite(z 1 0)` (int) or `ite(z 1.0 0.0)` (real), which matches Z3's behavior. The SMT-LIB functions `to_real` and `to_int` are used to convert mixed `IntExpr`s and `RealExpr`s.
+
+# Version 0.1.0 (August 27, 2023)
+Initial release.