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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
/* 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 "btoraig.h"
#include "dumper/btordumpaig.h"
}
class TestAig : public TestBtor
{
protected:
void binary_commutative_aig_test (BtorAIG *(*func) (BtorAIGMgr *,
BtorAIG *,
BtorAIG *) )
{
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
BtorAIG *aig1 = btor_aig_var (amgr);
BtorAIG *aig2 = btor_aig_var (amgr);
BtorAIG *aig3 = func (amgr, aig1, aig2);
BtorAIG *aig4 = func (amgr, aig1, aig2);
BtorAIG *aig5 = func (amgr, aig2, aig1);
ASSERT_TRUE (aig3 == aig4);
ASSERT_TRUE (aig4 == aig5);
btor_dumpaig_dump_aig (amgr, 0, d_log_file, aig5);
btor_aig_release (amgr, aig1);
btor_aig_release (amgr, aig2);
btor_aig_release (amgr, aig3);
btor_aig_release (amgr, aig4);
btor_aig_release (amgr, aig5);
btor_aig_mgr_delete (amgr);
}
};
TEST_F (TestAig, new_delete_aig_mgr)
{
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, false)
{
open_log_file ("false_aig");
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
btor_dumpaig_dump_aig (amgr, 0, d_log_file, BTOR_AIG_FALSE);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, true)
{
open_log_file ("true_aig");
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
btor_dumpaig_dump_aig (amgr, 0, d_log_file, BTOR_AIG_TRUE);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, var)
{
open_log_file ("var_aig");
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
BtorAIG *var = btor_aig_var (amgr);
ASSERT_TRUE (btor_aig_is_var (var));
btor_dumpaig_dump_aig (amgr, 0, d_log_file, var);
btor_aig_release (amgr, var);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, not)
{
open_log_file ("not_aig");
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
BtorAIG *var = btor_aig_var (amgr);
BtorAIG *_not = btor_aig_not (amgr, var);
btor_dumpaig_dump_aig (amgr, 0, d_log_file, _not);
btor_aig_release (amgr, var);
btor_aig_release (amgr, _not);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, and)
{
open_log_file ("and_aig");
binary_commutative_aig_test (btor_aig_and);
}
TEST_F (TestAig, or)
{
open_log_file ("or_aig");
binary_commutative_aig_test (btor_aig_or);
}
TEST_F (TestAig, eq)
{
open_log_file ("eq_aig");
binary_commutative_aig_test (btor_aig_eq);
}
TEST_F (TestAig, cond)
{
open_log_file ("cond_aig");
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
BtorAIG *aig1 = btor_aig_var (amgr);
BtorAIG *aig2 = btor_aig_var (amgr);
BtorAIG *aig3 = btor_aig_var (amgr);
BtorAIG *aig4 = btor_aig_cond (amgr, aig1, aig2, aig3);
BtorAIG *aig5 = btor_aig_cond (amgr, aig1, aig2, aig3);
ASSERT_TRUE (aig4 == aig5);
btor_dumpaig_dump_aig (amgr, 0, d_log_file, aig5);
btor_aig_release (amgr, aig1);
btor_aig_release (amgr, aig2);
btor_aig_release (amgr, aig3);
btor_aig_release (amgr, aig4);
btor_aig_release (amgr, aig5);
btor_aig_mgr_delete (amgr);
}
TEST_F (TestAig, aig_to_sat)
{
BtorAIGMgr *amgr = btor_aig_mgr_new (d_btor);
BtorSATMgr *smgr = btor_aig_get_sat_mgr (amgr);
BtorAIG *var1 = btor_aig_var (amgr);
BtorAIG *var2 = btor_aig_var (amgr);
BtorAIG *var3 = btor_aig_var (amgr);
BtorAIG *var4 = btor_aig_var (amgr);
BtorAIG *and1 = btor_aig_and (amgr, var1, var2);
BtorAIG *and2 = btor_aig_and (amgr, var3, var4);
BtorAIG *and3 = btor_aig_or (amgr, and1, and2);
btor_sat_enable_solver (smgr);
btor_sat_init (smgr);
btor_aig_to_sat (amgr, and3);
btor_sat_reset (smgr);
btor_aig_release (amgr, var1);
btor_aig_release (amgr, var2);
btor_aig_release (amgr, var3);
btor_aig_release (amgr, var4);
btor_aig_release (amgr, and1);
btor_aig_release (amgr, and2);
btor_aig_release (amgr, and3);
btor_aig_mgr_delete (amgr);
}
|
