1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
/*******************************************************************\
Module: Unit tests for union_find_replacet in
solvers/refinement/string_refinement.cpp
Author: Diffblue Ltd.
\*******************************************************************/
#include <testing-utils/use_catch.h>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/union_find_replace.h>
SCENARIO("union_find_replace", "[core][solvers][strings][string_refinement]")
{
GIVEN("An empty dictionary")
{
union_find_replacet dict;
pointer_typet char_pointer_type = pointer_type(unsignedbv_typet(16));
const symbol_exprt a("a", char_pointer_type);
const symbol_exprt b("b", char_pointer_type);
const symbol_exprt c("c", char_pointer_type);
const symbol_exprt d("d", char_pointer_type);
const symbol_exprt e("e", char_pointer_type);
const symbol_exprt f("f", char_pointer_type);
WHEN("Relations a=b, a=c, d=b, e=f are added")
{
dict.make_union(a, b);
dict.make_union(a, c);
dict.make_union(d, b);
dict.make_union(e, f);
THEN("find(d)=find(c), but find(e)!=find(a)")
{
REQUIRE(dict.find(d) == dict.find(c)); // transitive equality
REQUIRE(dict.find(a) == dict.find(a)); // trivial equality
REQUIRE(dict.find(b) == dict.find(d)); // rhs only symbol
REQUIRE(dict.find(b) == dict.find(c)); // rhs only transitive
REQUIRE(dict.find(e) != dict.find(a)); // transitive not equal
REQUIRE(dict.find(f) != dict.find(a)); // transitive not equal
}
GIVEN("Expressions a+e, a+d, c+f, c+d")
{
plus_exprt a_plus_e(a, e);
plus_exprt a_plus_d(a, d);
plus_exprt c_plus_f(c, f);
plus_exprt c_plus_d(c, d);
WHEN("We use the dictionary for replacement")
{
dict.replace_expr(a_plus_e);
dict.replace_expr(a_plus_d);
dict.replace_expr(c_plus_f);
dict.replace_expr(c_plus_d);
THEN("a+e=c+f but a+e!=c+d")
{
REQUIRE(a_plus_e == c_plus_f);
REQUIRE(a_plus_e != c_plus_d);
REQUIRE(a_plus_d == c_plus_d);
}
}
}
THEN("Introducing cycles does not cause infinite loops or exceptions")
{
dict.make_union(c, d);
REQUIRE(dict.find(d) == dict.find(c));
REQUIRE(dict.find(e) != dict.find(a));
}
}
}
}
|
