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