latest

Latest builds

cvc5-1.1.2

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.

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

cvc5-1.0.9

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.

cvc5-1.0.8

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

cvc5-1.0.7

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

cvc5-1.0.5

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.

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.