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