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 proof-related functions of the C API.
14 : : */
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5.h>
18 : : }
19 : :
20 : : #include "base/check.h"
21 : : #include "base/output.h"
22 : : #include "gtest/gtest.h"
23 : :
24 : : namespace cvc5::internal::test {
25 : :
26 : : class TestCApiBlackProof : public ::testing::Test
27 : : {
28 : : protected:
29 : 53 : void SetUp() override
30 : : {
31 : 53 : d_tm = cvc5_term_manager_new();
32 : 53 : d_solver = cvc5_new(d_tm);
33 : 53 : d_bool = cvc5_get_boolean_sort(d_tm);
34 : 53 : d_int = cvc5_get_integer_sort(d_tm);
35 : 53 : d_real = cvc5_get_real_sort(d_tm);
36 : 53 : d_str = cvc5_get_string_sort(d_tm);
37 : 53 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
38 : 53 : }
39 : 42 : void TearDown() override
40 : : {
41 : 42 : cvc5_delete(d_solver);
42 : 42 : cvc5_term_manager_delete(d_tm);
43 : 42 : }
44 : :
45 : 38 : Cvc5Proof create_proof()
46 : : {
47 : 38 : cvc5_set_option(d_solver, "produce-proofs", "true");
48 : 76 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
49 : : Cvc5Sort u_to_int =
50 : 38 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
51 : 38 : domain = {d_int};
52 : : Cvc5Sort int_pred =
53 : 38 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
54 : :
55 : 38 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
56 : 38 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
57 : 38 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f");
58 : 38 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p");
59 : 38 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
60 : 38 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
61 : 38 : std::vector<Cvc5Term> args = {f, x};
62 : : Cvc5Term f_x =
63 : 38 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
64 : 38 : args = {f, y};
65 : : Cvc5Term f_y =
66 : 38 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
67 : 38 : args = {f_x, f_y};
68 : 38 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
69 : 38 : args = {p, zero};
70 : : Cvc5Term p_0 =
71 : 38 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
72 : 38 : args = {p, f_y};
73 : : Cvc5Term p_f_y =
74 : 38 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
75 : :
76 : 38 : args = {zero, f_x};
77 : 38 : cvc5_assert_formula(
78 : 38 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
79 : 38 : args = {zero, f_y};
80 : 38 : cvc5_assert_formula(
81 : 38 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
82 : 38 : args = {sum, one};
83 : 38 : cvc5_assert_formula(
84 : 38 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
85 : 38 : cvc5_assert_formula(d_solver, p_0);
86 : 38 : args = {p_f_y};
87 : 38 : cvc5_assert_formula(
88 : 38 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
89 : 38 : Cvc5Result res = cvc5_check_sat(d_solver);
90 [ - + ][ - + ]: 38 : Assert(cvc5_result_is_unsat(res));
[ - - ]
91 : : size_t size;
92 : : const Cvc5Proof* proofs =
93 : 38 : cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size);
94 [ - + ][ - + ]: 38 : Assert(size == 1);
[ - - ]
95 : 76 : return proofs[0];
96 : : }
97 : :
98 : 10 : Cvc5Proof create_rewrite_proof()
99 : : {
100 : 10 : cvc5_set_option(d_solver, "produce-proofs", "true");
101 : 10 : cvc5_set_option(d_solver, "proof-granularity", "dsl-rewrite");
102 : 10 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
103 : 10 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 2);
104 : 10 : std::vector<Cvc5Term> args = {x, zero};
105 : : Cvc5Term geq =
106 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
107 : 10 : args = {zero, x};
108 : : Cvc5Term leq =
109 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data());
110 : 10 : args = {geq, leq};
111 : 10 : cvc5_assert_formula(
112 : : d_solver,
113 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
114 : 10 : Cvc5Result res = cvc5_check_sat(d_solver);
115 [ - + ][ - + ]: 10 : Assert(cvc5_result_is_unsat(res));
[ - - ]
116 : : size_t size;
117 : : const Cvc5Proof* proofs =
118 : 10 : cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size);
119 [ - + ][ - + ]: 10 : Assert(size == 1);
[ - - ]
120 : 20 : return proofs[0];
121 : : }
122 : :
123 : : Cvc5TermManager* d_tm;
124 : : Cvc5* d_solver;
125 : : Cvc5Sort d_bool;
126 : : Cvc5Sort d_int;
127 : : Cvc5Sort d_real;
128 : : Cvc5Sort d_str;
129 : : Cvc5Sort d_uninterpreted;
130 : : };
131 : :
132 : 24 : TEST_F(TestCApiBlackProof, get_rule)
133 : : {
134 : 12 : ASSERT_DEATH(cvc5_proof_get_rule(nullptr), "invalid proof");
135 : 11 : Cvc5Proof proof = create_proof();
136 [ - + ]: 11 : ASSERT_EQ(cvc5_proof_get_rule(proof), CVC5_PROOF_RULE_SCOPE);
137 : : }
138 : :
139 : 22 : TEST_F(TestCApiBlackProof, get_rewrite_rule)
140 : : {
141 : 11 : ASSERT_DEATH(cvc5_proof_get_rewrite_rule(nullptr), "invalid proof");
142 : :
143 : 10 : Cvc5Proof proof = create_rewrite_proof();
144 : 10 : ASSERT_DEATH(cvc5_proof_get_rewrite_rule(proof), "to return `DSL_REWRITE`");
145 : : Cvc5ProofRule rule;
146 : 27 : std::vector<Cvc5Proof> stack = {proof};
147 : 72 : do
148 : : {
149 : 81 : proof = stack.back();
150 : 81 : stack.pop_back();
151 : 81 : rule = cvc5_proof_get_rule(proof);
152 : : size_t size;
153 : 81 : const Cvc5Proof* children = cvc5_proof_get_children(proof, &size);
154 [ + + ]: 180 : for (size_t i = 0; i < size; ++i)
155 : : {
156 : 99 : stack.push_back(children[i]);
157 : : }
158 [ + + ]: 81 : } while (rule != CVC5_PROOF_RULE_DSL_REWRITE);
159 : 9 : (void)cvc5_proof_get_rewrite_rule(proof);
160 : : }
161 : :
162 : 18 : TEST_F(TestCApiBlackProof, get_result)
163 : : {
164 : 9 : ASSERT_DEATH(cvc5_proof_get_result(nullptr), "invalid proof");
165 : 8 : Cvc5Proof proof = create_proof();
166 : 8 : (void)cvc5_proof_get_result(proof);
167 : : }
168 : :
169 : 16 : TEST_F(TestCApiBlackProof, get_children)
170 : : {
171 : 8 : Cvc5Proof proof = create_proof();
172 : : size_t size;
173 : 8 : (void)cvc5_proof_get_children(proof, &size);
174 [ - + ]: 8 : ASSERT_TRUE(size > 0);
175 : 8 : ASSERT_DEATH(cvc5_proof_get_children(nullptr, &size), "invalid proof");
176 : 7 : ASSERT_DEATH(cvc5_proof_get_children(proof, nullptr),
177 : : "unexpected NULL argument");
178 : : }
179 : :
180 : 12 : TEST_F(TestCApiBlackProof, get_arguments)
181 : : {
182 : 6 : Cvc5Proof proof = create_proof();
183 : : size_t size;
184 : 6 : (void)cvc5_proof_get_arguments(proof, &size);
185 : 6 : ASSERT_DEATH(cvc5_proof_get_arguments(nullptr, &size), "invalid proof");
186 : 5 : ASSERT_DEATH(cvc5_proof_get_arguments(proof, nullptr),
187 : : "unexpected NULL argument");
188 : : }
189 : :
190 : 8 : TEST_F(TestCApiBlackProof, is_equal_disequal_hash)
191 : : {
192 : 4 : Cvc5Proof proof = create_proof();
193 : : size_t size;
194 : 4 : Cvc5Proof x = cvc5_proof_get_children(proof, &size)[0];
195 : 4 : Cvc5Proof y = cvc5_proof_get_children(x, &size)[0];
196 : :
197 [ - + ]: 4 : ASSERT_TRUE(cvc5_proof_is_equal(x, x));
198 [ - + ]: 4 : ASSERT_FALSE(cvc5_proof_is_disequal(x, x));
199 [ - + ]: 4 : ASSERT_FALSE(cvc5_proof_is_equal(x, y));
200 [ - + ]: 4 : ASSERT_TRUE(cvc5_proof_is_disequal(x, y));
201 [ - + ]: 4 : ASSERT_TRUE(cvc5_proof_is_equal(nullptr, nullptr));
202 [ - + ]: 4 : ASSERT_FALSE(cvc5_proof_is_equal(x, nullptr));
203 [ - + ]: 4 : ASSERT_FALSE(cvc5_proof_is_equal(nullptr, y));
204 [ - + ]: 4 : ASSERT_TRUE(cvc5_proof_is_disequal(x, nullptr));
205 [ - + ]: 4 : ASSERT_TRUE(cvc5_proof_is_disequal(nullptr, y));
206 : :
207 [ - + ]: 4 : ASSERT_EQ(cvc5_proof_hash(x), cvc5_proof_hash(x));
208 [ - + ]: 4 : ASSERT_NE(cvc5_proof_hash(x), cvc5_proof_hash(y));
209 : 4 : ASSERT_DEATH(cvc5_proof_hash(nullptr), "invalid proof");
210 : : }
211 : :
212 : 6 : TEST_F(TestCApiBlackProof, copy_release)
213 : : {
214 : 3 : ASSERT_DEATH(cvc5_proof_copy(nullptr), "invalid proof");
215 : 2 : ASSERT_DEATH(cvc5_proof_release(nullptr), "invalid proof");
216 : 1 : Cvc5Proof proof = create_proof();
217 [ - + ]: 1 : ASSERT_EQ(cvc5_proof_get_rule(proof), CVC5_PROOF_RULE_SCOPE);
218 : 1 : Cvc5Proof proof2 = cvc5_proof_copy(proof);
219 [ - + ]: 1 : ASSERT_EQ(cvc5_proof_get_rule(proof), CVC5_PROOF_RULE_SCOPE);
220 [ - + ]: 1 : ASSERT_EQ(cvc5_proof_get_rule(proof2), CVC5_PROOF_RULE_SCOPE);
221 [ - + ]: 1 : ASSERT_TRUE(cvc5_proof_is_equal(proof, proof2));
222 : 1 : cvc5_proof_release(proof);
223 [ - + ]: 1 : ASSERT_EQ(cvc5_proof_get_rule(proof), CVC5_PROOF_RULE_SCOPE);
224 [ - + ]: 1 : ASSERT_EQ(cvc5_proof_get_rule(proof2), CVC5_PROOF_RULE_SCOPE);
225 : 1 : cvc5_proof_release(proof);
226 : : // we cannot reliably check that querying on the (now freed) proof fails
227 : : // unless ASAN is enabled
228 : : }
229 : : } // namespace cvc5::internal::test
|
