Skip to content
This repository has been archived by the owner on May 7, 2021. It is now read-only.
/ CVC4-archived Public archive

Releases: CVC4/CVC4-archived

CVC4 1.8

05 May 18:11
@mpreiner mpreiner
1.8
5247901
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
CVC4 1.8 Latest
Latest

Changes since 1.7

New Features:

  • New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
    make CVC4 1.8 the last version that ships with the legacy API.
  • Strings: Full support of the new SMT-LIB standard for the theory of strings,
    including:
    • Support for str.replace_re, str.replace_re_all, str.is_digit,
      str.from_code, re.diff, and re.comp
    • Support for new operator names (e.g. str.in_re instead of str.in.re),
      new escape sequences. The new syntax is enabled by default for smt2 files.
  • Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
    examples of the SyGuS API can be found in ./examples/api/sygus_*.cpp.
  • Support for higher-order constraints. This includes treating function sorts
    (constructible by ->) as first-class sorts and handling partially applied
    function symbols. Support for higher-order constraints can be enabled by
    the option --uf-ho.
  • Support for set comprehension binders comprehension.
  • Eager bit-blasting: Support for SAT solver Kissat.

Improvements:

  • API: Function definitions can now be requested to be global. If the global
    parameter is set to true, they persist after popping the user context.
  • Java/Python bindings: The bindings now allow users to catch exceptions
  • Arithmetic: Performance improvements
    • Linear solver: New lemmas inspired by unit-cube tests
    • Non-linear solver: Expanded set of axioms
  • Ackermannization: The Ackermannization preprocessing pass now supports
    uninterpreted sorts and as a result all QF_UFBV problems are supported in
    combination with eager bit blasting.

Changes:

  • CVC language: Models printed in the CVC language now include an explicit end
    marker to facilitate the communication over pipes with CVC4.
  • API change: SmtEngine::query() has been renamed to
    SmtEngine::checkEntailed() and Result::Validity has been renamed to
    Result::Entailment along with corresponding changes to the enum values.
  • Java API change: The name of CVC4's package is now edu.stanford.CVC4
    instead of edu.nyu.acsys.CVC4.
  • The default output language is changed from CVC to SMT-LIB 2.6. The
    default output language is used when the problem language cannot be
    easily inferred (for example when CVC4 is used from the API).
  • Printing of BV constants: previously CVC4 would print BV constant
    values as indexed symbols by default and in binary notation with the
    option --bv-print-consts-in-binary. To be SMT-LIB compliant the
    default behavior is now to print BV constant values in binary
    notation and as indexed symbols with the new option
    --bv-print-consts-as-indexed-symbols. The option
    --bv-print-consts-in-binary has been removed.
  • Updated to SyGuS language version 2.0 by default. This is the last release
    that will support the SyGuS language version 1.0 (--lang=sygus1). A
    script is provided to convert version 1.0 files to version 2.0, see
    ./contrib/sygus-v1-to-v2.sh.
  • Support for user-provided rewrite rule quantifiers have been removed.
  • Support for certain option aliases have been removed.
  • Support for parallel portfolio builds has been removed.
Assets 5
Loading