Merge pull request #6254 from thomasspriggs/tas/smt2_more_logics

Add data structures for setting different smt2 logics in incremental solving

Author: thomasspriggs

src/solvers/smt2_incremental/smt_logics.cpp

@@ -3,7 +3,7 @@
 #include <solvers/smt2_incremental/smt_logics.h>
 
 // Define the irep_idts for logics.
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
 #include <solvers/smt2_incremental/smt_logics.def>
 #undef LOGIC_ID
@@ -21,7 +21,7 @@ bool smt_logict::operator!=(const smt_logict &other) const
 template <typename visitort>
 void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
 {
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   if(id == ID_smt_logic_##the_id)                                              \
     return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
 // The include below is marked as nolint because including the same file
@@ -41,7 +41,10 @@ void smt_logict::accept(smt_logic_const_downcast_visitort &&visitor) const
   ::accept(*this, id(), std::move(visitor));
 }
 
-smt_logic_quantifier_free_bit_vectorst::smt_logic_quantifier_free_bit_vectorst()
-  : smt_logict{ID_smt_logic_quantifier_free_bit_vectors}
-{
-}
+#define LOGIC_ID(the_id, the_name)                                             \
+  smt_logic_##the_id##t::smt_logic_##the_id##t()                               \
+    : smt_logict{ID_smt_logic_##the_id}                                        \
+  {                                                                            \
+  }
+#include "smt_logics.def"
+#undef LOGIC_ID

src/solvers/smt2_incremental/smt_logics.def

@@ -6,4 +6,9 @@
 ///  * The constant `irep_idt`s used to identify each of the logic classes.
 ///  * The member functions of the `smt_logic_const_downcast_visitort` class.
 ///  * The type of option checks required to implement `smt_logict::accept`.
-LOGIC_ID(quantifier_free_bit_vectors)
+LOGIC_ID(quantifier_free_uninterpreted_functions, QF_UF)
+LOGIC_ID(quantifier_free_bit_vectors, QF_BV)
+LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors, QF_UFBV)
+LOGIC_ID(quantifier_free_bit_vectors_arrays, QF_ABV)
+LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors_arrays, QF_AUFBV)
+LOGIC_ID(all, ALL)

src/solvers/smt2_incremental/smt_logics.h

@@ -61,16 +61,21 @@ const smt_logict &smt_logict::storert<derivedt>::downcast(const irept &irep)
   return static_cast<const smt_logict &>(irep);
 }
 
-class smt_logic_quantifier_free_bit_vectorst : public smt_logict
-{
-public:
-  smt_logic_quantifier_free_bit_vectorst();
-};
+#define LOGIC_ID(the_id, the_name)                                             \
+  /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */  \
+  class smt_logic_##the_id##t : public smt_logict                              \
+  {                                                                            \
+  public:                                                                      \
+    smt_logic_##the_id##t();                                                   \
+  };
+#include "smt_logics.def"
+#undef LOGIC_ID
 
 class smt_logic_const_downcast_visitort
 {
 public:
-#define LOGIC_ID(the_id) virtual void visit(const smt_logic_##the_id##t &) = 0;
+#define LOGIC_ID(the_id, the_name)                                             \
+  virtual void visit(const smt_logic_##the_id##t &) = 0;
 #include "smt_logics.def"
 #undef LOGIC_ID
 };

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -265,10 +265,13 @@ class smt_logic_to_string_convertert : public smt_logic_const_downcast_visitort
   {
   }
 
-  void visit(const smt_logic_quantifier_free_bit_vectorst &) override
-  {
-    os << "QF_BV";
+#define LOGIC_ID(the_id, the_name)                                             \
+  void visit(const smt_logic_##the_id##t &) override                           \
+  {                                                                            \
+    os << #the_name;                                                           \
   }
+#include "smt_logics.def"
+#undef LOGIC_ID
 };
 
 std::ostream &operator<<(std::ostream &os, const smt_logict &logic)

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -137,8 +137,19 @@ TEST_CASE(
   "Test smt_set_logic_commandt to string conversion",
   "[core][smt2_incremental]")
 {
-  const smt_logic_quantifier_free_bit_vectorst qf_bv;
+  const auto qf_uf = smt_logic_quantifier_free_uninterpreted_functionst{};
+  CHECK(smt_to_smt2_string(qf_uf) == "QF_UF");
+  const auto qf_bv = smt_logic_quantifier_free_bit_vectorst{};
   CHECK(smt_to_smt2_string(qf_bv) == "QF_BV");
+  const auto qf_ufbv =
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{};
+  CHECK(smt_to_smt2_string(qf_ufbv) == "QF_UFBV");
+  const auto qf_abv = smt_logic_quantifier_free_bit_vectors_arrayst{};
+  CHECK(smt_to_smt2_string(qf_abv) == "QF_ABV");
+  const auto qf_aufbv =
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectors_arrayst{};
+  CHECK(smt_to_smt2_string(qf_aufbv) == "QF_AUFBV");
+  CHECK(smt_to_smt2_string(smt_logic_allt{}) == "ALL");
   CHECK(
     smt_to_smt2_string(smt_set_logic_commandt{qf_bv}) == "(set-logic QF_BV)");
 }