Satisfiability.jl - v0.2.0

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

Scientific Software - Peer-reviewed - Julia
Published by elsoroka over 1 year ago

Satisfiability.jl - v0.2.0

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

Scientific Software - Peer-reviewed - Julia
Published by elsoroka over 1 year ago

Satisfiability.jl - v0.1.2

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

Scientific Software - Peer-reviewed - Julia
Published by elsoroka over 1 year ago

Satisfiability.jl - 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 toreal and toint are used to convert mixed IntExprs and RealExprs.

Scientific Software - Peer-reviewed - Julia
Published by elsoroka about 2 years ago