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
75
76
77
78
79
|
/* Boolector: Satisfiability Modulo Theories (SMT) solver.
*
* Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
*
* This file is part of Boolector.
* See COPYING for more information on using this software.
*/
#include "test.h"
extern "C" {
#include "btorexp.h"
}
class TestMap : public TestBtor
{
};
TEST_F (TestMap, new_delete)
{
BtorNodeMap *map;
map = btor_nodemap_new (d_btor);
btor_nodemap_delete (map);
}
TEST_F (TestMap, map0)
{
Btor *btor_a, *btor_b;
BtorNode *s, *d, *m;
BtorNodeMap *map;
BtorSortId sort;
btor_a = btor_new ();
btor_b = btor_new ();
sort = btor_sort_bv (btor_a, 32);
s = btor_exp_var (btor_a, sort, "s");
btor_sort_release (btor_a, sort);
sort = btor_sort_bv (btor_b, 32);
d = btor_exp_var (btor_b, sort, "d");
btor_sort_release (btor_b, sort);
map = btor_nodemap_new (d_btor);
btor_nodemap_map (map, s, d);
m = btor_nodemap_mapped (map, s);
ASSERT_EQ (m, d);
btor_node_release (btor_a, s);
btor_node_release (btor_b, d);
btor_nodemap_delete (map);
btor_delete (btor_a);
btor_delete (btor_b);
}
TEST_F (TestMap, map1)
{
Btor *btor_a;
BtorNode *s, *t, *a, *m;
BtorSortId sort;
BtorNodeMap *map;
btor_a = btor_new ();
sort = btor_sort_bv (btor_a, 32);
s = btor_exp_var (btor_a, sort, "0");
t = btor_exp_var (btor_a, sort, "1");
a = btor_exp_bv_and (btor_a, s, t);
map = btor_nodemap_new (d_btor);
btor_nodemap_map (map, s, a);
m = btor_nodemap_mapped (map, s);
ASSERT_EQ (m, a);
btor_sort_release (btor_a, sort);
btor_node_release (btor_a, t);
btor_node_release (btor_a, s);
btor_node_release (btor_a, a);
btor_nodemap_delete (map);
btor_delete (btor_a);
}
|
