Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Hans-Joerg Schurr, Aina Niemetz, Mudathir Mohamed
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : 5 : Term twoX = d_tm.mkTerm(Kind::MULT, {d_tm.mkInteger(2), x});
66 : 4 : Term xPlusX = d_tm.mkTerm(Kind::ADD, {x, x});
67 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::DISTINCT, {twoX, xPlusX}));
68 : 1 : d_solver->checkSat();
69 : 2 : return d_solver->getProof().front();
70 : : }
71 : : };
72 : :
73 : 2 : TEST_F(TestApiBlackProof, nullProof)
74 : : {
75 : 1 : Proof proof;
76 [ - + ]: 1 : ASSERT_EQ(proof.getRule(), ProofRule::UNKNOWN);
77 [ - + ]: 1 : ASSERT_EQ(std::hash<cvc5::ProofRule>()(ProofRule::UNKNOWN),
78 : : static_cast<size_t>(ProofRule::UNKNOWN));
79 [ - + ]: 1 : ASSERT_TRUE(proof.getResult().isNull());
80 [ - + ]: 1 : ASSERT_TRUE(proof.getChildren().empty());
81 [ - + ]: 1 : ASSERT_TRUE(proof.getArguments().empty());
82 : : }
83 : :
84 : 2 : TEST_F(TestApiBlackProof, getRule)
85 : : {
86 : 1 : Proof proof = createProof();
87 [ - + ]: 1 : ASSERT_EQ(proof.getRule(), ProofRule::SCOPE);
88 : : }
89 : :
90 : 2 : TEST_F(TestApiBlackProof, getRewriteRule)
91 : : {
92 : 1 : Proof proof = createRewriteProof();
93 [ + - ][ + - ]: 2 : ASSERT_THROW(proof.getRewriteRule(), CVC5ApiException);
[ - + ]
94 : : ProofRule rule;
95 : 1 : std::vector<Proof> stack;
96 : 1 : stack.push_back(proof);
97 : 8 : do
98 : : {
99 : 9 : proof = stack.back();
100 : 9 : stack.pop_back();
101 : 9 : rule = proof.getRule();
102 : 18 : std::vector<Proof> children = proof.getChildren();
103 : 9 : stack.insert(stack.cend(), children.cbegin(), children.cend());
104 [ + + ]: 9 : } while (rule != ProofRule::DSL_REWRITE);
105 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getRewriteRule());
106 : : }
107 : :
108 : 2 : TEST_F(TestApiBlackProof, getResult)
109 : : {
110 : 1 : Proof proof = createProof();
111 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getResult());
112 : : }
113 : :
114 : 2 : TEST_F(TestApiBlackProof, getChildren)
115 : : {
116 : 1 : Proof proof = createProof();
117 : 1 : std::vector<Proof> children;
118 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(children = proof.getChildren());
119 [ - + ]: 1 : ASSERT_FALSE(children.empty());
120 : : }
121 : :
122 : 2 : TEST_F(TestApiBlackProof, getArguments)
123 : : {
124 : 1 : Proof proof = createProof();
125 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getArguments());
126 : : }
127 : :
128 : 2 : TEST_F(TestApiBlackProof, equalhash)
129 : : {
130 : 1 : Proof x = createProof();
131 : 1 : Proof y = x.getChildren()[0];
132 : 1 : Proof z;
133 : :
134 [ - + ]: 1 : ASSERT_TRUE(x == x);
135 [ - + ]: 1 : ASSERT_FALSE(x != x);
136 [ - + ]: 1 : ASSERT_FALSE(x == y);
137 [ - + ]: 1 : ASSERT_TRUE(x != y);
138 [ - + ]: 1 : ASSERT_FALSE(x == z);
139 [ - + ]: 1 : ASSERT_TRUE(x != z);
140 : :
141 [ - + ]: 1 : ASSERT_TRUE(std::hash<Proof>()(x) == std::hash<Proof>()(x));
142 : 1 : (void)std::hash<Proof>{}(Proof());
143 [ - + ]: 1 : ASSERT_FALSE(std::hash<Proof>()(x) == std::hash<Proof>()(y));
144 : : }
145 : :
146 : : } // namespace test
147 : : } // namespace cvc5::internal
|
