Skip to content

JKind v3.0
Compare
Choose a tag to compare
@agacek agacek released this 21 Mar 16:05
· 194 commits to master since this release
v3.0
89c34de

The big focus of JKind v3.0 is bundling and ease-of-use. The default solver has changed from Yices to SMTInterpol. This means users will no longer need to install an SMT solver by default. In addition, JKindApi has been updated to make it possible to bundle JKind into existing applications. Tools like AGREE, Spear, and JKind-Xtext have been updated to bundle JKind. Thus tool users won't need to install JKind or any SMT solvers. Everything will work out of the box.

Other notes

  • Added LustreParseUtil to allow JKindApi users to specify ASTs using concrete syntax together with substitutions for variables.
  • Error messages about the input Lustre now display and highlight the relevant portion of the input file.
  • "Set of support" has been renamed to "inductive validity core." This now uses the annotation --%IVC and the flag -ivc.
  • Enabled smoothing for Z3.
  • Shell scripts now work on Linux and OS X (Thanks to Dave Greve).
  • BigFraction.doubleValue() is now stable for large fractions (Thanks to Dave Greve).
  • Added EquationBuilder.
  • Added JLustre2ExcelApi.
Assets 3
Loading