Latest builds

New Features

• A build configuration safe-mode is available via our configure script
  which guards all cvc5 features that are either not robust or do not have
  full proof and model support. It is also possible to guard against these
  features using the command line option --safe-mode=safe. The definition
  of what is allowable in safe mode coincides with our fuzzing guidelines,
  see https://github.com/cvc5/cvc5/wiki/Fuzzing-cvc5.
• We have significantly increased coverage of proofs in the Cooperating Proof
  Calculus (CPC) proof format. In particular, we expect that CPC proofs are
  complete for all theories and features allowed in safe mode. These proofs
  may be obtained by the (get-proof) SMT-LIB command, or via the API using
  the method Solver::getProof, and are checkable by Ethos 0.2.0
  (./contrib/get-ethos-checker).
• We now support the SMT-LIB version 2.7 standard syntax for arithmetic
  bit-vector conversion functions whose smt2 syntax is int_to_bv, ubv_to_int
  and sbv_to_int. The first maps to the existing kind Kind::INT_TO_BITVECTOR.
  The kinds Kind::BITVECTOR_UBV_TO_INT and Kind::BITVECTOR_SBV_TO_INT
  are added to the API for the latter two. Note the syntax int2bv and bv2nat
  as well as the kind Kind::BITVECTOR_TO_NAT are now deprecated.

Changes

• Bumped CaDiCaL to version 2.1.3.
• The proof granularity is now dsl-rewrite by default. The regression test
  make regress-dsl-proof is deleted and is now equivalent to
  make regress-proof.
• Following the SMT-LIB standard, we now print parentheses around all proof
  outputs.
• The option --safe-options is renamed to --safe-mode=safe. We additionally
  support the option --safe-mode=stable, which disables experimental
  features but does not insist on complete proofs or models.
• The quantifier instatiation strategy --mbqi-fast-sygus has been renamed to
  --mbqi-enum.

New Features

• Updates to the cpc proof signature. The 0.1.1 release of Ethos can check
  proofs generated by this version of cvc5 (./contrib/get-ethos-checker).

• Increased coverage for proofs, in particular for theories allowed by
  --safe-options.

• Added support for SymbolManager::getNamedTerms() to retrieve the set of
  terms that have been given names by the SMT-LIB attribute :named.

• Added option --parsing-mode to allow configuration of both more strict but
  also more lenient parsing than default. Already existing option
  --strict-parsing is an alias --parsing-mode=strict.
  Parsing symbols that start with . or @ (used for internally freshly
  introduced symbols) in lenient parsing mode (--parsing-mode=lenient).

Changes

• The option --safe-options now disables experimental theories and their
  extensions in cvc5. This includes the theory of bags, the theory of finite
  fields, the theory of separation logic, higher-order extensions to the theory
  of equality, as well as extensions of the theory of arithmetic for
  transcendental functions, integer-and, and power functions, and the theory of
  arrays for constant arrays. These theories are still enabled by default and
  further more can be used in combination with safe options by the options e.g.
  --arith-exp prior to setting --safe-options.

• Renamed the flag --sets-ext to --sets-exp, which enables non-standard
  extensions of the sets theory.

• Fixed a soundness bug in the solver for set.filter.

• When printing with tags -o pre-asserts or -o post-asserts, by default we
  now ensure that declarations are printed in a deterministic order.

• Bumped CaDiCaL to version 2.0.0.

New Features

• New C API, implemented as a thin wrapper around the C++ API.

  • Documentation: https://cvc5.github.io/docs-ci/docs-main/api/c/c.html
  • Examples: https://github.com/cvc5/cvc5/tree/main/examples/api/c

• Exposed creation and maintenance of Skolem functions to the API. Skolem
  functions are symbols that are internally introduced by cvc5 during solving.
  They are formalized via an identifier (see
  https://cvc5.github.io/docs-ci/docs-main/skolem-ids.html for details) as well
  as a (possibly empty) set of indices.

  • The API methods Term::isSkolem(), Term::getSkolemId(), and
    Term::getSkolemIndices()may now be used to identify terms corresponding
    to skolems.

• We now export kinds BITVECTOR_FROM_BOOLS, BITVECTOR_BIT, DIVISION_TOTAL,
  INTS_DIVISION_TOTAL, INTS_MODULUS_TOTAL which may appear in terms
  resulting from simplification or terms appearing in proofs.

• Proof rules corresponding to rewrite rules are now exported in the API via
  the enum ProofRewriteRule.

• A new Plugin class is available in our API. This class allows a user
  to be notified when SAT clauses or theory lemmas are learned internally
  by cvc5. The plugin class also contains a callback for the user to introduce
  new learned clauses into the state of cvc5 during solving.

• Added a new strategy --mbqi-fast-sygus (disabled by default) for quantifier
  instantiation which uses SyGuS enumeration to augment instantiations from
  model-based quantifier instantiation.

Changes

• We now require CMake >= 3.16.

• API
  All APIs have been refactored to expose a TermManager to the API. A term
  manager manages creation and maintenance of all terms and sorts (across
  potentially several solver instances within a thread).
  Corresponding functions that were previously associated with a solver
  instance and are now associated with a term manager are now deprecated
  and will be removed in a future release.

  • Python:
    • Constructor SymbolManager(Solver) is now deprecated and replaced
      by SymbolManager(TermManager).
  • Pythonic:
    • Unsat cores and proofs are now available via the Solver methods
      unsat_core() and proof(), respectively.

• The default proof format of cvc5 has been renamed to the
  Cooperating Proof Calculus (CPC) proof format. This proof format coincides
  with proof objects in our API.

  • API
    • The option --proof-format=cpc prints proofs in the CPC format.
      This option is now enabled by default.
  • The Ethos proof checker is available, which can check proofs in this
    format. In particular, the 0.1.0 release of Ethos can check proofs generated
    by this version of cvc5. This checker is the second generation of the
    AletheLF checker (alfc). Ethos inherits the code base of alfc and is based
    on a logical framework called Eunoia (formerly called AletheLF).
    See https://github.com/cvc5/ethos for more details. Note that the
    development version of Ethos is available for download via the script
    ./contrib/get-ethos-checker, which will be kept in sync with further
    development versions of cvc5.
  • The rules of this format have been formalized in Eunoia and are available
    in the cvc5 repository under the directory ./proofs/eo/cpc/.

• The semantics of SQRT was changed to assume the result is positive.

• Fixed a bug involving how sequence terms are printed in model values.

New Features

• Added support for nullable sorts and lift operator to the theory of datatypes.
• Adds a new strategy --sub-cbqi (disabled by default) for quantifier
  instantiation which uses subsolvers to compute unsat cores of instantiations
  that are used in proofs of unsatisfiability.

Changes

• SAT clauses are no longer marked as removable in MiniSat. This change
  improves performance overall on quantifier-free logics with arithmetic and
  strings.
• API
  • Functions kindToString(Kind) and sortKindToString(SortKind) are now
    deprecated and replaced by std::to_string(Kind) and
    std::to_string(SortKind). They will be removed in the next minor release.
• Minor changes to the output format for proofs. Proofs in the AletheLF
  proof format generated by cvc5 now correspond directly to their representation
  in proof objects obtained in via the API (the Proof class). Moreover,
  proofs now use SMT-LIB compliant syntax for quantified formulas and unary
  arithmetic negation.
• The option --safe-options now disallows cases where more than one regular
  option is used.
• Fixes the parsing of define-fun-rec and define-funs-rec in interactive
  mode.
• Renamed bag.duplicate_removal to bag.setof.
• Improvements to handling of constant production rules (Constant) in SyGuS
  grammars.

New Features

• Added support for forward declarations (feature :fwd-decls) in SyGuS
  inputs. This allows functions-to-synthesize to include previous
  functions-to-synthesize in their grammars. This feature is enabled by default
  for all SyGuS inputs.

Changes

• Fixed a bug when piping input from stdin, which caused cvc5 to have degraded
  performance. This bug could also cause cvc5 to throw spurious parser errors.

New Features

• API

  • The signature of functions Solver::mkFiniteFieldSort(const std::string&)
    and Solver::mkFiniteFieldElem(const std::string&, const Sort&) is now
    extended with an additional (optional) parameter to
    Solver::mkFiniteFieldSort(const std::string& size, uint32_t base) and
    Solver::mkFiniteFieldElem(const string& value, const Sort& sort, uint32_t base)
    to configure the base of the string representation of the given string
    parameters.
  • A new API for proofs is available. The new Proof class represents a node
    of the proof tree. Function
    Solver::getProof(modes::ProofComponent c = modes::ProofComponent::FULL)
    returns the root proof nodes of a proof component as a vector. Function
    Solver::proofToString(std::vector<Proof> proof, modes::ProofFormat format, modes::ProofComponent component)
    can be used to print proof components to a string with a specified proof
    format.
  • Added support for parsing inputs from file, string, or input stream. We
    provide an InputParser, SymbolManager, and Command class for reading
    inputs (see include/cvc5_parser.h). Example use cases of these classes
    are available at https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser.html
    and https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser_sym_manager.html.
    These interfaces are also available in the Java and Python APIs.
  • Added a variant of timeout cores that accepts a set of assumptions. This
    is available via the API method Solver::getTimeoutCoreAssuming or the
    SMT-LIB command get-timeout-core-assuming, which accept a list of
    formulas to assume, while all current assertions are implicitly included
    in the core.
  • Add new method Solver::getUnsatCoreLemmas which returns the set of theory
    lemmas that were relevant to showing the last query was unsatisfiable. This
    is also avialable via the SMT-LIB command get-unsat-core-lemmas.

• Support for the AletheLF (ALF) proof format. This format combines the
  strengths of the Alethe and LFSC proof formats, namely it borrows much of the
  syntax of Alethe, while being based on a logical framework like LFSC.

  • API
    • The option --proof-format=alf prints proofs in the AletheLF format.
      This option is enabled by default.
  • The ALF proof checker (alfc) is available for download via the script
    ./contrib/get-alf-checker.

• CaDiCaL is now integrated via the IPASIR-UP interface as CDCL(T) SAT
  solver. The CDCL(T) SAT solver can be configured via option --sat-solver.
  Currently, MiniSat is still default. Note that CaDiCaL cannot be used as the
  CDCL(T) SAT engine when proof production is enabled. In that case, option
  --sat-solver will default back to MiniSat.

Changes

• Various bug fixes.

Note This version is a pre-release for upcoming version 1.1.0.

New Features

• API
  • Added support for querying the values of real algebraic numbers in the API. In particular, the methods Term::isRealAlgebraicNumber(), Term::getRealAlgebraicNumberDefiningPolynomial(), Term::getRealAlgebraicNumberLowerBound(), and Term::getRealAlgebraicNumberUpperBound() may now be used to query the contents of terms corresponding to real algebraic numbers.

Note This version is a pre-release for upcoming version 1.1.0.

Changes

• API
  • C++ enums are now enum classes
  • Added argument fresh to Solver::declareFun which distinguishes whether the solver should construct a new term or (when applicable) return a term constructed with the same name and sort. An analogous flag is added to Solver::declareSort. The option --fresh-declarations determines whether the parser constructs fresh terms and sorts for each declaration (true by default, which matches the previous behavior).

• Various bug fixes.