Add smt commands

Author: thomasspriggs

src/solvers/Makefile

@@ -192,6 +192,9 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/smt_commands.cpp \
+      smt2_incremental/smt_logics.cpp \
+      smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \

src/solvers/smt2_incremental/smt_commands.cpp

@@ -0,0 +1,174 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_commands.h>
+
+#include <util/range.h>
+
+// Define the irep_idts for commands.
+#define COMMAND_ID(the_id)                                                     \
+  const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
+#include <solvers/smt2_incremental/smt_commands.def>
+#undef COMMAND_ID
+
+bool smt_commandt::operator==(const smt_commandt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_commandt::operator!=(const smt_commandt &other) const
+{
+  return !(*this == other);
+}
+
+smt_assert_commandt::smt_assert_commandt(smt_termt condition)
+  : smt_commandt{ID_smt_assert_command}
+{
+  INVARIANT(
+    condition.get_sort() == smt_bool_sortt{},
+    "Only terms with boolean sorts can be asserted.");
+  set(ID_cond, upcast(std::move(condition)));
+}
+
+const smt_termt &smt_assert_commandt::condition() const
+{
+  return downcast(find(ID_cond));
+}
+
+smt_check_sat_commandt::smt_check_sat_commandt()
+  : smt_commandt{ID_smt_check_sat_command}
+{
+}
+
+smt_declare_function_commandt::smt_declare_function_commandt(
+  smt_identifier_termt identifier,
+  std::vector<smt_sortt> parameter_sorts)
+  : smt_commandt{ID_smt_declare_function_command}
+{
+  set(ID_identifier, term_storert::upcast(std::move(identifier)));
+  std::transform(
+    std::make_move_iterator(parameter_sorts.begin()),
+    std::make_move_iterator(parameter_sorts.end()),
+    std::back_inserter(get_sub()),
+    [](smt_sortt &&parameter_sort) {
+      return sort_storert::upcast(std::move(parameter_sort));
+    });
+}
+
+const smt_identifier_termt &smt_declare_function_commandt::identifier() const
+{
+  return static_cast<const smt_identifier_termt &>(
+    term_storert::downcast(find(ID_identifier)));
+}
+
+const smt_sortt &smt_declare_function_commandt::return_sort() const
+{
+  return identifier().get_sort();
+}
+
+std::vector<std::reference_wrapper<const smt_sortt>>
+smt_declare_function_commandt::parameter_sorts() const
+{
+  return make_range(get_sub()).map([](const irept &parameter_sort) {
+    return std::cref(sort_storert::downcast(parameter_sort));
+  });
+}
+
+smt_exit_commandt::smt_exit_commandt() : smt_commandt{ID_smt_exit_command}
+{
+}
+
+smt_define_function_commandt::smt_define_function_commandt(
+  irep_idt identifier,
+  std::vector<smt_identifier_termt> parameters,
+  smt_termt definition)
+  : smt_commandt{ID_smt_define_function_command}
+{
+  set(ID_identifier, identifier);
+  std::transform(
+    std::make_move_iterator(parameters.begin()),
+    std::make_move_iterator(parameters.end()),
+    std::back_inserter(get_sub()),
+    [](smt_identifier_termt &&parameter) {
+      return upcast(std::move(parameter));
+    });
+  set(ID_code, upcast(std::move(definition)));
+}
+
+const irep_idt &smt_define_function_commandt::identifier() const
+{
+  return get(ID_identifier);
+}
+
+std::vector<std::reference_wrapper<const smt_identifier_termt>>
+smt_define_function_commandt::parameters() const
+{
+  return make_range(get_sub()).map([](const irept &parameter) {
+    return std::cref(
+      static_cast<const smt_identifier_termt &>(downcast((parameter))));
+  });
+}
+
+const smt_sortt &smt_define_function_commandt::return_sort() const
+{
+  return definition().get_sort();
+}
+
+const smt_termt &smt_define_function_commandt::definition() const
+{
+  return downcast(find(ID_code));
+}
+
+smt_get_value_commandt::smt_get_value_commandt(smt_termt descriptor)
+  : smt_commandt{ID_smt_get_value_command}
+{
+  set(ID_value, upcast(std::move(descriptor)));
+}
+
+const smt_termt &smt_get_value_commandt::descriptor() const
+{
+  return downcast(find(ID_value));
+}
+
+smt_push_commandt::smt_push_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_push_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_push_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_pop_commandt::smt_pop_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_pop_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_pop_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_set_logic_commandt::smt_set_logic_commandt(smt_logict logic)
+  : smt_commandt(ID_smt_set_logic_command)
+{
+  set(ID_value, upcast(std::move(logic)));
+}
+
+const smt_logict &smt_set_logic_commandt::logic() const
+{
+  return downcast(find(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));
+}

src/solvers/smt2_incremental/smt_commands.def

@@ -0,0 +1,16 @@
+/// \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 commands 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 command classes.
+COMMAND_ID(assert)
+COMMAND_ID(check_sat)
+COMMAND_ID(declare_function)
+COMMAND_ID(define_function)
+COMMAND_ID(exit)
+COMMAND_ID(get_value)
+COMMAND_ID(pop)
+COMMAND_ID(push)
+COMMAND_ID(set_logic)
+COMMAND_ID(set_option)

src/solvers/smt2_incremental/smt_commands.h

@@ -0,0 +1,121 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
+
+#include <solvers/smt2_incremental/smt_logics.h>
+#include <solvers/smt2_incremental/smt_options.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <util/irep.h>
+
+class smt_commandt : protected irept
+{
+public:
+  // smt_commandt does not support the notion of an empty / null state. Use
+  // optionalt<smt_commandt> instead if an empty command is required.
+  smt_commandt() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_commandt &) const;
+  bool operator!=(const smt_commandt &) const;
+
+protected:
+  using irept::irept;
+};
+
+class smt_assert_commandt : public smt_commandt,
+                            private smt_termt::storert<smt_assert_commandt>
+{
+public:
+  explicit smt_assert_commandt(smt_termt condition);
+  const smt_termt &condition() const;
+};
+
+class smt_check_sat_commandt : public smt_commandt
+{
+public:
+  smt_check_sat_commandt();
+};
+
+class smt_declare_function_commandt
+  : public smt_commandt,
+    private smt_sortt::storert<smt_declare_function_commandt>,
+    private smt_termt::storert<smt_declare_function_commandt>
+{
+public:
+  smt_declare_function_commandt(
+    smt_identifier_termt identifier,
+    std::vector<smt_sortt> parameter_sorts);
+  const smt_identifier_termt &identifier() const;
+  const smt_sortt &return_sort() const;
+  std::vector<std::reference_wrapper<const smt_sortt>> parameter_sorts() const;
+
+private:
+  using sort_storert = smt_sortt::storert<smt_declare_function_commandt>;
+  using term_storert = smt_termt::storert<smt_declare_function_commandt>;
+};
+
+class smt_define_function_commandt
+  : public smt_commandt,
+    private smt_termt::storert<smt_define_function_commandt>
+{
+public:
+  smt_define_function_commandt(
+    irep_idt identifier,
+    std::vector<smt_identifier_termt> parameters,
+    smt_termt definition);
+  const irep_idt &identifier() const;
+  std::vector<std::reference_wrapper<const smt_identifier_termt>>
+  parameters() const;
+  const smt_sortt &return_sort() const;
+  const smt_termt &definition() const;
+};
+
+class smt_exit_commandt : public smt_commandt
+{
+public:
+  smt_exit_commandt();
+};
+
+class smt_get_value_commandt : public smt_commandt,
+                               protected smt_termt::storert<smt_assert_commandt>
+{
+public:
+  explicit smt_get_value_commandt(smt_termt descriptor);
+  const smt_termt &descriptor() const;
+};
+
+class smt_push_commandt : public smt_commandt
+{
+public:
+  explicit smt_push_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
+class smt_pop_commandt : public smt_commandt
+{
+public:
+  explicit smt_pop_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
+class smt_set_logic_commandt
+  : public smt_commandt,
+    private smt_logict::storert<smt_set_logic_commandt>
+{
+public:
+  explicit smt_set_logic_commandt(smt_logict logic);
+  const smt_logict &logic() const;
+};
+
+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;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H

src/solvers/smt2_incremental/smt_logics.cpp

@@ -0,0 +1,47 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_logics.h>
+
+// Define the irep_idts for logics.
+#define LOGIC_ID(the_id)                                                       \
+  const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
+#include <solvers/smt2_incremental/smt_logics.def>
+#undef LOGIC_ID
+
+bool smt_logict::operator==(const smt_logict &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_logict::operator!=(const smt_logict &other) const
+{
+  return !(*this == other);
+}
+
+template <typename visitort>
+void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
+{
+#define LOGIC_ID(the_id)                                                       \
+  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
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_logics.def> // NOLINT(build/include)
+#undef LOGIC_ID
+  UNREACHABLE;
+}
+
+void smt_logict::accept(smt_logic_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+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}
+{
+}

src/solvers/smt2_incremental/smt_logics.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 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)