Latest builds

• Fixed issue with model values in MBQI solver (#185).

• Configuring a terminator when a SAT solver that does not have terminator
  support (CryptoMiniSat, Kissat) is configured will now raise an exception
  in Bitwuzla::configure_terminator() rather than at Bitwuzla::check_sat().
  This is also handled correspondingly in the C and Python bindings.

• Fixed handling of non-distinct variable bindings in SMT2 parser.

• Various fixes.

• Abstraction module (option --abstraction) for abstracting bit-vector
  arithmetic operators, is now enabled by default. Default minimum bit-vector
  size for abstraction (option --abstraction-bv-size) is now 33.
• Refactored and improved arithmetic normalization , fixed issue related to
  arithmetic normalization (issue #168).
• Fixed shadow handling of let bindings (issue #169).
• Bumped CaDiCaL to version 2.1.2.
• Added API support for converting a floating-point value to a Real string.
  • C++ API: Term::fp_value_to_real_str()
  • C API: bitwuzla_term_fp_value_to_real_string(Bitwuzla*, BitwuzlaTerm)
  • Python API: Term.fp_value_to_real_str()
• Fixed printing of fp.to_ubv and fp.to_sbv terms (#149) and quoted symbols (#151).
• Fixed error handling when parsing parameters of define-fun.
• New options to print AIG and CNF of current bit-vector abstraction.
  • --write-aiger=<name>.[aig|aag]: writes binary or ASCII AIGER to specified
    filename, format chosen based on suffix ( aig : binary, aag : ascii).
  • --write-cnf=<name>: writes CNF in DIMACS format to specified filename.

• Support for experimental floating-point formats is now disabled by
  default, due to known issues with experimental formats in SymFPU.
  Floating-point formats Float16, Float32, Float64 and Float128
  are considered non-experimental, every other format is considered
  experimental. Support for experimental formats can be enabled via build
  configuration option --fpexp. Use at your own risk.

• Added option -j/--nthreads for configuring multi-threading. Currently,
  multi-threading is only supported on the SAT solver level, and only when
  CryptoMiniSat is configured as the back end SAT solver. Else, configuring
  this option it is a noop.

• Added support for CryptoMiniSat as back end SAT solver.

• Add API support for simplifying terms.

  • C++ API: Bitwuzla::simplify(const Term&)
  • C API: bitwuzla_simplify_term(Bitwuzla*, BitwuzlaTerm)
  • Python API: Bitwuzla.simplify_term(Term)

• Fixed issue with model construction for arrays (issue #145).

• SMT2 parser now supports non-indexed rotate operators. These operators are
  binary, with the second argument representing the number of bits to rotate by:

  • (bvror <term> <term>)
  • (bvrol <term> <term>)

• Added new CLI option --pp-only (preprocess only).

• C++ API: Output streams can now be configured to disable letification of
  terms when printing (letification is enabled by default).
  To disable, for std::ostream os , use os << set_letify(false); .

• Fixed BV_AND_CONCAT rewrite (issues #131 and #134).

• Fixed a GMP memory leak in the BitVector move constructor.

• Fixed errors detected with UBSan.

• Added new abstraction module for abstracting bit-vector arithmetic
  operators, see Aina Niemetz, Mathias Preiner and Yoni Zohar. Scalable
  Bit-Blasting with Abstractions. CAV 2024, Springer, 2024..
  Enable with option --abstraction, the minimum bit-width of relevant terms
  to abstract can be configured via option --abstraction-bv-size.

• Quantification over array variables now supported.

• Improved arithmetic normalization.

• Added new command-line option --print-model. This enables auto-printing
  of models after a satisfiable query. Must be enabled to print models for
  BTOR2 input (automatically enables -m). Command line option -m,
  --produce-models alone now does not print models for BTOR2 input anymore.

• Parser now allows to configure auto-printing of models (corresponding to
  command-line option --print-model above) via:

  • C++ API: Parser::configure_auto_print_model(bool)
  • C API: bitwuzla_parser_configure_auto_print_model(BitwuzlaParser*,bool)
  • Python API: Parser.configure_auto_print_model(bool)

• Bumped Kissat to version 4.0.1.

• Fixed version string generation for dev versions. Previously, git information
  that is included in the version string was not regenerated at compile time,
  only at configure time.

• Fixed incorrect result with rewrite level 0 (issue #110) (missing guard,
  normalization preprocessing pass expects terms to be fully rewritten).

• Refactored node data storage and unique table handling, improves
  performance and memory footprint.

• Added support for BTOR2 model printing.

• Added support for querying the parser for declared sorts and terms.

  • C++ API:
    • New Function Parser::get_declared_sorts() to retrieve user-declared
      sorts (SMT-LIB: declared via declare-sort, BTOR2: always empty).
    • New Function Parser::get_declared_funs() to retrieve user-declared
      function symbols (SMT-LIB: declared via declare-const and declare-fun,
      BTOR2: inputs with a symbol).
  • C API:
    • New Function bitwuzla_parser_get_declared_sorts(BitwuzlaParser*, size_t*).
    • New Function bitwuzla_parser_get_declared_funs(BitwuzlaParser*, size_t*).
  • Python API:
    • New Function Parser.get_declared_sorts().
    • New Function Parser.get_declared_funs().

• Refactored statistics printing to not print NaN values.

• Improved logging and statistics for local search engine.

• Several improvements to build system configuration.

• Several fixes for Windows cross compilation.

• Added Linux aarch64 cross-compilation support (configure flag: --arm64).

• Introduce TermManager interface for creating Term and Sort
  (major API change).

  • Solver and parser instances now require a term manager for initialization.
    Terms and sorts can be shared across solver/parser instances if they were
    initialized with the same term manager. The term manager is responsible for
    managing Term and Sort objects.
  • C++ API:
    • New class TermManager for creating Term and Sort objects.
    • Term and Sort creation function mk_* moved to TermManager class.
    • Substitution functions substitute_term and substitute_terms moved
      to TermManager.
    • Constructor Bitwuzla(const Options &options) changed to
      Bitwuzla(TermManager&, const Options &options).
    • New function Bitwuzla::term_mgr() to retrieve configured term manager
      instance.
  • C API:
    • New functions bitwuzla_term_manager_new(),
      bitwuzla_term_manager_delete for creating and deleting term manager
      instances.
    • Function bitwuzla_new(const BitwuzlaOptions*) changed to
      bitwuzla_new(BitwuzlaTermManager*, const BitwuzlaOptions*).
    • New function bitwuzla_get_term_mgr(Bitwuzla*) to retrieve configured term
      manager instance from Bitwuzla instance.
    • New reference counting interface for fine-grained resource management:
      • New function bitwuzla_term_manager_release(BitwuzlaTermManager*) to release all created
        terms and sorts of a term manager instance.
      • New functions bitwuzla_term_copy(BitwuzlaTerm) and
        bitwuzla_term_release(BitwuzlaTerm) for
        incrementing/decrementing BitwuzlaTerm reference counts.
      • New functions bitwuzla_sort_copy(BitwuzlaSort) and
        bitwuzla_sort_release(BitwuzlaSort) for
        incrementing/decrementing BitwuzlaSort reference counts.
  • Python API:
    • New class TermManager for creating Term and Sort objects.
    • Term and Sort creation function mk_* moved to TermManager class.
    • Substitution functions substitute_term and substitute_terms moved
      to TermManager.
    • Constructor Bitwuzla(Options) changed to
      Bitwuzla(TermManager, Options).
    • New function Bitwuzla::term_mgr() to retrieve configured term manager
      instance.

• Refactor parser interface to allow parsing from string inputs.

  • A parser instance is not tied to an input file anymore.
  • Added support for parsing from string inputs.
  • Added support for parsing terms and sorts from string inputs.
  • Interface for parsing functions now returns bool instead of string.
  • C++ API:
    • Constructor Parser(Options&, const std::string&, const std::string&, std::ostream*)
      changed to Parser(TermManager&, Options&, const std::string&, std::ostream*)
    • Function std::string Parser::parse(bool) changed to
      void Parser::parse(const std::string, bool, bool)
      and now throws an exception on error. It now also supports parsing from
      string input.
    • New Function void Parser::parse(const std::string&, std::istream&, bool)
      allows parsing from an already open input stream and now throws an
      exception on error. This function is not limited to input files but also
      supports parsing from std::cin and strings.
    • New function bitwuzla::Term parse_term(const std::string&) to
      parse a term from string.
    • New function bitwuzla::Sort parse_sort(const std::string&) to
      parse a sort from string.
    • New bitwuzla::parser::Exception (derived from bitwuzla::Exception)
      which is thrown on parse error.
  • C API:
    • Function BitwulzaParser* bitwuzla_parser_new(BitwuzlaOptions*, const char*, FILE*, const char*, uint8_t, const char*)
      changed to BitwulzaParser* bitwuzla_parser_new(BitwuzlaTermManager*, BitwuzlaOptions*, const char*, uint8_t, const char*).
    • Function const char* bitwuzla_parser_parse(BitwulzaParser*, bool)
      changed to void bitwuzla_parser_parse(BitwulzaParser*, const char*, bool, bool, const char*).
    • New function const char* bitwuzla_parser_get_error_msg(BitwuzlaParser*)
      to query error message.
    • New function BitwuzlaTerm bitwuzla_parser_parse_term(BitwuzlaParser*, const char*, const char*)
      to parse a term from string.
    • New function BitwuzlaSort bitwuzla_parser_parse_sort(BitwuzlaParser*, const char*, const char*)
      to parse a sort from string.
  • Python API:
    • Class Parser is now constructed from options, a language and a base
      for the string representation of bit-vector values (does not require
      an input file name anymore).
    • Function Parser.parse(self, parse_only: bool) -> str changed to
      Parser.parse(self, infile_name, parse_only: bool, parse_file: bool) -> bool.
    • New function parse_term(self, iinput) -> Term to parse term from string.
    • New function parse_sort(self, iinput) -> Sort to parse sort form string.

• Fix special case handling for equality over constant arrays.