Skip to content

v0.9.0.0

Latest
Latest
Compare
Choose a tag to compare
@lsrcz lsrcz released this 08 Nov 00:21
· 4 commits to main since this release
v0.9.0.0
9413cac
This commit was signed with the committer’s verified signature.
lsrcz Sirui Lu
GPG key ID: 04D53E80A856B56F
Learn about vigilant mode.

Added

  • Added missing instances for concrete general and tabular functions. (#249)
  • Added eval mode constraint on demand. (#250)
  • Added support for uninterpreted functions in unified interfaces. (#250)
  • Added instances for concrete Ratio type. (#251)
  • Added serialization for the core constructs. (#253)
  • Added partial evaluation for distinct. (#254)

Changed

  • [Breaking] Moved the constraints for the general and tabular functions and
    simplified their instances declaration. (#249)
  • [Breaking] Renamed EvalMode to EvalModeAll, renamed MonadWithMode to
    MonadEvalModeAll. (#250)
  • Improved parallel symbolic evaluation performance. (#252)
  • [Breaking] Changed the metadata for identifiers from existential arguments to
    s-expressions. (#253)
  • [Breaking] Changed the solving/cegis results from maintaining the exception
    themselves to maintaining a textual representation of them. (#253)
  • [Breaking] Changed the 'VerifierResult' type for CEGIS to allow it report that
    the verifier cannot find a counter example. (#257)

Fixed

  • Fixed memory leak within the term cache. (#252)
  • Fixed printing of bv terms. (#255)
  • Fixed solverGenericCEGIS and make it also return the last failing cex. (#256)
  • solverGenericCEGIS will only rerun possible verifiers now. This will improve
    overall verification performance. (#258)
  • Fixed a critical bug in the lowering/evalSym/extractSym where the
    intermediate states are not properly memoized. (#259)
Assets 2
Loading