From 4b9a5c503d1039821745f3304c961682d7ec8eb2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 6 Aug 2025 17:33:53 -0700
Subject: [PATCH] Hanoi Omega-Automata INT is 32 bits

The Hanoi Omega-Automata specification requires that numbers of type INT are
nonnegative and less than 2^31.  Hence, uint32_t suffices, mp_integer is not
necessary.
---
 src/temporal-logic/hoa.cpp           | 22 ++++++++++++++++------
 src/temporal-logic/hoa.h             | 13 ++++++++-----
 src/temporal-logic/ltl_to_buechi.cpp |  2 +-
 3 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp
index 3d432aa3f..e7bcd43c7 100644
--- a/src/temporal-logic/hoa.cpp
+++ b/src/temporal-logic/hoa.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "hoa.h"
 
 #include <util/arith_tools.h>
+#include <util/string2int.h>
 
 #include <ebmc/ebmc_error.h>
 
@@ -167,9 +168,9 @@ hoa_tokenizert::tokent hoa_tokenizert::get_token(std::istream &in)
   }
 }
 
-mp_integer hoat::max_state_number() const
+hoat::intt hoat::max_state_number() const
 {
-  mp_integer max = 0;
+  intt max = 0;
 
   for(auto &state : body)
     max = std::max(max, state.first.number);
@@ -208,6 +209,7 @@ class hoa_parsert
   labelt parse_label_expr_and();
   labelt parse_label_expr_primary();
   acc_sigt parse_acc_sig();
+  hoat::intt parse_int();
 };
 
 hoat hoat::from_string(const std::string &src)
@@ -222,6 +224,15 @@ hoat hoat::from_string(const std::string &src)
   return hoat{header, body};
 }
 
+hoat::intt hoa_parsert::parse_int()
+{
+  auto text = tokenizer.consume().text;
+  auto int_opt = string2optional<hoat::intt>(text);
+  if(!int_opt.has_value())
+    throw ebmc_errort() << "HOA-parser failed to parse INT";
+  return int_opt.value();
+}
+
 hoat::headert hoa_parsert::parse_header()
 {
   std::string headername;
@@ -284,8 +295,7 @@ hoat::state_namet hoa_parsert::parse_state_name()
     state_name.label = parse_label();
 
   // INT
-  auto number = tokenizer.consume().text;
-  state_name.number = string2integer(number);
+  state_name.number = parse_int();
 
   // STRING?
   if(tokenizer.peek().is_string())
@@ -324,11 +334,11 @@ hoat::edget hoa_parsert::parse_edge()
     edge.label = parse_label();
 
   // state-conj: INT | state-conj "&" INT
-  edge.dest_states.push_back(string2integer(tokenizer.consume().text));
+  edge.dest_states.push_back(parse_int());
   while(tokenizer.peek().text == "&")
   {
     tokenizer.consume();
-    edge.dest_states.push_back(string2integer(tokenizer.consume().text));
+    edge.dest_states.push_back(parse_int());
   }
 
   // acc-sig?
diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h
index 394699544..2bf2fc9e7 100644
--- a/src/temporal-logic/hoa.h
+++ b/src/temporal-logic/hoa.h
@@ -10,8 +10,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #define CPROVER_TEMPORAL_LOGIC_HOA_H
 
 #include <util/irep.h>
-#include <util/mp_arith.h>
 
+#include <cstdint>
 #include <list>
 #include <map>
 #include <string>
@@ -24,12 +24,15 @@ class hoat
   using headert = std::list<std::pair<std::string, std::list<std::string>>>;
   headert header;
 
+  // A HOA INT is non-negative and less than 2^31
+  using intt = uint32_t;
+
   // body
   using labelt = irept;
   using acc_sigt = std::vector<std::string>;
   struct state_namet
   {
-    mp_integer number;
+    intt number;
     labelt label; // in-state condition
     acc_sigt acc_sig;
     bool is_accepting() const
@@ -40,7 +43,7 @@ class hoat
   struct edget
   {
     labelt label; // transition condition
-    std::vector<mp_integer> dest_states;
+    std::vector<intt> dest_states;
     acc_sigt acc_sig; // acceptance sets
   };
   using edgest = std::list<edget>;
@@ -61,10 +64,10 @@ class hoat
     return out;
   }
 
-  mp_integer max_state_number() const;
+  intt max_state_number() const;
 
   // atomic propositions
-  std::map<mp_integer, std::string> ap_map;
+  std::map<intt, std::string> ap_map;
 };
 
 #endif // CPROVER_TEMPORAL_LOGIC_HOA_H
diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp
index a87114419..1ec7a3458 100644
--- a/src/temporal-logic/ltl_to_buechi.cpp
+++ b/src/temporal-logic/ltl_to_buechi.cpp
@@ -178,7 +178,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
     // is nonaccepting with an unconditional self-loop.
     std::vector<exprt> error_disjuncts;
 
-    std::map<mp_integer, std::pair<hoat::state_namet, hoat::edgest>> state_map;
+    std::map<hoat::intt, std::pair<hoat::state_namet, hoat::edgest>> state_map;
     for(auto &state : hoa.body)
       state_map[state.first.number] = state;