Upgrade bitwuzla '0.3.0'

CHANGES.md

@@ -1,3 +1,12 @@
+## 0.3.0 (2023-12-12)
+
+Update [Bitwuzla](https://github.com/bitwuzla/bitwuzla/releases/tag/0.3.0) sources.
+
+`Bitwuzla_cxx` can now be installed alongside `Bitwuzla_c`.
+
+Vendor submodules:
+- [Bitwuzla](https://github.com/bitwuzla/bitwuzla) tag:0.3.0
+
 ## 0.2.0 (2023-09-01)
 
 Initial release.

bitwuzla-cxx.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.2.0"
+version: "0.3.0"
 synopsis: "SMT solver for AUFBVFP (C++ API)"
 description: """
 

bitwuzla_cxx.mli

@@ -149,6 +149,20 @@ module Options : sig
 
             This is an expert option to configure the prop solver engine.
         *)
+    | Prop_opt_lt_concat_sext : bool key
+        (** Propagation-based local search solver engine:
+          Optimization for inverse value computation of inequalities over
+          concat and sign extension operands.
+
+          When enabled, use optimized inverse value value computation for
+          inequalities over concats.
+
+          Values:
+          - [true]: enable
+          - [false]: disable \[{b default}\]
+
+          This is an expert option to configure the prop solver engine.
+      *)
     | Prop_path_sel : prop_path_sel key
         (** Propagation-based local search solver engine:
             Path selection.
@@ -765,7 +779,11 @@ module Kind : sig
     | Bv_neg
         (** Bit-vector negation (two's complement).
 
-        SMT-LIB: [bvneg] *)
+            SMT-LIB: [bvneg] *)
+    | Bv_nego
+        (** Bit-vector negation overflow test.
+
+            SMT-LIB: [bvnego] *)
     | Bv_nor  (** Bit-vector nor.
 
                   SMT-LIB: [bvnor] *)

dune-project

@@ -2,7 +2,7 @@
 (generate_opam_files true)
 
 (name bitwuzla-cxx)
-(version 0.2.0)
+(version 0.3.0)
 (maintainers "Frédéric Recoules <[email protected]>")
 (authors "Frédéric Recoules")
 (source (github  bitwuzla/ocaml-bitwuzla))

vendor/dune

@@ -49,8 +49,10 @@
      -DNDEBUG)
     (extra_deps ../../config.h ../../../../.bitwuzla_tree))))
  (subdir
-  src
-  (dirs :standard \ parser)
+   src
+  (subdir
+    parser
+    (dirs :standard \ btor2))
   (rule
    (deps ../COPYING)
    (target config.h)
@@ -102,6 +104,7 @@
    node_manager
    node_utils
    option
+   lexer
    assertion_tracker
    assertion_vector
    contradicting_ands
@@ -151,7 +154,9 @@
    type
    type_data
    type_manager
+   hash_pair
    logger
+   resources
    statistics)
   (include_dirs include src src/lib ../symfpu ../cadical)
   (flags
@@ -180,9 +185,7 @@
   (:p0001
    (file patch/0001-api-Add-hook-for-ocaml-z-value.patch))
   (:p0002
-   (file patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch))
-  (:p0003
-   (file patch/0003-Fix-compilation-with-older-GCC-version.patch)))
+   (file patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch)))
  (target .bitwuzla_tree)
  (action
   (no-infer
@@ -193,7 +196,4 @@
     (with-stdin-from
      %{p0002}
      (run patch -p1 --directory bitwuzla))
-    (with-stdin-from
-     %{p0003}
-     (run patch -p1 --directory bitwuzla))
     (write-file %{target} "")))))