fetch 'bitwuzla' from 'b772cd25'

api/dune

@@ -17,6 +17,7 @@
  (foreign_archives
   ../vendor/bitwuzla/src/api/cpp/bitwuzla-api
   ../vendor/bitwuzla/bitwuzla-cxx
+  ../vendor/bitwuzla/src/parser/smt2/bitwuzla-smt2
   ../vendor/bitwuzla/src/lib/bitwuzla-libs
   ../vendor/cadical/cadical)
  (library_flags -linkall)
@@ -37,6 +38,7 @@
  (foreign_archives
   ../vendor/bitwuzla/src/api/cpp/bitwuzla-api
   ../vendor/bitwuzla/bitwuzla-cxx
+  ../vendor/bitwuzla/src/parser/smt2/bitwuzla-smt2
   ../vendor/bitwuzla/src/lib/bitwuzla-libs
   ../vendor/cadical/cadical)
  (library_flags -linkall)
@@ -57,6 +59,7 @@
  (foreign_archives
   ../vendor/bitwuzla/src/api/cpp/bitwuzla-api
   ../vendor/bitwuzla/bitwuzla-cxx
+  ../vendor/bitwuzla/src/parser/smt2/bitwuzla-smt2
   ../vendor/bitwuzla/src/lib/bitwuzla-libs
   ../vendor/cadical/cadical)
  (library_flags -linkall)
@@ -77,6 +80,7 @@
  (foreign_archives
   ../vendor/bitwuzla/src/api/cpp/bitwuzla-api
   ../vendor/bitwuzla/bitwuzla-cxx
+  ../vendor/bitwuzla/src/parser/smt2/bitwuzla-smt2
   ../vendor/bitwuzla/src/lib/bitwuzla-libs
   ../vendor/cadical/cadical)
  (library_flags -linkall)

bitwuzla_cxx.ml

@@ -559,6 +559,12 @@ module type S = sig
           (** Bit-vector negation (two's complement).
 
         SMT-LIB: [bvneg] *)
+      | Bv_nego
+          (** Bit-vector negation overflow test.
+
+            Predicate indicating if bit-vector negation produces an overflow.
+
+            SMT-LIB: [bvnego] *)
       | Bv_nor  (** Bit-vector nor.
 
                   SMT-LIB: [bvnor] *)

bitwuzla_cxx.mli

@@ -72,12 +72,19 @@ module Options : sig
             - An unsigned integer value <= 4 \[{b default}: [0]\].
         *)
     | Time_limit_per : int key
-        (** Time limit in milliseconds per satisfiability check.**
+        (** Time limit in milliseconds per satisfiability check.
 
             Values:
             - An unsigned integer for the time limit in milliseconds.
             \[{b default}: [0]\].
         *)
+    | Memory_limit : int key
+        (** Memory limit in MB.
+
+              Values:
+              - An unsigned integer for the memory limit in MB.
+              \[{b default}: [0]\].
+          *)
     | Bv_solver : bv_solver key
     | Rewrite_level : int key
         (** Rewrite level.
@@ -791,6 +798,12 @@ module type S = sig
           (** Bit-vector negation (two's complement).
 
         SMT-LIB: [bvneg] *)
+      | Bv_nego
+          (** Bit-vector negation overflow test.
+
+            Predicate indicating if bit-vector negation produces an overflow.
+
+            SMT-LIB: [bvnego] *)
       | Bv_nor  (** Bit-vector nor.
 
                   SMT-LIB: [bvnor] *)

dune

@@ -24,6 +24,7 @@
  (foreign_archives
   vendor/bitwuzla/src/api/cpp/bitwuzla-api
   vendor/bitwuzla/bitwuzla-cxx
+  vendor/bitwuzla/src/parser/smt2/bitwuzla-smt2
   vendor/bitwuzla/src/lib/bitwuzla-libs
   vendor/cadical/cadical)
  (c_library_flags :standard -L/opt/homebrew/lib -lgmp)

vendor/dune

@@ -16,10 +16,10 @@
    (language cxx)
    (names
     bitvector
-    aig_manager
     aig_cnf
+    aig_manager
+    aig_node
     aig_printer
-    aig_bitblaster
     ls
     ls_bv
     bitvector_domain
@@ -50,7 +50,21 @@
     (extra_deps ../../config.h ../../../../.bitwuzla_tree))))
  (subdir
   src
-  (dirs :standard \ parser)
+  (subdir
+   parser
+   (include_subdirs no)
+   (subdir
+    smt2
+    (foreign_library
+     (archive_name bitwuzla-smt2)
+     (language cxx)
+     (names lexer)
+     (flags
+      :standard
+      -std=c++17
+      -I../..
+      -DNDEBUG)
+     (extra_deps ../../../../.bitwuzla_tree))))
   (rule
    (deps ../COPYING)
    (target config.h)
@@ -126,6 +140,7 @@
    rewrites_bv_norm
    rewrites_core
    rewrites_fp
+   resource_terminator
    cadical
    cryptominisat
    kissat
@@ -148,7 +163,6 @@
    solver_engine
    solver_state
    solving_context
-   timeout_terminator
    type
    type_data
    type_manager