Implement construction of exprt booleans from smt terms

Author: thomasspriggs

src/solvers/Makefile

@@ -193,6 +193,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -0,0 +1,67 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/type.h>
+
+class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
+{
+private:
+  const typet &type_to_construct;
+  optionalt<exprt> result;
+
+  explicit value_expr_from_smt_factoryt(const typet &type_to_construct)
+    : type_to_construct{type_to_construct}, result{}
+  {
+  }
+
+  void visit(const smt_bool_literal_termt &bool_literal) override
+  {
+    INVARIANT(
+      type_to_construct == bool_typet{},
+      "Bool terms may only be used to construct bool typed expressions.");
+    result = bool_literal.value() ? (exprt)true_exprt{} : false_exprt{};
+  }
+
+  void visit(const smt_identifier_termt &identifier_term) override
+  {
+    INVARIANT(
+      false, "Unexpected conversion of identifier to value expression.");
+  }
+
+  void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
+  {
+    UNIMPLEMENTED;
+  }
+
+  void
+  visit(const smt_function_application_termt &function_application) override
+  {
+    INVARIANT(
+      false,
+      "Unexpected conversion of function application to value expression.");
+  }
+
+public:
+  /// \brief This function is complete the external interface to this class. All
+  ///   construction of this class and construction of expressions should be
+  ///   carried out via this function.
+  static exprt make(const smt_termt &value_term, const typet &type_to_construct)
+  {
+    value_expr_from_smt_factoryt factory{type_to_construct};
+    value_term.accept(factory);
+    INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
+    return *factory.result;
+  }
+};
+
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct)
+{
+  return value_expr_from_smt_factoryt::make(value_term, type_to_construct);
+}

src/solvers/smt2_incremental/construct_value_expr_from_smt.h

@@ -0,0 +1,31 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
+
+#include <util/expr.h>
+
+class smt_termt;
+class typet;
+
+/// \brief Given a \p value_term and a \p type_to_construct, this function
+/// constructs a value exprt with a value based on \p value_term and a type of
+/// \p type_to_construct.
+/// \param value_term
+///   This must be a "simple" term encoding a value. It must not be a term
+///   requiring any kind of further evaluation to get a value, such as would be
+///   the case for identifiers or function applications.
+/// \param type_to_construct
+///   The type which the constructed expr returned is expected to have. This
+///   type must be compatible with the sort of \p value_term.
+/// \note The type is required separately in order to carry out this conversion,
+/// because the smt value term does not contain all the required information.
+/// For example an 8 bit, bit vector with a value of 255 could be used to
+/// construct an `unsigned char` with the value 255 or alternatively a
+/// `signed char` with the value -1. So these alternatives are disambiguated
+/// using the type.
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

unit/Makefile

@@ -100,6 +100,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/smt2/smt2_conv.cpp \
        solvers/smt2/smt2irep.cpp \
+       solvers/smt2_incremental/construct_value_expr_from_smt.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
        solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -0,0 +1,30 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
+{
+  optionalt<smt_termt> input_term;
+  optionalt<exprt> expected_result;
+
+  using rowt = std::pair<smt_termt, exprt>;
+  std::tie(input_term, expected_result) = GENERATE(
+    rowt{smt_bool_literal_termt{true}, true_exprt{}},
+    rowt{smt_bool_literal_termt{false}, false_exprt{}});
+  SECTION(
+    "Construction of \"" + id2string(expected_result->type().id()) +
+    "\" from \"" + smt_to_smt2_string(*input_term) + "\"")
+  {
+    REQUIRE(
+      construct_value_expr_from_smt(*input_term, expected_result->type()) ==
+      *expected_result);
+  }
+}