cprover
construct_value_expr_from_smt.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
6 
7 #include <util/arith_tools.h>
8 #include <util/bitvector_types.h>
9 #include <util/std_expr.h>
10 #include <util/std_types.h>
11 #include <util/type.h>
12 
14 {
15 private:
18 
21  {
22  }
23 
24  void visit(const smt_bool_literal_termt &bool_literal) override
25  {
26  INVARIANT(
28  "Bool terms may only be used to construct bool typed expressions.");
29  result = bool_literal.value() ? (exprt)true_exprt{} : false_exprt{};
30  }
31 
32  void visit(const smt_identifier_termt &identifier_term) override
33  {
34  INVARIANT(
35  false, "Unexpected conversion of identifier to value expression.");
36  }
37 
38  void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
39  {
40  if(
41  const auto bitvector_type =
42  type_try_dynamic_cast<bitvector_typet>(type_to_construct))
43  {
44  INVARIANT(
45  bitvector_type->get_width() ==
46  bit_vector_constant.get_sort().bit_width(),
47  "Width of smt bit vector term must match the width of bit vector "
48  "type.");
49  result = from_integer(bit_vector_constant.value(), type_to_construct);
50  return;
51  }
52 
53  INVARIANT(
54  false,
55  "construct_value_expr_from_smt for bit vector should not be applied to "
56  "unsupported type " +
58  }
59 
60  void
61  visit(const smt_function_application_termt &function_application) override
62  {
63  INVARIANT(
64  false,
65  "Unexpected conversion of function application to value expression.");
66  }
67 
68 public:
72  static exprt make(const smt_termt &value_term, const typet &type_to_construct)
73  {
75  value_term.accept(factory);
76  INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
77  return *factory.result;
78  }
79 };
80 
82  const smt_termt &value_term,
83  const typet &type_to_construct)
84 {
85  return value_expr_from_smt_factoryt::make(value_term, type_to_construct);
86 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Pre-defined bitvector types.
The Boolean type.
Definition: std_types.h:36
Base class for all expressions.
Definition: expr.h:54
The Boolean constant false.
Definition: std_expr.h:2865
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:103
mp_integer value() const
Definition: smt_terms.cpp:98
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
bool value() const
Definition: smt_terms.cpp:46
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
void accept(smt_term_const_downcast_visitort &) const
Definition: smt_terms.cpp:150
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
value_expr_from_smt_factoryt(const typet &type_to_construct)
void visit(const smt_bool_literal_termt &bool_literal) override
void visit(const smt_function_application_termt &function_application) override
void visit(const smt_identifier_termt &identifier_term) override
void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
static exprt make(const smt_termt &value_term, const typet &type_to_construct)
This function is complete the external interface to this class.
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.
Pre-defined types.
Defines typet, type_with_subtypet and type_with_subtypest.