Skip to content

Releases: elsoroka/Satisfiability.jl

Release list

v0.2.0

v0.2.0 Latest
Latest

Choose a tag to compare

View all tags
@elsoroka elsoroka released this 21 Nov 17:10
v0.2.0
ca26317
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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

Assets 2
Loading

v0.1.2

v0.1.2

Choose a tag to compare

View all tags
@elsoroka elsoroka released this 28 May 21:17
v0.1.2
dd89b1b
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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

Contributors

mykelk
Loading

v0.1.1

v0.1.1

Choose a tag to compare

View all tags
@elsoroka elsoroka released this 17 Dec 00:43
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
Verified
Learn about vigilant mode.
  • 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.
Loading