Skip to content

NEWS.md

Latest commit

 

History

History
630 lines (484 loc) · 25.2 KB

NEWS.md

File metadata and controls

630 lines (484 loc) · 25.2 KB

This file contains a summary of important user-visible changes.

New Features

  • 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.

cvc5 1.2.1

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.

cvc5 1.2.0

New Features

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

  • 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.

cvc5 1.1.2

New Features

  • Added support for nullable sorts and lift operator to the theory of datatypes.

  • Added 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.

  • Add support for the kind BITVECTOR_NEGO corresponding to bitvector negation overflow detection.

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.

cvc5 1.1.1

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.

cvc5 1.1.0

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.
    • Added 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.

cvc5 1.0.9

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

New Features

  • API
    • Added the ability to query the logic that has been set in the solver via Solver::isLogicSet and Solver::getLogic.

Changes

  • SMT-LIB
    • The syntax for 0-ary tuples has been changed for the purposes of disambiguation. The new syntax for 0-ary tuple sort is UnitTuple whose 0-ary constructor is tuple.unit (the previous syntax had overloaded Tuple and tuple, with no arguments).

cvc5 1.0.8

Note: This is a pre-release version for the 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).

cvc5 1.0.7

Changes

  • Various bug fixes

cvc5 1.0.6

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.
    • 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. components.
  • API
    • Simplified the Solver::mkTuple method. The sorts of the elements no longer need to be provided.
    • 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.

cvc5 1.0.5

New Features

  • A new (hand-written) parser is available and enabled by default.
    • Note: the previous 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.

cvc5 1.0.4

New Features

  • Support for the theory of (prime-order) finite fields:
    • Sorts are created with
      • C++: Solver::makeFiniteFieldSort
      • SMT-LIB: (_ FiniteField P) for prime order P
    • Constants are created with
      • C++: Solver::makeFiniteFieldElem
      • SMT-LIB: (as ffN F) for integer N and field sort F
    • The operators are multiplication, addition and negation
      • C++: kinds FF_MUL, FF_ADD, and FF_NEG
      • SMT-LIB: operators ff.mul, ff.add, and ff.neg
    • The only predicate is equality

cvc5 1.0.3

New Features

  • API
    • New API function Solver::getVersion(), returns a string representation of the solver version.
  • Support for bit-vector overflow detection operators:
    • BITVECTOR_UADDO unsigned addition overflow detection
    • BITVECTOR_SADDO signed addition overflow detection
    • BITVECTOR_UMULO unsigned multiplication overflow detection
    • BITVECTOR_SMULO signed multiplication overflow detection
    • BITVECTOR_USUBO unsigned subtraction overflow detection
    • BITVECTOR_SSUBO signed subtraction overflow detection
    • BITVECTOR_SDIVO signed division overflow detection
  • Support for Web Assembly compilation using Emscripten.

Changes

  • The (non-standard) operators BITVECTOR_TO_NAT and INT_TO_BITVECTOR now belong to the UF theory. A logic that includes UF is required to use them.
  • The sort for (non-standard) bit-vector operators BITVECTOR_REDAND and BITVECTOR_REDOR is now (_ BitVec 1) (was Boolean), following the definition of reduction operators in Verilog (their origin).
  • Reenable functionality that allows (get-model) commands after answering unknown when :produce-models is set to true. Note that there is no guarantee that building a model succeeds in this case.

cvc5 1.0.2

Changes

  • API
    • Previously, it was not possible to share Sort, Term, Op, Grammar and datatype objects between Solver instances. This is now allowed for solvers that belong to the same thread.

cvc5 1.0.1

New Features

  • Support for cross-compiling an ARM binary of cvc5 on x86 macOS.
  • Support for declaring oracle functions in the API via the method declareOracleFun. This allows users to declare functions whose semantics are associated with a provided executable implementation.

Changes

  • Removed support for non-standard declare-funs, declare-consts, and declare-sorts commands.
  • The kind for integer constants is now CONST_INTEGER, while real constants continue to have kind CONST_RATIONAL.
  • Type rules for (dis)equality and if-then-else no longer allow mixing integers and reals. Type rules for other operators like APPLY_UF now require their arguments to match the type of the function being applied, and do not assume integer/real subtyping.
  • The API method mkTuple no longer supports casting integers to reals when constructing tuples.

cvc5 1.0

Website

https://cvc5.github.io

Documentation

https://cvc5.github.io/docs

System Description

cvc5: A Versatile and Industrial-Strength SMT Solver.
Barbosa H., Barrett C., Brain M., Kremer G., Lachnitt H., Mann M., Mohamed A., Mohamed M., Niemetz A., Nötzli A., Ozdemir A., Preiner M., Reynolds A., Sheng Y., Tinelli C., and Zohar Y., TACAS 2022. http://dx.doi.org/10.1007/978-3-030-99524-9_24

New Features

Streamlined C++ API

Documentation: https://cvc5.github.io/docs/latest/api/cpp/cpp.html

Two new Python language bindings

New Java language bindings

Documentation: https://cvc5.github.io/docs/latest/api/java/java.html

Theory of Bags (Multisets)

A new theory of bags, which are collections that allow duplicates. It supports basic operators like union disjoint, union max, intersection, difference subtract, difference remove, duplicate removal, and multiplicity of an element in a bag.

Theory of Sequences

  • A new parametric theory of sequences whose syntax is compatible with the syntax for sequences used by Z3.
  • A new array-inspired procedure (option --seq-array).

Arithmetic

Nonlinear real arithmetic is now solved using a new solver based on cylindrical algebraic coverings. Includes full support for non-rational models and a number of options --nl-cov-* for, e.g., different projection operators, Lazard's lifting or variable elimination. The new solver requires the libpoly library, and Lazard's lifting additionally requires CoCoALib.

Arrays

Added support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j.

Bit-vectors

  • New bit-vector solver with CaDiCaL as default SAT back-end.
  • New approach for solving bit-vectors as integers (option --solve-bv-as-int).

Datatypes

Support for generic datatype updaters ((_ update s) t u) which replaces the field specified by selector s of t by the value u.

Integers

  • Support for an integer operator (_ iand n) that returns the bitwise and of two integers, seen as integers modulo n.
  • Support for an integer operator int.pow2, used as (int.pow2 x) which represents 2 to the power of x.

Quantifiers

  • Improved support for enumerative instantiation (option --enum-inst).
  • SyGuS-based quantifier instantiation (option --sygus-inst).

Strings

  • Improved performance using new techniques, including model-based reductions, eager context-dependent simplification, and equality-based conflict finding.
  • Support for str.indexof_re(s, r, n), which returns the index of the first occurrence of a regular expression r in a string s after index n or -1 if r does not match a substring after n.

Proofs

  • Documentation available at: https://cvc5.github.io/docs/latest/proofs/proofs.html
  • When used after an unsatisfiable response to checkSat, getProof returns a representation of the refutation proof for the current set of assertions (get-proof in SMT-LIB).
  • Preliminary support for translations to external proof formats LFSC and Alethe.

Difficulty Estimation

The API method getDifficulty returns a map from asserted formulas to integers which estimates how much that formula contributed to the difficulty of the overall problem (get-difficulty in SMT-LIB).

Learned Literals

The API method getLearnedLiterals gets a list of literals that are entailed by the current set of assertions that were learned during solving (get-learned-literals in SMT-LIB).

Abduction and Interpolation

  • The API method getAbduct can be used to find an abduct for the current set of assertions and provided goal (get-abduct in SMT-LIB). Optionally, a SyGuS grammar can be provided to restrict the shape of possible abducts. If using the text inferace, the grammar may be provided using the same syntax for grammars as in SyGuS IF format.
  • The API method getInterpolant can be used to find an interpolant for the current set of assertions and provided goal (get-interpolant in SMT-LIB). Like abduction, grammars may be provided to restrict the shape of interpolants.

Support for Incremental Synthesis Queries

  • The core SyGuS solver now supports getting multiple solutions for a synthesis conjecture via the API. The method checkSynthNext finds the next SyGuS solution to the current set of SyGuS constraints (check-synth-next in SyGuS IF).
  • getAbductNext finds the next abduct for the current set of assertions and provided goal (get-abduct-next in SMT-LIB).
  • getInterpolantNext finds the next interpolant for the current set of assertions and provided goal (get-interpolant-next in SMT-LIB).

Pool-based Quantifier Instantiation

  • The API method declarePool declares symbol sets of terms called pools (declare-pool in SMT-LIB).
  • Pools can be used in annotations of quantified formulas for fine grained control over quantifier instantiations (:inst-pool, :inst-add-to-pool, :skolem-add-to-pool in SMT-LIB).

Diagnostic Outputs

The option -o TAG can be used to enable a class of useful diagnostic information, such as the state of the input formula before and after pre-preprocessing, quantifier instantiations, literals learned during solving, among others. For SyGuS problems, it can be used to show candidate solutions and grammars that the solver has generated.

Unsat cores

  • Production modes based on the new proof infrastructure (--unsat-cores-mode=sat-proof) and on the solving-under-assumption feature of Minisat (--unsat-cores-mode=assumptions). The mode based on SAT assumptions + preprocessing proofs is the new default.
  • Computing minimal unsat cores (option --minimal-unsat-cores).

Blocking Models

  • The API method blockModels can be used to block the current model using various policies for how to exclude the values of terms (block-model in SMT-LIB).
  • The API method blockModelValues can be used to block the current model for a provided set of terms (block-model-values in SMT-LIB).

Model Cores

  • The API method isModelCoreSymbol can be used to query whether the value for a symbol was critical to whether the model satisfies the current set of assertions.
  • Models can be limited to show only model core symbols (option --model-cores).

Changes

  • CaDiCaL and SymFPU are now required dependencies. CaDiCaL 1.4.1 is now the version used by default.
  • Options have been extensively refactored, please refer to the cvc5 documentation for further information.
  • Removed support for the CVC language.
  • SyGuS: Removed support for SyGuS-IF 1.0.
  • Removed support for the (non-standard) define command.
  • Removed the legacy API along with the Java and Python bindings for it.
  • Interactive shell: the GPL-licensed Readline library has been replaced the BSD-licensed Editline. Compiling with --best now enables Editline, instead of Readline. Without selecting optional GPL components, Editline-enabled cvc5 builds will be BSD licensed.
  • The competition build type includes the dependencies used for SMT-COMP by default. Note that this makes this build type produce GPL-licensed binaries.
  • Bit-vector operator bvxnor was previously mistakenly marked as left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We now restrict bvxnor to only allow two operands in order to avoid confusion about the semantics, since the behavior of n-ary operands to bvxnor is now undefined in SMT-LIB.
  • SMT-LIB output for get-model command now conforms with the standard, and does not begin with the keyword model. The output is the same as before, only with this word removed from the beginning.
  • Building with Python 2 is now deprecated.
  • The SMT-LIB syntax for some extensions has been changed. Notably, set operators are now prefixed by set., and relations by rel.. For example, union is now written set.union.
  • Removed support for redundant logics ALL_SUPPORTED and QF_ALL_SUPPORTED, use ALL and QF_ALL instead.