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 the guards of the C++ API functions.
11 : : */
12 : :
13 : : #include <gtest/gtest.h>
14 : :
15 : : #include "test_api.h"
16 : :
17 : : namespace cvc5::internal {
18 : :
19 : : namespace test {
20 : :
21 : : class TestApiBlackProof : public TestApi
22 : : {
23 : : protected:
24 : 5 : Proof createProof()
25 : : {
26 : 5 : d_solver->setOption("produce-proofs", "true");
27 : :
28 : 5 : Sort uSort = d_tm.mkUninterpretedSort("u");
29 : 5 : Sort intSort = d_tm.getIntegerSort();
30 : 5 : Sort boolSort = d_tm.getBooleanSort();
31 : 15 : Sort uToIntSort = d_tm.mkFunctionSort({uSort}, intSort);
32 : 15 : Sort intPredSort = d_tm.mkFunctionSort({intSort}, boolSort);
33 : 5 : std::vector<Proof> proof;
34 : :
35 : 5 : Term x = d_tm.mkConst(uSort, "x");
36 : 5 : Term y = d_tm.mkConst(uSort, "y");
37 : 5 : Term f = d_tm.mkConst(uToIntSort, "f");
38 : 5 : Term p = d_tm.mkConst(intPredSort, "p");
39 : 5 : Term zero = d_tm.mkInteger(0);
40 : 5 : Term one = d_tm.mkInteger(1);
41 : 20 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
42 : 20 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
43 : 20 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
44 : 20 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
45 : 20 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
46 [ + + ][ - - ]: 15 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x}));
47 [ + + ][ - - ]: 15 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y}));
48 [ + + ][ - - ]: 15 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one}));
49 : 5 : d_solver->assertFormula(p_0);
50 : 5 : d_solver->assertFormula(p_f_y.notTerm());
51 : 5 : d_solver->checkSat();
52 : :
53 : 10 : return d_solver->getProof().front();
54 : 5 : }
55 : :
56 : 1 : Proof createRewriteProof()
57 : : {
58 : 1 : d_solver->setOption("produce-proofs", "true");
59 : 1 : d_solver->setOption("proof-granularity", "dsl-rewrite");
60 : 1 : Sort intSort = d_tm.getIntegerSort();
61 : 1 : Term x = d_tm.mkConst(intSort, "x");
62 : 1 : Term zero = d_tm.mkInteger(0);
63 : 4 : Term geq = d_tm.mkTerm(Kind::GEQ, {x, zero});
64 : 4 : Term leq = d_tm.mkTerm(Kind::LEQ, {zero, x});
65 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::DISTINCT, {geq, leq}));
66 : 1 : d_solver->checkSat();
67 : 2 : return d_solver->getProof().front();
68 : 1 : }
69 : : };
70 : :
71 : 4 : TEST_F(TestApiBlackProof, nullProof)
72 : : {
73 : 1 : Proof proof;
74 [ - + ][ + - ]: 1 : ASSERT_EQ(proof.getRule(), ProofRule::UNKNOWN);
75 [ - + ]: 1 : ASSERT_EQ(std::hash<cvc5::ProofRule>()(ProofRule::UNKNOWN),
76 [ + - ]: 1 : static_cast<size_t>(ProofRule::UNKNOWN));
77 [ - + ][ + - ]: 1 : ASSERT_TRUE(proof.getResult().isNull());
78 [ - + ][ + - ]: 1 : ASSERT_TRUE(proof.getChildren().empty());
79 [ - + ][ + - ]: 1 : ASSERT_TRUE(proof.getArguments().empty());
80 [ + - ]: 1 : }
81 : :
82 : 4 : TEST_F(TestApiBlackProof, getRule)
83 : : {
84 : 1 : Proof proof = createProof();
85 [ - + ][ + - ]: 1 : ASSERT_EQ(proof.getRule(), ProofRule::SCOPE);
86 [ + - ]: 1 : }
87 : :
88 : 4 : TEST_F(TestApiBlackProof, getRewriteRule)
89 : : {
90 : 1 : Proof proof = createRewriteProof();
91 : 1 : ASSERT_THROW(proof.getRewriteRule(), CVC5ApiException);
92 : : ProofRule rule;
93 : 1 : std::vector<Proof> stack;
94 : 1 : stack.push_back(proof);
95 : : do
96 : : {
97 : 9 : proof = stack.back();
98 : 9 : stack.pop_back();
99 : 9 : rule = proof.getRule();
100 : 9 : std::vector<Proof> children = proof.getChildren();
101 : 9 : stack.insert(stack.cend(), children.cbegin(), children.cend());
102 [ + + ]: 9 : } while (rule != ProofRule::DSL_REWRITE);
103 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getRewriteRule());
[ + - ][ - - ]
104 [ + - ]: 1 : }
105 : :
106 : 4 : TEST_F(TestApiBlackProof, getResult)
107 : : {
108 : 1 : Proof proof = createProof();
109 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getResult());
[ + - ][ - - ]
110 [ + - ]: 1 : }
111 : :
112 : 4 : TEST_F(TestApiBlackProof, getChildren)
113 : : {
114 : 1 : Proof proof = createProof();
115 : 1 : std::vector<Proof> children;
116 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(children = proof.getChildren());
[ + - ][ - - ]
117 [ - + ][ + - ]: 1 : ASSERT_FALSE(children.empty());
118 [ + - ][ + - ]: 1 : }
119 : :
120 : 4 : TEST_F(TestApiBlackProof, getArguments)
121 : : {
122 : 1 : Proof proof = createProof();
123 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getArguments());
[ + - ][ - - ]
124 [ + - ]: 1 : }
125 : :
126 : 4 : TEST_F(TestApiBlackProof, equalhash)
127 : : {
128 : 1 : Proof x = createProof();
129 : 1 : Proof y = x.getChildren()[0];
130 : 1 : Proof z;
131 : :
132 [ - + ][ + - ]: 1 : ASSERT_TRUE(x == x);
133 [ - + ][ + - ]: 1 : ASSERT_FALSE(x != x);
134 [ - + ][ + - ]: 1 : ASSERT_FALSE(x == y);
135 [ - + ][ + - ]: 1 : ASSERT_TRUE(x != y);
136 [ - + ][ + - ]: 1 : ASSERT_FALSE(x == z);
137 [ - + ][ + - ]: 1 : ASSERT_TRUE(x != z);
138 : :
139 [ - + ][ + - ]: 1 : ASSERT_TRUE(std::hash<Proof>()(x) == std::hash<Proof>()(x));
140 : 1 : (void)std::hash<Proof>{}(Proof());
141 [ - + ][ + - ]: 1 : ASSERT_FALSE(std::hash<Proof>()(x) == std::hash<Proof>()(y));
142 [ + - ][ + - ]: 1 : }
[ + - ]
143 : :
144 : : } // namespace test
145 : : } // namespace cvc5::internal
|
