Latest builds

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.

New Features

• API

  • New API function Solver::mkFloatingPoint(const Term& sign, const Term& exp, const Term& sig), returns a floating-point value from the three IEEE-754 bit-vector value components.
  • 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.

• Support for timeout cores

  • API
    • New API function Solver::getTimeoutCore() when applicable returns a subset of the current assertions that cause the solver to timeout without a provided timeout (option --timeout-core-timeout).
  • SMT-LIB
    • New command (get-timeout-core) which invokes the above method.

• Support for new interfaces to the SyGuS solver.

  • API
    • New API function Solver::findSynth which takes an identifier specifying a target term to synthesize and (optionally) a grammar. This method can be used to directly enumerate terms in a provided grammar (FindSynthTarget::ENUM), or as a way of finding other terms of interest, e.g., a rewrite rule that is applicable to the current set of assertions (FindSynthTarget::REWRITE_INPUT).
    • New API function Solver::findSynthNext which gets the next term in the enumeration.
  • SMT-LIB
    • New commands find-synth and find-synth-next which invoke the above methods.

Changes

• Removed support for the ANTLR parser and parsing for the TPTP language.
• API
  • Simplified the Solver::mkTuple method. The sorts of the elements no longer need to be provided.
  • The option --print-unsat-cores-full has been renamed to --print-cores-full. Setting this option to true will print all assertions in the unsat core, regardless of whether they are named. This option also impacts how timeout cores are printed.
  • Removed API support for the deprecated SyGuS 2.0 command Solver::synthInv. This method is equivalent to Solver::synthFun
    with a Boolean range sort.

New Features

• A new (hand-written) parser is available and enabled by default.
  • Note that the previous ANTLR3-based parser can be enabled using command line options --no-flex-parser --no-stdin-input-per-line. These options will be available until version 1.1 is released.