Merge pull request #6240 from thomasspriggs/tas/smt2_data_structures_to_string

Add conversion of incremental smt2 data structures to string

Author: thomasspriggs

src/solvers/Makefile

@@ -197,6 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
+      smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 

src/solvers/smt2_incremental/smt_commands.cpp

@@ -83,7 +83,9 @@ smt_define_function_commandt::smt_define_function_commandt(
   smt_termt definition)
   : smt_commandt{ID_smt_define_function_command}
 {
-  set(ID_identifier, identifier);
+  set(
+    ID_identifier,
+    upcast(smt_identifier_termt{std::move(identifier), definition.get_sort()}));
   std::transform(
     std::make_move_iterator(parameters.begin()),
     std::make_move_iterator(parameters.end()),
@@ -94,9 +96,10 @@ smt_define_function_commandt::smt_define_function_commandt(
   set(ID_code, upcast(std::move(definition)));
 }
 
-const irep_idt &smt_define_function_commandt::identifier() const
+const smt_identifier_termt &smt_define_function_commandt::identifier() const
 {
-  return get(ID_identifier);
+  return static_cast<const smt_identifier_termt &>(
+    downcast(find(ID_identifier)));
 }
 
 std::vector<std::reference_wrapper<const smt_identifier_termt>>

src/solvers/smt2_incremental/smt_commands.h

@@ -70,7 +70,7 @@ class smt_define_function_commandt
     irep_idt identifier,
     std::vector<smt_identifier_termt> parameters,
     smt_termt definition);
-  const irep_idt &identifier() const;
+  const smt_identifier_termt &identifier() const;
   std::vector<std::reference_wrapper<const smt_identifier_termt>>
   parameters() const;
   const smt_sortt &return_sort() const;

src/solvers/smt2_incremental/smt_sorts.cpp

@@ -27,6 +27,10 @@ smt_bool_sortt::smt_bool_sortt() : smt_sortt{ID_smt_bool_sort}
 smt_bit_vector_sortt::smt_bit_vector_sortt(const std::size_t bit_width)
   : smt_sortt{ID_smt_bit_vector_sort}
 {
+  INVARIANT(
+    bit_width > 0,
+    "The definition of SMT2 bit vector theory requires the number of "
+    "bits to be greater than 0.");
   set_size_t(ID_width, bit_width);
 }