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