Add larger selection of SMT logics

We almost certainly don't need all of these in the near future, but
having the data structures for them available will make it straight
forward to experiment with different options.

Author: thomasspriggs

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_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)

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)");
 }