Skip to content

JavaSMT v1.0.1
Compare
Choose a tag to compare
@cheshire cheshire released this 25 Aug 15:39
· 3453 commits to master since this release
1.0.1
This tag was signed with the committer’s verified signature.
cheshire George Karpenkov
GPG key ID: 4409A54039D4B02F
Learn about vigilant mode.
ad1a628

Changes since 0.60:

  • New package structure
    • Root package is java_smt
    • Solver bindings are in the package java_smt/solvers
    • User-facing API is in the package java_smt/api, apart from the entry
      point SolverContextFactory
  • New solver versions:
    • Z3: 4.4.1-1558-gf96cfea
    • MathSAT: 5.3.12, compiled with GMP6.1.1 with enable-fat option
    • OptiMathSAT: 1.4.0
    • Princess: 2016-06-27-r2652
  • Floating point rounding mode can be now specified for all operations in
    FloatingPointFormulaManager.
    Additionally, default rounding mode can be set using an option
    solver.floatingPointRoundingMode.
  • Automatic boolean formula simplification for Z3.
  • New utils package, with optional utilities. Includes:
    • UfElimination class for performing Ackermannization and returning the
      metadata describing the fresh variables.
  • modularCongruence method was moved to IntegerFormulaManager and now
    throws an exception on non-positive input.
  • Caching and statistics are moved to the statistics branch.
  • Better cancellation handling for Z3
  • Add makeTrue() and makeFalse() methods to BooleanFormulaManager
  • Added Ackermannization tactic.
Assets 2
Loading