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 "test_api.h"
14 : :
15 : : namespace cvc5::internal {
16 : :
17 : : namespace test {
18 : :
19 : : class TestApiBlackGrammar : public TestApi
20 : : {
21 : : protected:
22 : 6 : void SetUp() override
23 : : {
24 : 6 : TestApi::SetUp();
25 : 6 : d_bool = d_tm.getBooleanSort();
26 : 6 : }
27 : : Sort d_bool;
28 : : };
29 : :
30 : 4 : TEST_F(TestApiBlackGrammar, toString)
31 : : {
32 : 1 : d_solver->setOption("sygus", "true");
33 : 1 : Term start = d_tm.mkVar(d_bool);
34 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
35 [ - + ][ + - ]: 2 : ASSERT_EQ(g.toString(), "");
36 : 1 : g.addRule(start, d_tm.mkBoolean(false));
37 [ - + ][ + - ]: 2 : ASSERT_NE(g.toString(), "");
38 : : {
39 : 1 : std::stringstream ss;
40 : 1 : ss << g;
41 [ - + ][ + - ]: 2 : ASSERT_EQ(ss.str(), g.toString());
42 [ + - ]: 1 : }
43 [ + - ][ + - ]: 1 : }
44 : :
45 : 4 : TEST_F(TestApiBlackGrammar, addRule)
46 : : {
47 : 1 : d_solver->setOption("sygus", "true");
48 : :
49 : 1 : Term nullTerm;
50 : 1 : Term start = d_tm.mkVar(d_bool);
51 : 1 : Term nts = d_tm.mkVar(d_bool);
52 : :
53 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
54 : :
55 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g.addRule(start, d_tm.mkBoolean(false)));
[ + - ][ - - ]
56 : :
57 : 2 : ASSERT_THROW(g.addRule(nullTerm, d_tm.mkBoolean(false)), CVC5ApiException);
58 : 1 : ASSERT_THROW(g.addRule(start, nullTerm), CVC5ApiException);
59 : 2 : ASSERT_THROW(g.addRule(nts, d_tm.mkBoolean(false)), CVC5ApiException);
60 : 2 : ASSERT_THROW(g.addRule(start, d_tm.mkInteger(0)), CVC5ApiException);
61 : :
62 : 1 : d_solver->synthFun("f", {}, d_bool, g);
63 : :
64 : 2 : ASSERT_THROW(g.addRule(start, d_tm.mkBoolean(false)), CVC5ApiException);
65 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
66 : :
67 : 4 : TEST_F(TestApiBlackGrammar, addRules)
68 : : {
69 : 1 : d_solver->setOption("sygus", "true");
70 : :
71 : 1 : Term nullTerm;
72 : 1 : Term start = d_tm.mkVar(d_bool);
73 : 1 : Term nts = d_tm.mkVar(d_bool);
74 : :
75 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
76 : :
77 : 2 : ASSERT_NO_THROW(g.addRules(start, {d_tm.mkBoolean(false)}));
78 : :
79 : 5 : ASSERT_THROW(g.addRules(nullTerm, {d_tm.mkBoolean(false)}), CVC5ApiException);
80 : 5 : ASSERT_THROW(g.addRules(start, {nullTerm}), CVC5ApiException);
81 : 5 : ASSERT_THROW(g.addRules(nts, {d_tm.mkBoolean(false)}), CVC5ApiException);
82 : 5 : ASSERT_THROW(g.addRules(start, {d_tm.mkInteger(0)}), CVC5ApiException);
83 : :
84 : 1 : d_solver->synthFun("f", {}, d_bool, g);
85 : :
86 : 5 : ASSERT_THROW(g.addRules(start, {d_tm.mkBoolean(false)}), CVC5ApiException);
87 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
88 : :
89 : 4 : TEST_F(TestApiBlackGrammar, addAnyConstant)
90 : : {
91 : 1 : d_solver->setOption("sygus", "true");
92 : :
93 : 1 : Term nullTerm;
94 : 1 : Term start = d_tm.mkVar(d_bool);
95 : 1 : Term nts = d_tm.mkVar(d_bool);
96 : :
97 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
98 : :
99 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g.addAnyConstant(start));
[ + - ][ - - ]
100 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g.addAnyConstant(start));
[ + - ][ - - ]
101 : :
102 : 1 : ASSERT_THROW(g.addAnyConstant(nullTerm), CVC5ApiException);
103 : 1 : ASSERT_THROW(g.addAnyConstant(nts), CVC5ApiException);
104 : :
105 : 1 : d_solver->synthFun("f", {}, d_bool, g);
106 : :
107 : 1 : ASSERT_THROW(g.addAnyConstant(start), CVC5ApiException);
108 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
109 : :
110 : 4 : TEST_F(TestApiBlackGrammar, addAnyVariable)
111 : : {
112 : 1 : d_solver->setOption("sygus", "true");
113 : :
114 : 1 : Term nullTerm;
115 : 1 : Term x = d_tm.mkVar(d_bool);
116 : 1 : Term start = d_tm.mkVar(d_bool);
117 : 1 : Term nts = d_tm.mkVar(d_bool);
118 : :
119 : 5 : Grammar g1 = d_solver->mkGrammar({x}, {start});
120 : 3 : Grammar g2 = d_solver->mkGrammar({}, {start});
121 : :
122 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g1.addAnyVariable(start));
[ + - ][ - - ]
123 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g1.addAnyVariable(start));
[ + - ][ - - ]
124 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g2.addAnyVariable(start));
[ + - ][ - - ]
125 : :
126 : 1 : ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC5ApiException);
127 : 1 : ASSERT_THROW(g1.addAnyVariable(nts), CVC5ApiException);
128 : :
129 : 1 : d_solver->synthFun("f", {}, d_bool, g1);
130 : :
131 : 1 : ASSERT_THROW(g1.addAnyVariable(start), CVC5ApiException);
132 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
133 : :
134 : 4 : TEST_F(TestApiBlackGrammar, equalHash)
135 : : {
136 : 1 : d_solver->setOption("sygus", "true");
137 : :
138 : 1 : Term x = d_tm.mkVar(d_bool, "x");
139 : 1 : Term start1 = d_tm.mkVar(d_bool, "start");
140 : 1 : Term start2 = d_tm.mkVar(d_bool, "start");
141 : 1 : Grammar g1, g2;
142 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g2);
143 : :
144 : : {
145 : 2 : g1 = d_solver->mkGrammar({}, {start1});
146 : 2 : g2 = d_solver->mkGrammar({}, {start1});
147 [ - + ][ + - ]: 1 : ASSERT_EQ(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g1));
148 [ - + ][ + - ]: 1 : ASSERT_EQ(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
149 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
150 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
151 : : }
152 : :
153 : : {
154 : 2 : g1 = d_solver->mkGrammar({}, {start1});
155 : 3 : g2 = d_solver->mkGrammar({x}, {start1});
156 [ - + ][ + - ]: 1 : ASSERT_NE(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
157 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
158 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
159 : : }
160 : :
161 : : {
162 : 3 : g1 = d_solver->mkGrammar({x}, {start1});
163 : 3 : g2 = d_solver->mkGrammar({x}, {start2});
164 [ - + ][ + - ]: 1 : ASSERT_NE(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
165 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
166 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
167 : : }
168 : :
169 : : {
170 : 3 : g1 = d_solver->mkGrammar({x}, {start1});
171 : 3 : g2 = d_solver->mkGrammar({x}, {start1});
172 : 1 : g2.addAnyVariable(start1);
173 [ - + ][ + - ]: 1 : ASSERT_NE(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
174 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
175 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
176 : : }
177 : :
178 : : {
179 : 3 : g1 = d_solver->mkGrammar({x}, {start1});
180 : 3 : g2 = d_solver->mkGrammar({x}, {start1});
181 : 3 : std::vector<Term> rules = {d_tm.mkFalse()};
182 : 1 : g1.addRules(start1, rules);
183 : 1 : g2.addRules(start1, rules);
184 [ - + ][ + - ]: 1 : ASSERT_EQ(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
185 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
186 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
187 [ + - ]: 1 : }
188 : :
189 : : {
190 : 3 : g1 = d_solver->mkGrammar({x}, {start1});
191 : 3 : g2 = d_solver->mkGrammar({x}, {start1});
192 : 3 : std::vector<Term> rules2 = {d_tm.mkFalse()};
193 : 1 : g2.addRules(start1, rules2);
194 [ - + ][ + - ]: 1 : ASSERT_NE(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
195 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
196 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
197 [ + - ]: 1 : }
198 : :
199 : : {
200 : 3 : g1 = d_solver->mkGrammar({x}, {start1});
201 : 3 : g2 = d_solver->mkGrammar({x}, {start1});
202 : 3 : std::vector<Term> rules1 = {d_tm.mkTrue()};
203 : 3 : std::vector<Term> rules2 = {d_tm.mkFalse()};
204 : 1 : g1.addRules(start1, rules1);
205 : 1 : g2.addRules(start1, rules2);
206 [ - + ][ + - ]: 1 : ASSERT_NE(std::hash<Grammar>{}(g1), std::hash<Grammar>{}(g2));
207 [ - + ][ + - ]: 1 : ASSERT_EQ(g1, g1);
208 [ - + ][ + - ]: 1 : ASSERT_NE(g1, g2);
209 [ + - ][ + - ]: 1 : }
210 : 1 : (void)std::hash<Grammar>{}(Grammar());
211 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
212 : : } // namespace test
213 : : } // namespace cvc5::internal
|
