diff --git a/Project.toml b/Project.toml index ccb6c2c..449c87b 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "Satisfiability" uuid = "160ab843-0bc6-4ba4-9585-b7478b70f443" authors = ["Emi Soroka , Mykel Kochenderfer, Sanjay Lall"] -version = "0.1.0" +version = "0.1.1" [compat] julia = "1" diff --git a/README.md b/README.md index 14d1404..3c49b36 100644 --- a/README.md +++ b/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. diff --git a/docs/make.jl b/docs/make.jl index ebe33a7..f4332cc 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -33,7 +33,8 @@ pages = [ ], "Library" => [ "functions.md" - ] + ], + "release_notes.md" ], format=fmt, ) diff --git a/docs/src/release_notes.md b/docs/src/release_notes.md new file mode 100644 index 0000000..4d7f3e9 --- /dev/null +++ b/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.