Skip to content

Commit b3baa40

Browse files
committed
Improve value_set to_constant()
For multi-valued sets, calculate the interval then, if it's a single value interval return a constant, otherwise use the base operation.
1 parent 714cee3 commit b3baa40

File tree

2 files changed

+22
-2
lines changed

2 files changed

+22
-2
lines changed

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -166,8 +166,15 @@ value_set_abstract_objectt::value_range_implementation() const
166166
exprt value_set_abstract_objectt::to_constant() const
167167
{
168168
verify();
169-
return values.size() == 1 ? (*values.begin())->to_constant()
170-
: abstract_objectt::to_constant();
169+
170+
if(values.size() == 1)
171+
return values.first()->to_constant();
172+
173+
auto interval = to_interval();
174+
if(interval.is_single_value_interval())
175+
return interval.get_lower();
176+
177+
return abstract_objectt::to_constant();
171178
}
172179

173180
constant_interval_exprt value_set_abstract_objectt::to_interval() const

unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -354,6 +354,19 @@ SCENARIO(
354354
EXPECT_UNMODIFIED(merged, val1);
355355
}
356356
}
357+
WHEN("merging 1 with { 1, [1, 1] }")
358+
{
359+
auto op1 = make_constant(val1, environment, ns);
360+
auto op2 = make_value_set(
361+
{val1, constant_interval_exprt(val1, val1)}, environment, ns);
362+
363+
auto merged = merge(op1, op2);
364+
365+
THEN("result is unmodified 1")
366+
{
367+
EXPECT_UNMODIFIED(merged, val1);
368+
}
369+
}
357370
WHEN("merging 1 with { [ 2, 2 ] }")
358371
{
359372
auto op1 = make_constant(val1, environment, ns);

0 commit comments

Comments
 (0)