cprover
Loading...
Searching...
No Matches
c_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes that are internal to the C frontend
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_expr.h"
10
11#include <util/arith_tools.h>
12
14 exprt vector1,
15 optionalt<exprt> vector2,
16 exprt::operandst indices)
18 ID_shuffle_vector,
19 {std::move(vector1), nil_exprt{}, exprt{}},
20 typet{})
21{
22 if(vector2.has_value())
23 op1() = std::move(*vector2);
24
25 const vector_typet &vt = to_vector_type(op0().type());
26 type() = vector_typet{vt.element_type(),
27 from_integer(indices.size(), vt.size().type())};
28
29 op2().operands().swap(indices);
30}
31
33{
36
37 if(indices().empty())
39
40 auto input_size =
41 numeric_cast<mp_integer>(to_vector_type(vector1().type()).size());
42 CHECK_RETURN(input_size.has_value());
43
45 operands.reserve(indices().size());
46
47 for(const exprt &index : indices())
48 {
50 {
51 operands.push_back(if_exprt{
53 index, ID_lt, from_integer(*input_size, index.type())},
54 index_exprt{vector1(), index},
56 vector2(),
57 minus_exprt{index, from_integer(*input_size, index.type())}}});
58 }
59 else
60 operands.push_back(index_exprt{vector1(), index});
61 }
62
63 return vector_exprt{std::move(operands), type()};
64}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes that are internal to the C frontend.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
Binary minus.
Definition: std_expr.h:973
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
The NIL expression.
Definition: std_expr.h:2874
const vector_typet & type() const
Definition: c_expr.h:27
const exprt & vector2() const
Definition: c_expr.h:47
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:13
const exprt::operandst & indices() const
Definition: c_expr.h:62
vector_exprt lower() const
Definition: c_expr.cpp:32
bool has_two_input_vectors() const
Definition: c_expr.h:57
const exprt & vector1() const
Definition: c_expr.h:37
The type of an expression, extends irept.
Definition: type.h:29
Vector constructor from list of elements.
Definition: std_expr.h:1575
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
nonstd::optional< T > optionalt
Definition: optional.h:35
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040