From 149934a0ce628571329a48e1c7fc0dbc4995905d Mon Sep 17 00:00:00 2001
From: Christoph Kirsch <ckirsch@gmail.com>
Date: Tue, 31 Dec 2024 17:11:47 +0100
Subject: [PATCH] Replacing boolector with bitwuzla, introducing explicit Bool
 type in monster

---
 Makefile        | 14 +++++++-------
 tools/monster.c |  9 ++++++---
 2 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index eec975bd..eb4590cd 100644
--- a/Makefile
+++ b/Makefile
@@ -344,10 +344,10 @@ rotor-btor2: $(rotors) selfie-rotorized.btor2 synthesize
 btor2: beator-btor2 rotor-btor2
 
 # Consider these targets as targets, not files
-.PHONY: spike qemu assemble beator-32 rotor-32 32-bit boolector beator-btormc rotor-btormc btormc extras
+.PHONY: spike qemu assemble beator-32 rotor-32 32-bit bitwuzla beator-btormc rotor-btormc btormc extras
 
 # Run everything that requires non-standard tools
-extras: spike qemu assemble beator-32 rotor-32 32-bit
+extras: spike qemu assemble beator-32 rotor-32 32-bit bitwuzla
 
 # Run selfie on spike
 spike: selfie.m selfie.s
@@ -391,11 +391,11 @@ rotor-32: tools/rotor.c selfie.h
 	./beator-32 -c selfie.h tools/beator.c - 0 --check-block-access
 	./rotor-32 -c selfie.h tools/rotor.c - $(rotor)
 
-# Run boolector SMT solver on SMT-LIB files generated by monster
-boolector: smt
-	$(foreach file, $(smts-1), [ $$(boolector $(file) -e 0 | grep -c ^sat$$) -eq 1 ] &&) true
-	$(foreach file, $(smts-2), [ $$(boolector $(file) -e 0 | grep -c ^sat$$) -eq 2 ] &&) true
-	$(foreach file, $(smts-3), [ $$(boolector $(file) -e 0 | grep -c ^sat$$) -eq 3 ] &&) true
+# Run bitwuzla SMT solver on SMT-LIB files generated by monster
+bitwuzla: smt
+	$(foreach file, $(smts-1), [ $$(bitwuzla $(file) | grep -c ^sat$$) -eq 1 ] &&) true
+	$(foreach file, $(smts-2), [ $$(bitwuzla $(file) | grep -c ^sat$$) -eq 2 ] &&) true
+	$(foreach file, $(smts-3), [ $$(bitwuzla $(file) | grep -c ^sat$$) -eq 3 ] &&) true
 
 # Run btormc bounded model checker on BTOR2 files generated by beator
 beator-btormc: beator-btor2
diff --git a/tools/monster.c b/tools/monster.c
index f2b9d93c..b50911db 100644
--- a/tools/monster.c
+++ b/tools/monster.c
@@ -738,7 +738,7 @@ void constrain_add_sub_mul_divu_remu_sltu(char* operator) {
 void zero_extend_sltu() {
   if (rd != REG_ZR)
     if (*(reg_sym + rd))
-      *(reg_sym + rd) = (uint64_t) smt_unary(bv_zero_extension(1), (char*) *(reg_sym + rd));
+      *(reg_sym + rd) = (uint64_t) smt_ternary("ite", (char*) *(reg_sym + rd), bv_constant(1), bv_constant(0));
 }
 
 void constrain_load() {
@@ -876,7 +876,7 @@ void constrain_beq() {
   bvar = smt_variable("b", 1);
 
   w = w
-    + dprintf(output_fd, "(assert (= %s %s)); beq in ", bvar, smt_binary("bvcomp", op1, op2))
+    + dprintf(output_fd, "(assert (= %s %s)); beq in ", bvar, smt_binary("=", op1, op2))
     + print_code_context_for_instruction(pc)
     + dprintf(output_fd, "\n");
 
@@ -1284,6 +1284,9 @@ char* bv_constant(uint64_t value) {
 char* bv_variable(uint64_t bits) {
   char* string;
 
+  if (bits == 1)
+    return "Bool";
+
   string = string_alloc(10 + 2); // up to 64-bit variables require up to 2 decimal digits
 
   sprintf(string, "(_ BitVec %lu)", bits);
@@ -1316,7 +1319,7 @@ char* smt_variable(char* prefix, uint64_t bits) {
   sprintf(svar, "%s%lu", prefix, variable_version);
 
   w = w
-    + dprintf(output_fd, "(declare-fun %s () (_ BitVec %lu)); variable for ", svar, bits)
+    + dprintf(output_fd, "(declare-fun %s () %s); variable for ", svar, bv_variable(bits))
     + print_code_context_for_instruction(pc)
     + dprintf(output_fd, "\n");