Add smt_set_option_commandt

Author: thomasspriggs

src/solvers/Makefile

@@ -193,6 +193,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
       smt2_incremental/smt_commands.cpp \
+      smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt_to_string.cpp \

src/solvers/smt2_incremental/smt_commands.cpp

@@ -144,6 +144,17 @@ size_t smt_pop_commandt::levels() const
   return get_size_t(ID_value);
 }
 
+smt_set_option_commandt::smt_set_option_commandt(smt_optiont option)
+  : smt_commandt(ID_smt_set_option_command)
+{
+  set(ID_value, upcast(std::move(option)));
+}
+
+const smt_optiont &smt_set_option_commandt::option() const
+{
+  return downcast(find(ID_value));
+}
+
 template <typename visitort>
 void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
 {

src/solvers/smt2_incremental/smt_commands.h

@@ -4,6 +4,7 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
 
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/smt_options.h>
 #include <util/irep.h>
 
 class smt_command_const_downcast_visitort;
@@ -103,9 +104,13 @@ class smt_set_logic_commandt : public smt_commandt
 public:
 };
 
-class smt_set_option_commandt : public smt_commandt
+class smt_set_option_commandt :
+  public smt_commandt,
+  private smt_optiont::storert<smt_set_option_commandt>
 {
 public:
+  explicit smt_set_option_commandt(smt_optiont option);
+  const smt_optiont &option() const;
 };
 
 class smt_command_const_downcast_visitort

src/solvers/smt2_incremental/smt_options.cpp

@@ -0,0 +1,55 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_options.h>
+
+// Define the irep_idts for options.
+#define OPTION_ID(the_id)                                                        \
+  const irep_idt ID_smt_option_##the_id{"smt_option_" #the_id};
+#include <solvers/smt2_incremental/smt_options.def>
+#undef OPTION_ID
+
+smt_optiont::smt_optiont(const irep_idt id) : irept(id)
+{
+}
+
+bool smt_optiont::operator==(const smt_optiont &other) const {
+  return irept::operator==(other);
+}
+
+bool smt_optiont::operator!=(const smt_optiont &other) const {
+  return !(*this == other);
+}
+
+smt_option_produce_modelst::smt_option_produce_modelst(bool setting)
+  : smt_optiont{ID_smt_option_produce_models}
+{
+  set(ID_value, setting);
+}
+
+bool smt_option_produce_modelst::setting() const
+{
+  return get_bool(ID_value);
+}
+
+template <typename visitort>
+void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
+{
+#define OPTION_ID(the_id)                                                      \
+  if(id == ID_smt_option_##the_id)                                             \
+    return visitor.visit(static_cast<const smt_option_##the_id##t &>(option));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_options.def> // NOLINT(build/include)
+#undef OPTION_ID
+  UNREACHABLE;
+}
+
+void smt_optiont::accept(smt_option_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_optiont::accept(smt_option_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}

src/solvers/smt2_incremental/smt_options.def

@@ -0,0 +1,9 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of options which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the option classes.
+///  * The member functions of the `smt_option_const_downcast_visitort` class.
+///  * The type of option checks required to implement `smt_optiont::accept`.
+OPTION_ID(produce_models)

src/solvers/smt2_incremental/smt_options.h

@@ -0,0 +1,79 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
+
+#include <util/irep.h>
+
+class smt_option_const_downcast_visitort;
+
+class smt_optiont : protected irept
+{
+public:
+  // smt_optiont does not support the notion of an empty / null state. Use
+  // optionalt<smt_optiont> instead if an empty option is required.
+  smt_optiont() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_optiont &) const;
+  bool operator!=(const smt_optiont &) const;
+
+  void accept(smt_option_const_downcast_visitort &) const;
+  void accept(smt_option_const_downcast_visitort &&) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_optiont to and
+  ///   from irept. These casts are required by other irept derived classes in
+  ///   order to store instances of smt_optiont inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_optiont option);
+    static const smt_optiont &downcast(const irept &);
+  };
+
+protected:
+  explicit smt_optiont(irep_idt id);
+};
+
+template <typename derivedt>
+smt_optiont::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+    std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_termt to store it.");
+}
+
+template <typename derivedt>
+irept smt_optiont::storert<derivedt>::upcast(smt_optiont option)
+{
+  return static_cast<irept &&>(std::move(option));
+}
+
+template <typename derivedt>
+const smt_optiont &smt_optiont::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_optiont &>(irep);
+}
+
+class smt_option_produce_modelst : public smt_optiont
+{
+public:
+  explicit smt_option_produce_modelst(bool setting);
+  bool setting() const;
+};
+
+class smt_option_const_downcast_visitort
+{
+public:
+#define OPTION_ID(the_id) virtual void visit(const smt_option_##the_id##t &) = 0;
+#include "smt_options.def"
+#undef OPTION_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H