cprover
Loading...
Searching...
No Matches
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>
9#include <util/std_expr.h>
10#include <util/std_types.h>
11#include <util/type.h>
12
14{
15private:
18
21 {
22 }
23
24 void visit(const smt_bool_literal_termt &bool_literal) override
25 {
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 {
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 {
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
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 {
64 false,
65 "Unexpected conversion of function application to value expression.");
66 }
67
68public:
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)
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
mp_integer value() const
Definition smt_terms.cpp:98
std::size_t bit_width() const
Definition smt_sorts.cpp:60
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:81
void accept(smt_term_const_downcast_visitort &) const
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
Pre-defined types.
Defines typet, type_with_subtypet and type_with_subtypest.