35 return shared_from_this();
48 if(other->is_bottom())
50 return shared_from_this();
54 auto other_value_set =
58 auto const &other_values = other_value_set->get_values();
59 merged_values.insert(other_values.begin(), other_values.end());
60 return std::make_shared<value_set_abstract_valuet>(
61 type(), std::move(merged_values));
70 values{std::move(values)}
72 if(values.size() > max_value_set_size)
114 std::vector<std::string> vals;
115 for(
const auto &elem :
values)
117 vals.push_back(
expr2c(elem, ns));
120 std::sort(vals.begin(), vals.end());
123 for(
const auto &val : vals)
131 std::shared_ptr<const value_set_abstract_valuet> &out_value,
133 const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
135 std::vector<exprt> &operands_so_far)
137 if(expr.
operands().size() == operands_so_far.size())
139 exprt expr_with_evaluated_operands_filled_in = expr;
140 expr_with_evaluated_operands_filled_in.
operands() = operands_so_far;
141 simplify(expr_with_evaluated_operands_filled_in, ns);
142 if(expr_with_evaluated_operands_filled_in.
is_constant())
146 std::make_shared<value_set_abstract_valuet>(
149 expr_with_evaluated_operands_filled_in}));
151 auto post_merge_casted =
152 std::dynamic_pointer_cast<const value_set_abstract_valuet>(
155 out_value = post_merge_casted;
159 out_value = std::make_shared<value_set_abstract_valuet>(expr.
type());
163 for(
auto const &operand_value :
164 operand_value_sets[operands_so_far.size()]->get_values())
166 operands_so_far.push_back(operand_value);
168 out_value, expr, operand_value_sets, ns, operands_so_far);
169 operands_so_far.pop_back();
174 static std::shared_ptr<const value_set_abstract_valuet>
177 const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
180 const bool is_top =
false;
181 const bool is_bottom =
true;
182 auto result_abstract_value =
183 std::make_shared<const value_set_abstract_valuet>(
184 expr.
type(), is_top, is_bottom);
185 auto operands_so_far = std::vector<exprt>{};
187 result_abstract_value, expr, operand_value_sets, ns, operands_so_far);
188 return result_abstract_value;
193 const std::vector<abstract_object_pointert> &operands,
200 auto operand_value_sets = std::vector<const value_set_abstract_valuet *>{};
201 for(
auto const &possible_value_set : operands)
204 const auto as_value_set =
207 as_value_set ==
nullptr || as_value_set->is_top() ||
208 as_value_set->is_bottom())
210 return std::make_shared<value_set_abstract_valuet>(expr.
type());
212 operand_value_sets.push_back(as_value_set);