Add incremental SMT2 sort checked construction of bit vector predicate application and application of core theory functions

src/solvers/Makefile

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

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -0,0 +1,44 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+
+#include <util/invariant.h>
+
+static void validate_bit_vector_predicate_arguments(
+  const smt_termt &left,
+  const smt_termt &right)
+{
+  const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(left_sort, "Left operand must have bitvector sort.");
+  const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(right_sort, "Right operand must have bitvector sort.");
+  // The below invariant is based on the smtlib standard.
+  // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
+  INVARIANT(
+    left_sort->bit_width() == right_sort->bit_width(),
+    "Left and right operands must have the same bit width.");
+}
+
+#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)               \
+  void smt_bit_vector_theoryt::the_name##t::validate(                          \
+    const smt_termt &left, const smt_termt &right)                             \
+  {                                                                            \
+    validate_bit_vector_predicate_arguments(left, right);                      \
+  }                                                                            \
+                                                                               \
+  smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort(                  \
+    const smt_termt &, const smt_termt &)                                      \
+  {                                                                            \
+    return smt_bool_sortt{};                                                   \
+  }                                                                            \
+                                                                               \
+  const char *smt_bit_vector_theoryt::the_name##t::identifier()                \
+  {                                                                            \
+    return #the_identifier;                                                    \
+  }                                                                            \
+                                                                               \
+  const smt_function_application_termt::factoryt<                              \
+    smt_bit_vector_theoryt::the_name##t>                                       \
+    smt_bit_vector_theoryt::the_name{};
+#include "smt_bit_vector_theory.def"
+#undef SMT_BITVECTOR_THEORY_PREDICATE

src/solvers/smt2_incremental/smt_bit_vector_theory.def

@@ -0,0 +1,13 @@
+/// \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 bitvector theory functions which are implemented and it is used to
+/// automate repetitive parts of the implementation.
+SMT_BITVECTOR_THEORY_PREDICATE(bvult, unsigned_less_than)
+SMT_BITVECTOR_THEORY_PREDICATE(bvule, unsigned_less_than_or_equal)
+SMT_BITVECTOR_THEORY_PREDICATE(bvugt, unsigned_greater_than)
+SMT_BITVECTOR_THEORY_PREDICATE(bvuge, unsigned_greater_than_or_equal)
+SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than)
+SMT_BITVECTOR_THEORY_PREDICATE(bvsle, signed_less_than_or_equal)
+SMT_BITVECTOR_THEORY_PREDICATE(bvsgt, signed_greater_than)
+SMT_BITVECTOR_THEORY_PREDICATE(bvsge, signed_greater_than_or_equal)

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -0,0 +1,25 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+class smt_bit_vector_theoryt
+{
+public:
+#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)               \
+  /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */  \
+  struct the_name##t final                                                     \
+  {                                                                            \
+    static const char *identifier();                                           \
+    static smt_sortt                                                           \
+    return_sort(const smt_termt &left, const smt_termt &right);                \
+    static void validate(const smt_termt &left, const smt_termt &right);       \
+  };                                                                           \
+  static const smt_function_application_termt::factoryt<the_name##t> the_name;
+#include "smt_bit_vector_theory.def"
+#undef SMT_BITVECTOR_THEORY_PREDICATE
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

src/solvers/smt2_incremental/smt_commands.cpp

@@ -198,3 +198,51 @@ void smt_commandt::accept(smt_command_const_downcast_visitort &&visitor) const
 {
   ::accept(*this, id(), std::move(visitor));
 }
+
+smt_command_functiont::smt_command_functiont(
+  const smt_declare_function_commandt &function_declaration)
+  : _identifier(function_declaration.identifier())
+{
+  const auto sort_references = function_declaration.parameter_sorts();
+  parameter_sorts =
+    make_range(sort_references).collect<decltype(parameter_sorts)>();
+}
+
+smt_command_functiont::smt_command_functiont(
+  const smt_define_function_commandt &function_definition)
+  : _identifier{function_definition.identifier()}
+{
+  const auto parameters = function_definition.parameters();
+  parameter_sorts =
+    make_range(parameters)
+      .map([](const smt_termt &term) { return term.get_sort(); })
+      .collect<decltype(parameter_sorts)>();
+}
+
+irep_idt smt_command_functiont::identifier() const
+{
+  return _identifier.identifier();
+}
+
+smt_sortt smt_command_functiont::return_sort(
+  const std::vector<smt_termt> &arguments) const
+{
+  return _identifier.get_sort();
+}
+
+void smt_command_functiont::validate(
+  const std::vector<smt_termt> &arguments) const
+{
+  INVARIANT(
+    parameter_sorts.size() == arguments.size(),
+    "Number of parameters and number of arguments must be the same.");
+  const auto parameter_sort_arguments =
+    make_range(parameter_sorts).zip(make_range(arguments));
+  for(const auto &parameter_sort_argument_pair : parameter_sort_arguments)
+  {
+    INVARIANT(
+      parameter_sort_argument_pair.first ==
+        parameter_sort_argument_pair.second.get_sort(),
+      "Sort of argument must have the same sort as the parameter.");
+  }
+}

src/solvers/smt2_incremental/smt_commands.h

@@ -132,4 +132,22 @@ class smt_command_const_downcast_visitort
 #undef COMMAND_ID
 };
 
+/// \brief A function generated from a command. Used for validating function
+///   application term arguments.
+class smt_command_functiont
+{
+private:
+  std::vector<smt_sortt> parameter_sorts;
+  smt_identifier_termt _identifier;
+
+public:
+  explicit smt_command_functiont(
+    const smt_declare_function_commandt &function_declaration);
+  explicit smt_command_functiont(
+    const smt_define_function_commandt &function_definition);
+  irep_idt identifier() const;
+  smt_sortt return_sort(const std::vector<smt_termt> &arguments) const;
+  void validate(const std::vector<smt_termt> &arguments) const;
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H

src/solvers/smt2_incremental/smt_core_theory.cpp

@@ -0,0 +1,200 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_core_theory.h>
+
+const char *smt_core_theoryt::nott::identifier()
+{
+  return "not";
+}
+
+smt_sortt smt_core_theoryt::nott::return_sort(const smt_termt &operand)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::nott::validate(const smt_termt &operand)
+{
+  INVARIANT(
+    operand.get_sort() == smt_bool_sortt{},
+    "\"not\" may only be applied to terms which have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::nott>
+  smt_core_theoryt::make_not{};
+
+const char *smt_core_theoryt::impliest::identifier()
+{
+  return "=>";
+}
+
+smt_sortt
+smt_core_theoryt::impliest::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::impliest::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == smt_bool_sortt{},
+    "Left hand side of \"=>\" must have bool sort.");
+  INVARIANT(
+    rhs.get_sort() == smt_bool_sortt{},
+    "Right hand side of \"=>\" must have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::impliest>
+  smt_core_theoryt::implies{};
+
+const char *smt_core_theoryt::andt::identifier()
+{
+  return "and";
+}
+
+smt_sortt
+smt_core_theoryt::andt::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::andt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == smt_bool_sortt{},
+    "Left hand side of \"and\" must have bool sort.");
+  INVARIANT(
+    rhs.get_sort() == smt_bool_sortt{},
+    "Right hand side of \"and\" must have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::andt>
+  smt_core_theoryt::make_and{};
+
+const char *smt_core_theoryt::ort::identifier()
+{
+  return "or";
+}
+
+smt_sortt
+smt_core_theoryt::ort::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::ort::validate(const smt_termt &lhs, const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == smt_bool_sortt{},
+    "Left hand side of \"or\" must have bool sort.");
+  INVARIANT(
+    rhs.get_sort() == smt_bool_sortt{},
+    "Right hand side of \"or\" must have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::ort>
+  smt_core_theoryt::make_or{};
+
+const char *smt_core_theoryt::xort::identifier()
+{
+  return "xor";
+}
+
+smt_sortt
+smt_core_theoryt::xort::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::xort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == smt_bool_sortt{},
+    "Left hand side of \"xor\" must have bool sort.");
+  INVARIANT(
+    rhs.get_sort() == smt_bool_sortt{},
+    "Right hand side of \"xor\" must have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::xort>
+  smt_core_theoryt::make_xor{};
+
+const char *smt_core_theoryt::equalt::identifier()
+{
+  return "=";
+}
+
+smt_sortt
+smt_core_theoryt::equalt::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::equalt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == rhs.get_sort(),
+    "\"=\" may only be applied to terms which have the same sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::equalt>
+  smt_core_theoryt::equal{};
+
+const char *smt_core_theoryt::distinctt::identifier()
+{
+  return "distinct";
+}
+
+smt_sortt
+smt_core_theoryt::distinctt::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::distinctt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == rhs.get_sort(),
+    "\"distinct\" may only be applied to terms which have the same sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::distinctt>
+  smt_core_theoryt::distinct{};
+
+const char *smt_core_theoryt::if_then_elset::identifier()
+{
+  return "ite";
+}
+
+smt_sortt smt_core_theoryt::if_then_elset::return_sort(
+  const smt_termt &,
+  const smt_termt &then_term,
+  const smt_termt &)
+{
+  return then_term.get_sort();
+}
+
+void smt_core_theoryt::if_then_elset::validate(
+  const smt_termt &condition,
+  const smt_termt &then_term,
+  const smt_termt &else_term)
+{
+  INVARIANT(
+    condition.get_sort() == smt_bool_sortt{},
+    "Condition term must have bool sort.");
+  INVARIANT(
+    then_term.get_sort() == else_term.get_sort(),
+    "\"ite\" must have \"then\" and \"else\" terms of the same sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::if_then_elset>
+  smt_core_theoryt::if_then_else;