Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Black box testing of solver functions of the C API.
14 : : */
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5.h>
18 : : }
19 : :
20 : : #include <cmath>
21 : :
22 : : #include "base/check.h"
23 : : #include "base/output.h"
24 : : #include "gtest/gtest.h"
25 : :
26 : : namespace cvc5::internal::test {
27 : :
28 : : class TestCApiBlackStatistics : public ::testing::Test
29 : : {
30 : : protected:
31 : 238 : void SetUp() override
32 : : {
33 : 238 : d_tm = cvc5_term_manager_new();
34 : 238 : d_solver = cvc5_new(d_tm);
35 : 238 : cvc5_check_sat(d_solver);
36 : 238 : }
37 : 213 : void TearDown() override
38 : : {
39 : 213 : cvc5_delete(d_solver);
40 : 213 : cvc5_term_manager_delete(d_tm);
41 : 213 : }
42 : : Cvc5TermManager* d_tm;
43 : : Cvc5* d_solver;
44 : : };
45 : :
46 : 52 : TEST_F(TestCApiBlackStatistics, stat_is_internal)
47 : : {
48 : 26 : ASSERT_DEATH(cvc5_stat_is_internal(nullptr), "invalid statistic");
49 : 25 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
50 : : "theory::strings::checkRuns");
51 [ - + ]: 25 : ASSERT_TRUE(cvc5_stat_is_int(stat));
52 [ - + ]: 25 : ASSERT_TRUE(cvc5_stat_is_internal(stat));
53 : : }
54 : :
55 : 50 : TEST_F(TestCApiBlackStatistics, stat_is_default)
56 : : {
57 : 25 : ASSERT_DEATH(cvc5_stat_is_default(nullptr), "invalid statistic");
58 : 24 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
59 : : "theory::strings::checkRuns");
60 [ - + ]: 24 : ASSERT_TRUE(cvc5_stat_is_int(stat));
61 [ - + ]: 24 : ASSERT_FALSE(cvc5_stat_is_default(stat));
62 : : }
63 : :
64 : 48 : TEST_F(TestCApiBlackStatistics, stat_is_int)
65 : : {
66 : 24 : ASSERT_DEATH(cvc5_stat_is_int(nullptr), "invalid statistic");
67 : 23 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
68 : : "theory::strings::checkRuns");
69 [ - + ]: 23 : ASSERT_TRUE(cvc5_stat_is_int(stat));
70 : : }
71 : :
72 : 46 : TEST_F(TestCApiBlackStatistics, stat_get_int)
73 : : {
74 : 23 : ASSERT_DEATH(cvc5_stat_get_int(nullptr), "invalid statistic");
75 : 22 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
76 : : "theory::strings::checkRuns");
77 [ - + ]: 22 : ASSERT_TRUE(cvc5_stat_is_int(stat));
78 : 22 : (void)cvc5_stat_get_int(stat);
79 : 22 : stat = cvc5_stats_get(cvc5_get_statistics(d_solver), "global::totalTime");
80 [ - + ]: 22 : ASSERT_TRUE(cvc5_stat_is_string(stat));
81 : 22 : ASSERT_DEATH(cvc5_stat_get_int(stat), "expected Stat of type int64_t");
82 : : }
83 : :
84 : 42 : TEST_F(TestCApiBlackStatistics, stat_is_double)
85 : : {
86 : 21 : ASSERT_DEATH(cvc5_stat_is_double(nullptr), "invalid statistic");
87 : : Cvc5Stat stat =
88 : 20 : cvc5_stats_get(cvc5_get_statistics(d_solver), "global::totalTime");
89 [ - + ]: 20 : ASSERT_FALSE(cvc5_stat_is_double(stat));
90 : : }
91 : :
92 : 40 : TEST_F(TestCApiBlackStatistics, stat_get_double)
93 : : {
94 : 20 : ASSERT_DEATH(cvc5_stat_get_double(nullptr), "invalid statistic");
95 : : Cvc5Stat stat =
96 : 19 : cvc5_stats_get(cvc5_get_statistics(d_solver), "global::totalTime");
97 [ - + ]: 19 : ASSERT_FALSE(cvc5_stat_is_double(stat));
98 : 19 : ASSERT_DEATH(cvc5_stat_get_double(stat), "expected Stat of type double");
99 : : }
100 : :
101 : 36 : TEST_F(TestCApiBlackStatistics, stat_is_string)
102 : : {
103 : 18 : ASSERT_DEATH(cvc5_stat_is_string(nullptr), "invalid statistic");
104 : : Cvc5Stat stat =
105 : 17 : cvc5_stats_get(cvc5_get_statistics(d_solver), "global::totalTime");
106 [ - + ]: 17 : ASSERT_TRUE(cvc5_stat_is_string(stat));
107 : : }
108 : :
109 : 34 : TEST_F(TestCApiBlackStatistics, stat_get_string)
110 : : {
111 : 17 : ASSERT_DEATH(cvc5_stat_get_string(nullptr), "invalid statistic");
112 : : Cvc5Stat stat =
113 : 16 : cvc5_stats_get(cvc5_get_statistics(d_solver), "global::totalTime");
114 [ - + ]: 16 : ASSERT_TRUE(cvc5_stat_is_string(stat));
115 : 16 : (void)cvc5_stat_get_string(stat);
116 : 16 : stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
117 : : "theory::strings::checkRuns");
118 [ - + ]: 16 : ASSERT_FALSE(cvc5_stat_is_string(stat));
119 : 16 : ASSERT_DEATH(cvc5_stat_get_string(stat), "expected Stat of type std::string");
120 : : }
121 : :
122 : 30 : TEST_F(TestCApiBlackStatistics, stat_is_histogram)
123 : : {
124 : 15 : ASSERT_DEATH(cvc5_stat_is_histogram(nullptr), "invalid statistic");
125 : 14 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
126 : : "theory::strings::reductions");
127 [ - + ]: 14 : ASSERT_TRUE(cvc5_stat_is_histogram(stat));
128 : : }
129 : :
130 : 28 : TEST_F(TestCApiBlackStatistics, stat_get_histogram)
131 : : {
132 : : const char** keys;
133 : : uint64_t* values;
134 : : size_t size;
135 : 14 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
136 : : "theory::strings::reductions");
137 [ - + ]: 14 : ASSERT_TRUE(cvc5_stat_is_histogram(stat));
138 : 14 : cvc5_stat_get_histogram(stat, &keys, &values, &size);
139 : 14 : ASSERT_DEATH(cvc5_stat_get_histogram(nullptr, &keys, &values, &size),
140 : : "invalid statistic");
141 : 13 : ASSERT_DEATH(cvc5_stat_get_histogram(stat, nullptr, &values, &size),
142 : : "unexpected NULL argument");
143 : 12 : ASSERT_DEATH(cvc5_stat_get_histogram(stat, &keys, nullptr, &size),
144 : : "unexpected NULL argument");
145 : 11 : ASSERT_DEATH(cvc5_stat_get_histogram(stat, &keys, &values, nullptr),
146 : : "unexpected NULL argument");
147 : 10 : stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
148 : : "theory::strings::checkRuns");
149 [ - + ]: 10 : ASSERT_FALSE(cvc5_stat_is_histogram(stat));
150 : 10 : ASSERT_DEATH(cvc5_stat_get_histogram(stat, &keys, &values, &size),
151 : : "expected Stat of typ");
152 : : }
153 : :
154 : 18 : TEST_F(TestCApiBlackStatistics, stat_to_string)
155 : : {
156 : 9 : ASSERT_DEATH(cvc5_stat_to_string(nullptr), "invalid statistic");
157 : 8 : Cvc5Stat stat = cvc5_stats_get(cvc5_get_statistics(d_solver),
158 : : "theory::strings::reductions");
159 : 8 : (void)cvc5_stat_to_string(stat);
160 : : }
161 : :
162 : 16 : TEST_F(TestCApiBlackStatistics, stats_iter_init)
163 : : {
164 : 8 : ASSERT_DEATH(cvc5_stats_iter_init(nullptr, false, false),
165 : : "invalid statistics");
166 : 7 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
167 : 7 : cvc5_stats_iter_init(stats, true, true);
168 : : }
169 : :
170 : 14 : TEST_F(TestCApiBlackStatistics, stats_iter_has_next)
171 : : {
172 : 7 : ASSERT_DEATH(cvc5_stats_iter_has_next(nullptr), "invalid statistics");
173 : 6 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
174 : 6 : ASSERT_DEATH(cvc5_stats_iter_has_next(stats), "iterator not initialized");
175 : 5 : cvc5_stats_iter_init(stats, true, true);
176 [ - + ]: 5 : ASSERT_TRUE(cvc5_stats_iter_has_next(stats));
177 : : }
178 : :
179 : 10 : TEST_F(TestCApiBlackStatistics, stats_iter_next)
180 : : {
181 : 5 : ASSERT_DEATH(cvc5_stats_iter_next(nullptr, nullptr), "invalid statistics");
182 : 4 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
183 : 4 : cvc5_stats_iter_init(stats, true, true);
184 [ - + ]: 4 : ASSERT_TRUE(cvc5_stats_iter_has_next(stats));
185 : 4 : (void)cvc5_stats_iter_next(stats, nullptr);
186 : : }
187 : :
188 : 8 : TEST_F(TestCApiBlackStatistics, stats_get)
189 : : {
190 : 4 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
191 : 4 : ASSERT_DEATH(cvc5_stats_get(nullptr, "global::totalTime"),
192 : : "invalid statistics");
193 : 3 : ASSERT_DEATH(cvc5_stats_get(stats, nullptr), "unexpected NULL argument");
194 : 2 : (void)cvc5_stats_get(stats, "global::totalTime");
195 : : }
196 : :
197 : 4 : TEST_F(TestCApiBlackStatistics, stats_to_string)
198 : : {
199 : 2 : ASSERT_DEATH(cvc5_stats_to_string(nullptr), "invalid statistics");
200 : 1 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
201 : 1 : (void)cvc5_stats_to_string(stats);
202 : : }
203 : :
204 : : } // namespace cvc5::internal::test
|
