Skip to content

Releases: elsoroka/Satisfiability.jl

v0.2.0

21 Nov 17:10
@elsoroka elsoroka
v0.2.0
ca26317
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.
Compare
Choose a tag to compare
v0.2.0 Latest
Latest

Support Unicode variable names.
Add experimental support for 3D tensor variables.

Assets 2
Loading

v0.1.2

28 May 21:17
@elsoroka elsoroka
v0.1.2
dd89b1b
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.
Compare
Choose a tag to compare
v0.1.2

If Z3 is not already installed, automatically install it when users install Satisfiability.jl. Credit to @mykelk for this improvement :)

Contributors

mykelk
Assets 2
Loading

v0.1.1

17 Dec 00:43
@elsoroka elsoroka
Releases
0322f6f
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v0.1.1
  • 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 IntExprs and RealExprs.
Assets 2
Loading