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 Solver class of the C++ API.
11 : : */
12 : :
13 : : #include <cvc5/cvc5_types.h>
14 : : #include <gtest/gtest.h>
15 : :
16 : : #include <algorithm>
17 : : #include <cmath>
18 : :
19 : : #include "base/output.h"
20 : : #include "test_api.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : : namespace test {
25 : :
26 : : class TestApiBlackSolver : public TestApi
27 : : {
28 : : };
29 : :
30 : 4 : TEST_F(TestApiBlackSolver, pow2Large1)
31 : : {
32 : : // Based on https://github.com/cvc5/cvc5-projects/issues/371
33 : 1 : Sort s4 = d_tm.mkArraySort(d_string, d_int);
34 : 1 : Sort s7 = d_tm.mkArraySort(d_int, d_string);
35 : 2 : Term t10 = d_tm.mkInteger("68038927088685865242724985643");
36 : 2 : Term t74 = d_tm.mkInteger("8416288636405");
37 : 1 : std::vector<DatatypeConstructorDecl> ctors;
38 : 1 : ctors.push_back(d_tm.mkDatatypeConstructorDecl("_x109"));
39 : 1 : ctors.back().addSelector("_x108", s7);
40 : 1 : ctors.push_back(d_tm.mkDatatypeConstructorDecl("_x113"));
41 : 1 : ctors.back().addSelector("_x110", s4);
42 : 1 : ctors.back().addSelector("_x111", d_int);
43 : 1 : ctors.back().addSelector("_x112", s7);
44 : 2 : Sort s11 = d_solver->declareDatatype("_x107", ctors);
45 : 1 : Term t82 = d_tm.mkConst(s11, "_x114");
46 : 3 : Term t180 = d_tm.mkTerm(Kind::POW2, {t10});
47 : 4 : Term t258 = d_tm.mkTerm(Kind::GEQ, {t74, t180});
48 : 1 : d_solver->assertFormula(t258);
49 : 1 : ASSERT_THROW(d_solver->simplify(t82, true), CVC5ApiException);
50 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
51 : :
52 : 4 : TEST_F(TestApiBlackSolver, pow2Large2)
53 : : {
54 : : // Based on https://github.com/cvc5/cvc5-projects/issues/333
55 : 1 : Term t1 = d_tm.mkBitVector(63, ~(((uint64_t)1) << 62));
56 : 3 : Term t2 = d_tm.mkTerm(Kind::BITVECTOR_UBV_TO_INT, {t1});
57 : 3 : Term t3 = d_tm.mkTerm(Kind::POW2, {t2});
58 : 4 : Term t4 = d_tm.mkTerm(Kind::DISTINCT, {t3, t2});
59 : 1 : ASSERT_THROW(d_solver->checkSatAssuming({t4}), CVC5ApiException);
60 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
61 : :
62 : 4 : TEST_F(TestApiBlackSolver, pow2Large3)
63 : : {
64 : : // Based on https://github.com/cvc5/cvc5-projects/issues/339
65 : 2 : Term t203 = d_tm.mkInteger("6135470354240554220207");
66 : 3 : Term t262 = d_tm.mkTerm(Kind::POW2, {t203});
67 : 3 : Term t536 = d_tm.mkTerm(d_tm.mkOp(Kind::INT_TO_BITVECTOR, {49}), {t262});
68 : : // should not throw an exception, will not simplify.
69 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(t536));
[ + - ][ - - ]
70 [ + - ][ + - ]: 1 : }
[ + - ]
71 : :
72 : 4 : TEST_F(TestApiBlackSolver, recoverableException)
73 : : {
74 : 1 : d_solver->setOption("produce-models", "true");
75 : 1 : Term x = d_tm.mkConst(d_bool, "x");
76 : 1 : d_solver->assertFormula(x.eqTerm(x).notTerm());
77 : 1 : ASSERT_THROW(d_solver->getValue(x), CVC5ApiRecoverableException);
78 : :
79 : : try
80 : : {
81 : 1 : d_solver->getValue(x);
82 : : }
83 [ - + ]: 1 : catch (const CVC5ApiRecoverableException& e)
84 : : {
85 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(e.what());
[ + - ][ - - ]
86 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(e.getMessage());
[ + - ][ - - ]
87 [ + - ]: 1 : }
88 [ + - ]: 1 : }
89 : :
90 : 4 : TEST_F(TestApiBlackSolver, simplify)
91 : : {
92 : 2 : ASSERT_THROW(d_solver->simplify(Term()), CVC5ApiException);
93 : :
94 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
95 : 4 : Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort);
96 : 3 : Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
97 : 2 : DatatypeDecl consListSpec = d_tm.mkDatatypeDecl("list");
98 : 2 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
99 : 1 : cons.addSelector("head", d_int);
100 : 1 : cons.addSelectorSelf("tail");
101 : 1 : consListSpec.addConstructor(cons);
102 : 2 : DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
103 : 1 : consListSpec.addConstructor(nil);
104 : 1 : Sort consListSort = d_tm.mkDatatypeSort(consListSpec);
105 : :
106 : 1 : Term x = d_tm.mkConst(bvSort, "x");
107 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(x));
[ + - ][ - - ]
108 : 1 : Term a = d_tm.mkConst(bvSort, "a");
109 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(a));
[ + - ][ - - ]
110 : 1 : Term b = d_tm.mkConst(bvSort, "b");
111 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(b));
[ + - ][ - - ]
112 : 4 : Term x_eq_x = d_tm.mkTerm(Kind::EQUAL, {x, x});
113 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(x_eq_x));
[ + - ][ - - ]
114 [ - + ][ + - ]: 2 : ASSERT_NE(d_tm.mkTrue(), x_eq_x);
115 [ - + ][ + - ]: 2 : ASSERT_EQ(d_tm.mkTrue(), d_solver->simplify(x_eq_x));
116 : 4 : Term x_eq_b = d_tm.mkTerm(Kind::EQUAL, {x, b});
117 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(x_eq_b));
[ + - ][ - - ]
118 [ - + ][ + - ]: 2 : ASSERT_NE(d_tm.mkTrue(), x_eq_b);
119 [ - + ][ + - ]: 2 : ASSERT_NE(d_tm.mkTrue(), d_solver->simplify(x_eq_b));
120 : :
121 : 1 : Term i1 = d_tm.mkConst(d_int, "i1");
122 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(i1));
[ + - ][ - - ]
123 : 5 : Term i2 = d_tm.mkTerm(Kind::MULT, {i1, d_tm.mkInteger("23")});
124 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(i2));
[ + - ][ - - ]
125 [ - + ][ + - ]: 1 : ASSERT_NE(i1, i2);
126 [ - + ][ + - ]: 2 : ASSERT_NE(i1, d_solver->simplify(i2));
127 : 4 : Term i3 = d_tm.mkTerm(Kind::ADD, {i1, d_tm.mkInteger(0)});
128 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(i3));
[ + - ][ - - ]
129 [ - + ][ + - ]: 1 : ASSERT_NE(i1, i3);
130 [ - + ][ + - ]: 2 : ASSERT_EQ(i1, d_solver->simplify(i3));
131 : :
132 : 1 : Datatype consList = consListSort.getDatatype();
133 : : Term dt1 =
134 : 3 : d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
135 : 2 : {consList.getConstructor("cons").getTerm(),
136 : : d_tm.mkInteger(0),
137 : 1 : d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
138 : 5 : {consList.getConstructor("nil").getTerm()})});
139 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(dt1));
[ + - ][ - - ]
140 : 2 : Term dt2 = d_tm.mkTerm(Kind::APPLY_SELECTOR,
141 : 3 : {consList["cons"].getSelector("head").getTerm(), dt1});
142 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(dt2));
[ + - ][ - - ]
143 : :
144 : 1 : Term b1 = d_tm.mkVar(bvSort, "b1");
145 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(b1));
[ + - ][ - - ]
146 : 1 : Term b2 = d_tm.mkVar(bvSort, "b1");
147 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(b2));
[ + - ][ - - ]
148 : 1 : Term b3 = d_tm.mkVar(d_uninterpreted, "b3");
149 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(b3));
[ + - ][ - - ]
150 : 1 : Term v1 = d_tm.mkConst(bvSort, "v1");
151 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(v1));
[ + - ][ - - ]
152 : 1 : Term v2 = d_tm.mkConst(d_int, "v2");
153 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(v2));
[ + - ][ - - ]
154 : 1 : Term f1 = d_tm.mkConst(funSort1, "f1");
155 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(f1));
[ + - ][ - - ]
156 : 1 : Term f2 = d_tm.mkConst(funSort2, "f2");
157 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(f2));
[ + - ][ - - ]
158 : 10 : d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
159 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(f1));
[ + - ][ - - ]
160 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->simplify(f2));
[ + - ][ - - ]
161 : :
162 : 1 : TermManager tm;
163 : 1 : Solver slv(tm);
164 : 1 : ASSERT_THROW(slv.simplify(x), CVC5ApiException);
165 : : }
166 : :
167 : 4 : TEST_F(TestApiBlackSolver, simplifyApplySubs)
168 : : {
169 : 1 : d_solver->setOption("incremental", "true");
170 : 1 : Term x = d_tm.mkConst(d_int, "x");
171 : 1 : Term zero = d_tm.mkInteger(0);
172 : 4 : Term eq = d_tm.mkTerm(Kind::EQUAL, {x, zero});
173 : 1 : d_solver->assertFormula(eq);
174 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSat());
[ + - ][ - - ]
175 : :
176 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->simplify(x, false), x);
177 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->simplify(x, true), zero);
178 [ + - ][ + - ]: 1 : }
[ + - ]
179 : :
180 : 4 : TEST_F(TestApiBlackSolver, assertFormula)
181 : : {
182 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->assertFormula(d_tm.mkTrue()));
[ + - ][ - - ]
183 : 2 : ASSERT_THROW(d_solver->assertFormula(Term()), CVC5ApiException);
184 : 1 : TermManager tm;
185 : 1 : Solver slv(tm);
186 : 2 : ASSERT_THROW(slv.assertFormula(d_tm.mkTrue()), CVC5ApiException);
187 : : }
188 : :
189 : 4 : TEST_F(TestApiBlackSolver, checkSat)
190 : : {
191 : 1 : d_solver->setOption("incremental", "false");
192 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSat());
[ + - ][ - - ]
193 : 1 : ASSERT_THROW(d_solver->checkSat(), CVC5ApiException);
194 : : }
195 : :
196 : 4 : TEST_F(TestApiBlackSolver, checkSatAssuming)
197 : : {
198 : 1 : d_solver->setOption("incremental", "false");
199 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()));
[ + - ][ - - ]
200 : 2 : ASSERT_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()), CVC5ApiException);
201 : 1 : TermManager tm;
202 : 1 : Solver slv(tm);
203 : 2 : ASSERT_THROW(slv.checkSatAssuming(d_tm.mkTrue()), CVC5ApiException);
204 : : }
205 : :
206 : 4 : TEST_F(TestApiBlackSolver, checkSatAssuming1)
207 : : {
208 : 1 : Term x = d_tm.mkConst(d_bool, "x");
209 : 1 : Term y = d_tm.mkConst(d_bool, "y");
210 : 4 : Term z = d_tm.mkTerm(Kind::AND, {x, y});
211 : 1 : d_solver->setOption("incremental", "true");
212 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()));
[ + - ][ - - ]
213 : 2 : ASSERT_THROW(d_solver->checkSatAssuming(Term()), CVC5ApiException);
214 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()));
[ + - ][ - - ]
215 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSatAssuming(z));
[ + - ][ - - ]
216 [ + - ][ + - ]: 1 : }
[ + - ]
217 : :
218 : 4 : TEST_F(TestApiBlackSolver, checkSatAssuming2)
219 : : {
220 : 1 : d_solver->setOption("incremental", "true");
221 : :
222 : 3 : Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
223 : 3 : Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool);
224 : :
225 : 1 : Term n = Term();
226 : : // Constants
227 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
228 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
229 : : // Functions
230 : 1 : Term f = d_tm.mkConst(uToIntSort, "f");
231 : 1 : Term p = d_tm.mkConst(intPredSort, "p");
232 : : // Values
233 : 1 : Term zero = d_tm.mkInteger(0);
234 : 1 : Term one = d_tm.mkInteger(1);
235 : : // Terms
236 : 4 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
237 : 4 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
238 : 4 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
239 : 4 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
240 : 4 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
241 : : // Assertions
242 : : Term assertions =
243 : 5 : d_tm.mkTerm(Kind::AND,
244 : : {
245 : 2 : d_tm.mkTerm(Kind::LEQ, {zero, f_x}), // 0 <= f(x)
246 : 2 : d_tm.mkTerm(Kind::LEQ, {zero, f_y}), // 0 <= f(y)
247 : 2 : d_tm.mkTerm(Kind::LEQ, {sum, one}), // f(x) + f(y) <= 1
248 : : p_0.notTerm(), // not p(0)
249 : : p_f_y // p(f(y))
250 : 5 : });
251 : :
252 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()));
[ + - ][ - - ]
253 : 1 : d_solver->assertFormula(assertions);
254 : 3 : ASSERT_NO_THROW(
255 [ + - ]: 1 : d_solver->checkSatAssuming(d_tm.mkTerm(Kind::DISTINCT, {x, y})));
256 : 5 : ASSERT_NO_THROW(d_solver->checkSatAssuming(
257 [ + - ]: 1 : {d_tm.mkFalse(), d_tm.mkTerm(Kind::DISTINCT, {x, y})}));
258 : 1 : ASSERT_THROW(d_solver->checkSatAssuming(n), CVC5ApiException);
259 : 11 : ASSERT_THROW(
260 : : d_solver->checkSatAssuming({n, d_tm.mkTerm(Kind::DISTINCT, {x, y})}),
261 [ + - ]: 1 : CVC5ApiException);
262 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
263 : :
264 : 4 : TEST_F(TestApiBlackSolver, declareFunFresh)
265 : : {
266 : 2 : Term t1 = d_solver->declareFun(std::string("b"), {}, d_bool, true);
267 : 2 : Term t2 = d_solver->declareFun(std::string("b"), {}, d_bool, false);
268 : 2 : Term t3 = d_solver->declareFun(std::string("b"), {}, d_bool, false);
269 [ - + ][ + - ]: 1 : ASSERT_FALSE(t1 == t2);
270 [ - + ][ + - ]: 1 : ASSERT_FALSE(t1 == t3);
271 [ - + ][ + - ]: 1 : ASSERT_TRUE(t2 == t3);
272 : 2 : Term t4 = d_solver->declareFun(std::string("c"), {}, d_bool, false);
273 [ - + ][ + - ]: 1 : ASSERT_FALSE(t2 == t4);
274 : 2 : Term t5 = d_solver->declareFun(std::string("b"), {}, d_int, false);
275 [ - + ][ + - ]: 1 : ASSERT_FALSE(t2 == t5);
276 : :
277 : 1 : TermManager tm;
278 : 1 : Solver slv(tm);
279 : 4 : ASSERT_THROW(slv.declareFun(std::string("b"), {}, d_int, false),
280 [ + - ]: 1 : CVC5ApiException);
281 [ + - ][ + - ]: 1 : }
[ + - ]
282 : :
283 : 4 : TEST_F(TestApiBlackSolver, declareDatatype)
284 : : {
285 : 2 : DatatypeConstructorDecl lin = d_tm.mkDatatypeConstructorDecl("lin");
286 : 3 : std::vector<DatatypeConstructorDecl> ctors0 = {lin};
287 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareDatatype(std::string(""), ctors0));
[ + - ][ - - ]
288 : :
289 : 2 : DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
290 : 3 : std::vector<DatatypeConstructorDecl> ctors1 = {nil};
291 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareDatatype(std::string("a"), ctors1));
[ + - ][ - - ]
292 : :
293 : 2 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
294 : 2 : DatatypeConstructorDecl nil2 = d_tm.mkDatatypeConstructorDecl("nil");
295 : 4 : std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
296 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareDatatype(std::string("b"), ctors2));
[ + - ][ - - ]
297 : :
298 : 2 : DatatypeConstructorDecl cons2 = d_tm.mkDatatypeConstructorDecl("cons");
299 : 2 : DatatypeConstructorDecl nil3 = d_tm.mkDatatypeConstructorDecl("nil");
300 : 4 : std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
301 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareDatatype(std::string(""), ctors3));
[ + - ][ - - ]
302 : :
303 : : // must have at least one constructor
304 : 1 : std::vector<DatatypeConstructorDecl> ctors4;
305 : 3 : ASSERT_THROW(d_solver->declareDatatype(std::string("c"), ctors4),
306 [ + - ]: 1 : CVC5ApiException);
307 : : // constructors may not be reused
308 : 2 : DatatypeConstructorDecl ctor1 = d_tm.mkDatatypeConstructorDecl("_x21");
309 : 2 : DatatypeConstructorDecl ctor2 = d_tm.mkDatatypeConstructorDecl("_x31");
310 [ + + ][ - - ]: 3 : d_solver->declareDatatype(std::string("_x17"), {ctor1, ctor2});
311 : 8 : ASSERT_THROW(d_solver->declareDatatype(std::string("_x86"), {ctor1, ctor2}),
312 [ + - ]: 1 : CVC5ApiException);
313 : :
314 : 1 : TermManager tm;
315 : 1 : Solver slv(tm);
316 : 2 : DatatypeConstructorDecl nnil = d_tm.mkDatatypeConstructorDecl("nil");
317 : 7 : ASSERT_THROW(slv.declareDatatype(std::string("a"), {nnil}), CVC5ApiException);
318 [ + - ][ + - ]: 1 : }
319 : :
320 : 4 : TEST_F(TestApiBlackSolver, declareFun)
321 : : {
322 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
323 : 3 : Sort funSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
324 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareFun("f1", {}, bvSort));
[ + - ][ - - ]
325 : 3 : ASSERT_NO_THROW(d_solver->declareFun("f3", {bvSort, d_int}, bvSort));
326 : 4 : ASSERT_THROW(d_solver->declareFun("f2", {}, funSort), CVC5ApiException);
327 : : // functions as arguments is allowed
328 : 3 : ASSERT_NO_THROW(d_solver->declareFun("f4", {bvSort, funSort}, bvSort));
329 : 8 : ASSERT_THROW(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
330 [ + - ]: 1 : CVC5ApiException);
331 : :
332 : 1 : TermManager tm;
333 : 1 : Solver slv(tm);
334 : 4 : ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC5ApiException);
335 [ + - ][ + - ]: 1 : }
336 : :
337 : 4 : TEST_F(TestApiBlackSolver, declareSort)
338 : : {
339 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSort("s", 0));
[ + - ][ - - ]
340 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSort("s", 2));
[ + - ][ - - ]
341 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSort("", 2));
[ + - ][ - - ]
342 : : }
343 : :
344 : 4 : TEST_F(TestApiBlackSolver, declareSortFresh)
345 : : {
346 : 2 : Sort t1 = d_solver->declareSort(std::string("b"), 0, true);
347 : 2 : Sort t2 = d_solver->declareSort(std::string("b"), 0, false);
348 : 2 : Sort t3 = d_solver->declareSort(std::string("b"), 0, false);
349 [ - + ][ + - ]: 1 : ASSERT_FALSE(t1 == t2);
350 [ - + ][ + - ]: 1 : ASSERT_FALSE(t1 == t3);
351 [ - + ][ + - ]: 1 : ASSERT_TRUE(t2 == t3);
352 : 2 : Sort t4 = d_solver->declareSort(std::string("c"), 0, false);
353 [ - + ][ + - ]: 1 : ASSERT_FALSE(t2 == t4);
354 : 2 : Sort t5 = d_solver->declareSort(std::string("b"), 1, false);
355 [ - + ][ + - ]: 1 : ASSERT_FALSE(t2 == t5);
356 [ + - ][ + - ]: 1 : }
[ + - ]
357 : :
358 : 4 : TEST_F(TestApiBlackSolver, defineFun)
359 : : {
360 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
361 : 3 : Sort funSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
362 : 1 : Term b1 = d_tm.mkVar(bvSort, "b1");
363 : 1 : Term b2 = d_tm.mkVar(d_int, "b2");
364 : 1 : Term b3 = d_tm.mkVar(funSort, "b3");
365 : 1 : Term v1 = d_tm.mkConst(bvSort, "v1");
366 : 1 : Term v2 = d_tm.mkConst(funSort, "v2");
367 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->defineFun("f", {}, bvSort, v1));
[ + - ][ - - ]
368 : 3 : ASSERT_NO_THROW(d_solver->defineFun("ff", {b1, b2}, bvSort, v1));
369 : 8 : ASSERT_THROW(d_solver->defineFun("ff", {v1, b2}, bvSort, v1),
370 [ + - ]: 1 : CVC5ApiException);
371 : 7 : ASSERT_THROW(d_solver->defineFun("fff", {b1}, bvSort, v2), CVC5ApiException);
372 : 7 : ASSERT_THROW(d_solver->defineFun("ffff", {b1}, funSort, v2),
373 [ + - ]: 1 : CVC5ApiException);
374 : : // b3 has function sort, which is allowed as an argument
375 : 3 : ASSERT_NO_THROW(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1));
376 : :
377 : 1 : TermManager tm;
378 : 1 : Solver slv(tm);
379 : 1 : Sort bvSort2 = tm.mkBitVectorSort(32);
380 : 1 : Term v12 = tm.mkConst(bvSort2, "v1");
381 : 1 : Term b12 = tm.mkVar(bvSort2, "b1");
382 : 2 : Term b22 = tm.mkVar(tm.getIntegerSort(), "b2");
383 : 4 : ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC5ApiException);
384 : 4 : ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC5ApiException);
385 : 8 : ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC5ApiException);
386 : 8 : ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC5ApiException);
387 : 8 : ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC5ApiException);
388 : 8 : ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC5ApiException);
389 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
390 : :
391 : 4 : TEST_F(TestApiBlackSolver, defineFunGlobal)
392 : : {
393 : 1 : Term bTrue = d_tm.mkBoolean(true);
394 : : // (define-fun f () Bool true)
395 : 2 : Term f = d_solver->defineFun("f", {}, d_bool, bTrue, true);
396 : 1 : Term b = d_tm.mkVar(d_bool, "b");
397 : : // (define-fun g (b Bool) Bool b)
398 : 3 : Term g = d_solver->defineFun("g", {b}, d_bool, b, true);
399 : :
400 : : // (assert (or (not f) (not (g true))))
401 [ + + ][ - - ]: 4 : d_solver->assertFormula(d_tm.mkTerm(
402 : : Kind::OR,
403 [ + + ][ - - ]: 4 : {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()}));
404 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
405 : 1 : d_solver->resetAssertions();
406 : : // (assert (or (not f) (not (g true))))
407 [ + + ][ - - ]: 4 : d_solver->assertFormula(d_tm.mkTerm(
408 : : Kind::OR,
409 [ + + ][ - - ]: 4 : {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()}));
410 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
411 : :
412 : 1 : TermManager tm;
413 : 1 : Solver slv(tm);
414 : 4 : ASSERT_THROW(slv.defineFun("f", {}, d_bool, bTrue, true), CVC5ApiException);
415 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
416 : :
417 : 4 : TEST_F(TestApiBlackSolver, defineFunRec)
418 : : {
419 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
420 : 4 : Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort);
421 : 3 : Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
422 : 1 : Term b1 = d_tm.mkVar(bvSort, "b1");
423 : 1 : Term b11 = d_tm.mkVar(bvSort, "b1");
424 : 1 : Term b2 = d_tm.mkVar(d_int, "b2");
425 : 1 : Term b3 = d_tm.mkVar(funSort2, "b3");
426 : 1 : Term v1 = d_tm.mkConst(bvSort, "v1");
427 : 1 : Term v2 = d_tm.mkConst(d_int, "v2");
428 : 1 : Term v3 = d_tm.mkConst(funSort2, "v3");
429 : 1 : Term f1 = d_tm.mkConst(funSort1, "f1");
430 : 1 : Term f2 = d_tm.mkConst(funSort2, "f2");
431 : 1 : Term f3 = d_tm.mkConst(bvSort, "f3");
432 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->defineFunRec("f", {}, bvSort, v1));
[ + - ][ - - ]
433 : 3 : ASSERT_NO_THROW(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1));
434 : 3 : ASSERT_NO_THROW(d_solver->defineFunRec(f1, {b1, b11}, v1));
435 : 7 : ASSERT_THROW(d_solver->defineFunRec("fff", {b1}, bvSort, v3),
436 [ + - ]: 1 : CVC5ApiException);
437 : 8 : ASSERT_THROW(d_solver->defineFunRec("ff", {b1, v2}, bvSort, v1),
438 [ + - ]: 1 : CVC5ApiException);
439 : 7 : ASSERT_THROW(d_solver->defineFunRec("ffff", {b1}, funSort2, v3),
440 [ + - ]: 1 : CVC5ApiException);
441 : : // b3 has function sort, which is allowed as an argument
442 : 3 : ASSERT_NO_THROW(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1));
443 : 5 : ASSERT_THROW(d_solver->defineFunRec(f1, {b1}, v1), CVC5ApiException);
444 : 6 : ASSERT_THROW(d_solver->defineFunRec(f1, {b1, b11}, v2), CVC5ApiException);
445 : 6 : ASSERT_THROW(d_solver->defineFunRec(f1, {b1, b11}, v3), CVC5ApiException);
446 : 5 : ASSERT_THROW(d_solver->defineFunRec(f2, {b1}, v2), CVC5ApiException);
447 : 5 : ASSERT_THROW(d_solver->defineFunRec(f3, {b1}, v1), CVC5ApiException);
448 : :
449 : 1 : TermManager tm;
450 : 1 : Solver slv(tm);
451 : 1 : Sort bvSort2 = tm.mkBitVectorSort(32);
452 : 1 : Term v12 = tm.mkConst(bvSort2, "v1");
453 : 1 : Term b12 = tm.mkVar(bvSort2, "b1");
454 : 2 : Term b22 = tm.mkVar(tm.getIntegerSort(), "b2");
455 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12));
[ + - ][ - - ]
456 : 3 : ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
457 : 4 : ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC5ApiException);
458 : 4 : ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC5ApiException);
459 : 8 : ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
460 [ + - ]: 1 : CVC5ApiException);
461 : 8 : ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
462 [ + - ]: 1 : CVC5ApiException);
463 : 8 : ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
464 [ + - ]: 1 : CVC5ApiException);
465 : 8 : ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
466 [ + - ]: 1 : CVC5ApiException);
467 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
468 : :
469 : 4 : TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
470 : : {
471 : 1 : d_solver->setLogic("QF_BV");
472 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
473 : 4 : Sort funSort = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort);
474 : 1 : Term b = d_tm.mkVar(bvSort, "b");
475 : 1 : Term v = d_tm.mkConst(bvSort, "v");
476 : 1 : Term f = d_tm.mkConst(funSort, "f");
477 : 4 : ASSERT_THROW(d_solver->defineFunRec("f", {}, bvSort, v), CVC5ApiException);
478 : 6 : ASSERT_THROW(d_solver->defineFunRec(f, {b, b}, v), CVC5ApiException);
479 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
480 : :
481 : 4 : TEST_F(TestApiBlackSolver, defineFunRecGlobal)
482 : : {
483 : 1 : d_solver->push();
484 : 1 : Term bTrue = d_tm.mkBoolean(true);
485 : : // (define-fun f () Bool true)
486 : 2 : Term f = d_solver->defineFunRec("f", {}, d_bool, bTrue, true);
487 : 1 : Term b = d_tm.mkVar(d_bool, "b");
488 : : // (define-fun g (b Bool) Bool b)
489 : 1 : Term g = d_solver->defineFunRec(
490 : 4 : d_tm.mkConst(d_tm.mkFunctionSort({d_bool}, d_bool), "g"), {b}, b, true);
491 : :
492 : : // (assert (or (not f) (not (g true))))
493 [ + + ][ - - ]: 4 : d_solver->assertFormula(d_tm.mkTerm(
494 : : Kind::OR,
495 [ + + ][ - - ]: 4 : {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()}));
496 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
497 : 1 : d_solver->pop();
498 : : // (assert (or (not f) (not (g true))))
499 [ + + ][ - - ]: 4 : d_solver->assertFormula(d_tm.mkTerm(
500 : : Kind::OR,
501 [ + + ][ - - ]: 4 : {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()}));
502 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
503 : :
504 : 1 : TermManager tm;
505 : 1 : Solver slv(tm);
506 : 2 : Term bb = tm.mkVar(tm.getBooleanSort(), "b");
507 : 12 : ASSERT_THROW(
508 : : slv.defineFunRec(d_tm.mkConst(d_tm.mkFunctionSort({d_bool}, d_bool), "g"),
509 : : {bb},
510 : : bb,
511 : : true),
512 [ + - ]: 1 : CVC5ApiException);
513 : 10 : ASSERT_THROW(
514 : : slv.defineFunRec(
515 : : tm.mkConst(tm.mkFunctionSort({d_bool}, d_bool), "g"), {b}, b, true),
516 [ + - ]: 1 : CVC5ApiException);
517 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
518 : :
519 : 4 : TEST_F(TestApiBlackSolver, defineFunsRec)
520 : : {
521 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
522 : 4 : Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort);
523 : 3 : Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
524 : 1 : Term b1 = d_tm.mkVar(bvSort, "b1");
525 : 1 : Term b11 = d_tm.mkVar(bvSort, "b1");
526 : 1 : Term b2 = d_tm.mkVar(d_int, "b2");
527 : 1 : Term b4 = d_tm.mkVar(d_uninterpreted, "b4");
528 : 1 : Term v1 = d_tm.mkConst(bvSort, "v1");
529 : 1 : Term v2 = d_tm.mkConst(d_int, "v2");
530 : 1 : Term v4 = d_tm.mkConst(d_uninterpreted, "v4");
531 : 1 : Term f1 = d_tm.mkConst(funSort1, "f1");
532 : 1 : Term f2 = d_tm.mkConst(funSort2, "f2");
533 : 1 : Term f3 = d_tm.mkConst(bvSort, "f3");
534 : 10 : ASSERT_NO_THROW(
535 [ + - ]: 1 : d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
536 : 23 : ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
537 [ + - ]: 1 : CVC5ApiException);
538 : 23 : ASSERT_THROW(d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
539 [ + - ]: 1 : CVC5ApiException);
540 : 22 : ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
541 [ + - ]: 1 : CVC5ApiException);
542 : 23 : ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
543 [ + - ]: 1 : CVC5ApiException);
544 : 23 : ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
545 [ + - ]: 1 : CVC5ApiException);
546 : :
547 : 1 : TermManager tm;
548 : 1 : Solver slv(tm);
549 : 1 : Sort uSort2 = tm.mkUninterpretedSort("u");
550 : 1 : Sort bvSort2 = tm.mkBitVectorSort(32);
551 : 4 : Sort funSort12 = tm.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
552 : 4 : Sort funSort22 = tm.mkFunctionSort({uSort2}, tm.getIntegerSort());
553 : 1 : Term b12 = tm.mkVar(bvSort2, "b1");
554 : 1 : Term b112 = tm.mkVar(bvSort2, "b1");
555 : 1 : Term b42 = tm.mkVar(uSort2, "b4");
556 : 1 : Term v12 = tm.mkConst(bvSort2, "v1");
557 : 2 : Term v22 = tm.mkConst(tm.getIntegerSort(), "v2");
558 : 1 : Term f12 = tm.mkConst(funSort12, "f1");
559 : 1 : Term f22 = tm.mkConst(funSort22, "f2");
560 : 10 : ASSERT_NO_THROW(
561 [ + - ]: 1 : slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
562 : 23 : ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
563 [ + - ]: 1 : CVC5ApiException);
564 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
565 [ + - ]: 1 : CVC5ApiException);
566 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
567 [ + - ]: 1 : CVC5ApiException);
568 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
569 [ + - ]: 1 : CVC5ApiException);
570 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
571 [ + - ]: 1 : CVC5ApiException);
572 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
573 [ + - ]: 1 : CVC5ApiException);
574 : 23 : ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
575 [ + - ]: 1 : CVC5ApiException);
576 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
577 : :
578 : 4 : TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
579 : : {
580 : 1 : d_solver->setLogic("QF_BV");
581 : 1 : Sort bvSort = d_tm.mkBitVectorSort(32);
582 : 4 : Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort);
583 : 3 : Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
584 : 1 : Term b = d_tm.mkVar(bvSort, "b");
585 : 1 : Term u = d_tm.mkVar(d_uninterpreted, "u");
586 : 1 : Term v1 = d_tm.mkConst(bvSort, "v1");
587 : 1 : Term v2 = d_tm.mkConst(d_int, "v2");
588 : 1 : Term f1 = d_tm.mkConst(funSort1, "f1");
589 : 1 : Term f2 = d_tm.mkConst(funSort2, "f2");
590 : 23 : ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
591 [ + - ]: 1 : CVC5ApiException);
592 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
593 : :
594 : 4 : TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
595 : : {
596 : 3 : Sort fSort = d_tm.mkFunctionSort({d_bool}, d_bool);
597 : :
598 : 1 : d_solver->push();
599 : 1 : Term bTrue = d_tm.mkBoolean(true);
600 : 1 : Term b = d_tm.mkVar(d_bool, "b");
601 : 1 : Term gSym = d_tm.mkConst(fSort, "g");
602 : : // (define-funs-rec ((g ((b Bool)) Bool)) (b))
603 : 5 : d_solver->defineFunsRec({gSym}, {{b}}, {b}, true);
604 : :
605 : : // (assert (not (g true)))
606 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::APPLY_UF, {gSym, bTrue}).notTerm());
607 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
608 : 1 : d_solver->pop();
609 : : // (assert (not (g true)))
610 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::APPLY_UF, {gSym, bTrue}).notTerm());
611 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
612 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
613 : :
614 : 4 : TEST_F(TestApiBlackSolver, getAssertions)
615 : : {
616 : 1 : Term a = d_tm.mkConst(d_bool, "a");
617 : 1 : Term b = d_tm.mkConst(d_bool, "b");
618 : 1 : d_solver->assertFormula(a);
619 : 1 : d_solver->assertFormula(b);
620 : 4 : std::vector<Term> asserts{a, b};
621 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getAssertions(), asserts);
622 [ + - ][ + - ]: 1 : }
[ + - ]
623 : :
624 : 4 : TEST_F(TestApiBlackSolver, getInfo)
625 : : {
626 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getInfo("name"));
[ + - ][ - - ]
627 : 3 : ASSERT_THROW(d_solver->getInfo("asdf"), CVC5ApiException);
628 : : }
629 : :
630 : 4 : TEST_F(TestApiBlackSolver, getOption)
631 : : {
632 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getOption("incremental"));
[ + - ][ - - ]
633 : 3 : ASSERT_THROW(d_solver->getOption("asdf"), CVC5ApiException);
634 : : }
635 : :
636 : 4 : TEST_F(TestApiBlackSolver, getOptionNames)
637 : : {
638 : 1 : std::vector<std::string> names = d_solver->getOptionNames();
639 [ - + ][ + - ]: 1 : ASSERT_TRUE(names.size() > 100);
640 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(names.begin(), names.end(), "verbose"), names.end());
641 [ - + ][ + - ]: 1 : ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end());
642 [ + - ]: 1 : }
643 : :
644 : 4 : TEST_F(TestApiBlackSolver, getOptionInfo)
645 : : {
646 : 1 : d_solver->setOption("verbosity", "2");
647 : :
648 : : {
649 : 3 : ASSERT_THROW(d_solver->getOptionInfo("asdf-invalid"), CVC5ApiException);
650 : : }
651 : : {
652 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("verbose");
653 [ - + ][ + - ]: 1 : ASSERT_EQ("verbose", info.name);
654 [ - + ][ + - ]: 2 : ASSERT_EQ(std::vector<std::string>{}, info.aliases);
655 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON);
656 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
657 [ - + ][ + - ]: 1 : ASSERT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
658 : 1 : std::stringstream ss;
659 : 1 : ss << info;
660 [ - + ][ + - ]: 2 : ASSERT_EQ(ss.str(), "OptionInfo{ verbose | void }");
661 [ + - ]: 1 : }
662 : : {
663 : : // bool type with default
664 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("print-success");
665 [ - + ][ + - ]: 1 : ASSERT_EQ("print-success", info.name);
666 [ - + ][ + - ]: 2 : ASSERT_EQ(std::vector<std::string>{}, info.aliases);
667 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON);
668 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
669 [ - + ]: 1 : ASSERT_TRUE(
670 [ + - ]: 1 : std::holds_alternative<OptionInfo::ValueInfo<bool>>(info.valueInfo));
671 : 1 : auto valInfo = std::get<OptionInfo::ValueInfo<bool>>(info.valueInfo);
672 [ - + ][ + - ]: 1 : ASSERT_EQ(false, valInfo.defaultValue);
673 [ - + ][ + - ]: 1 : ASSERT_EQ(false, valInfo.currentValue);
674 [ - + ][ + - ]: 1 : ASSERT_EQ(info.boolValue(), false);
675 : 1 : std::stringstream ss;
676 : 1 : ss << info;
677 [ - + ]: 2 : ASSERT_EQ(ss.str(),
678 [ + - ]: 1 : "OptionInfo{ print-success | bool | false | default false }");
679 [ + - ]: 1 : }
680 : : {
681 : : // int64 type with default
682 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("verbosity");
683 [ - + ][ + - ]: 1 : ASSERT_EQ("verbosity", info.name);
684 [ - + ][ + - ]: 2 : ASSERT_EQ(std::vector<std::string>{}, info.aliases);
685 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON);
686 [ - + ][ + - ]: 1 : ASSERT_TRUE(info.setByUser);
687 [ - + ]: 1 : ASSERT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
688 [ + - ]: 1 : info.valueInfo));
689 : 1 : auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo);
690 [ - + ][ + - ]: 1 : ASSERT_EQ(0, numInfo.defaultValue);
691 [ - + ][ + - ]: 1 : ASSERT_EQ(2, numInfo.currentValue);
692 [ + - ][ + - ]: 1 : ASSERT_FALSE(numInfo.minimum || numInfo.maximum);
[ - + ][ + - ]
693 [ - + ][ + - ]: 1 : ASSERT_EQ(info.intValue(), 2);
694 : 1 : std::stringstream ss;
695 : 1 : ss << info;
696 [ - + ]: 2 : ASSERT_EQ(
697 : : ss.str(),
698 [ + - ]: 1 : "OptionInfo{ verbosity | set by user | int64_t | 2 | default 0 }");
699 [ + - ]: 1 : }
700 : : {
701 : : // uint64 type with default
702 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("rlimit");
703 [ - + ][ + - ]: 1 : ASSERT_EQ("rlimit", info.name);
704 [ - + ][ + - ]: 2 : ASSERT_EQ(std::vector<std::string>{}, info.aliases);
705 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON);
706 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
707 [ - + ]: 1 : ASSERT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(
708 [ + - ]: 1 : info.valueInfo));
709 : 1 : auto numInfo = std::get<OptionInfo::NumberInfo<uint64_t>>(info.valueInfo);
710 [ - + ][ + - ]: 1 : ASSERT_EQ(0, numInfo.defaultValue);
711 [ - + ][ + - ]: 1 : ASSERT_EQ(0, numInfo.currentValue);
712 [ + - ][ + - ]: 1 : ASSERT_FALSE(numInfo.minimum || numInfo.maximum);
[ - + ][ + - ]
713 [ - + ][ + - ]: 1 : ASSERT_EQ(info.uintValue(), 0);
714 : 1 : std::stringstream ss;
715 : 1 : ss << info;
716 [ - + ][ + - ]: 2 : ASSERT_EQ(ss.str(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }");
717 [ + - ]: 1 : }
718 : : // string type
719 : : {
720 : 2 : auto info = d_solver->getOptionInfo("random-freq");
721 [ - + ][ + - ]: 1 : ASSERT_EQ(info.name, "random-freq");
722 [ - + ][ + - ]: 4 : ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"});
723 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::EXPERT);
724 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
725 [ - + ]: 1 : ASSERT_TRUE(std::holds_alternative<cvc5::OptionInfo::NumberInfo<double>>(
726 [ + - ]: 1 : info.valueInfo));
727 : 1 : auto ni = std::get<cvc5::OptionInfo::NumberInfo<double>>(info.valueInfo);
728 [ - + ][ + - ]: 1 : ASSERT_EQ(ni.currentValue, 0.0);
729 [ - + ][ + - ]: 1 : ASSERT_EQ(ni.defaultValue, 0.0);
730 [ + - ][ + - ]: 1 : ASSERT_TRUE(ni.minimum && ni.maximum);
[ - + ][ + - ]
731 [ - + ][ + - ]: 1 : ASSERT_EQ(*ni.minimum, 0.0);
732 [ - + ][ + - ]: 1 : ASSERT_EQ(*ni.maximum, 1.0);
733 [ - + ][ + - ]: 1 : ASSERT_EQ(info.doubleValue(), 0.0);
734 : 1 : std::stringstream ss;
735 : 1 : ss << info;
736 [ - + ]: 2 : ASSERT_EQ(ss.str(),
737 : : "OptionInfo{ random-freq, random-frequency | double | 0 | "
738 [ + - ]: 1 : "default 0 | 0 <= x <= 1 }");
739 [ + - ]: 1 : }
740 : : {
741 : : // string type with default
742 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("force-logic");
743 [ - + ][ + - ]: 1 : ASSERT_EQ("force-logic", info.name);
744 [ - + ][ + - ]: 2 : ASSERT_EQ(std::vector<std::string>{}, info.aliases);
745 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON);
746 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
747 [ - + ]: 1 : ASSERT_TRUE(std::holds_alternative<OptionInfo::ValueInfo<std::string>>(
748 [ + - ]: 1 : info.valueInfo));
749 : 1 : auto valInfo = std::get<OptionInfo::ValueInfo<std::string>>(info.valueInfo);
750 [ - + ][ + - ]: 1 : ASSERT_EQ("", valInfo.defaultValue);
751 [ - + ][ + - ]: 1 : ASSERT_EQ("", valInfo.currentValue);
752 [ - + ][ + - ]: 2 : ASSERT_EQ(info.stringValue(), "");
753 : 1 : std::stringstream ss;
754 : 1 : ss << info;
755 [ - + ]: 2 : ASSERT_EQ(ss.str(),
756 [ + - ]: 1 : "OptionInfo{ force-logic | string | \"\" | default \"\" }");
757 [ + - ][ + - ]: 1 : }
758 : : {
759 : : // mode option
760 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("simplification");
761 [ - + ][ + - ]: 1 : ASSERT_EQ("simplification", info.name);
762 [ - + ][ + - ]: 4 : ASSERT_EQ(std::vector<std::string>{"simplification-mode"}, info.aliases);
763 [ - + ][ + - ]: 1 : ASSERT_EQ(info.category, cvc5::modes::OptionCategory::REGULAR);
764 [ - + ][ + - ]: 1 : ASSERT_FALSE(info.setByUser);
765 [ - + ][ + - ]: 1 : ASSERT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
766 : 1 : auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
767 [ - + ][ + - ]: 1 : ASSERT_EQ("batch", modeInfo.defaultValue);
768 [ - + ][ + - ]: 1 : ASSERT_EQ("batch", modeInfo.currentValue);
769 [ - + ][ + - ]: 1 : ASSERT_EQ(2, modeInfo.modes.size());
770 [ - + ]: 1 : ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch")
771 [ + - ]: 1 : != modeInfo.modes.end());
772 [ - + ]: 1 : ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none")
773 [ + - ]: 1 : != modeInfo.modes.end());
774 : 1 : std::stringstream ss;
775 : 1 : ss << info;
776 [ - + ]: 2 : ASSERT_EQ(ss.str(),
777 : : "OptionInfo{ simplification, simplification-mode | mode | batch "
778 [ + - ]: 1 : "| default batch | modes: batch, none }");
779 [ + - ][ + - ]: 1 : }
780 : : }
781 : :
782 : 4 : TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
783 : : {
784 : 1 : d_solver->setOption("incremental", "false");
785 : 1 : d_solver->checkSatAssuming(d_tm.mkFalse());
786 : 1 : ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException);
787 : : }
788 : :
789 : 4 : TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
790 : : {
791 : 1 : d_solver->setOption("incremental", "true");
792 : 1 : d_solver->setOption("produce-unsat-assumptions", "false");
793 : 1 : d_solver->checkSatAssuming(d_tm.mkFalse());
794 : 1 : ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException);
795 : : }
796 : :
797 : 4 : TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
798 : : {
799 : 1 : d_solver->setOption("incremental", "true");
800 : 1 : d_solver->setOption("produce-unsat-assumptions", "true");
801 : 1 : d_solver->checkSatAssuming(d_tm.mkFalse());
802 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getUnsatAssumptions());
[ + - ][ - - ]
803 : 1 : d_solver->checkSatAssuming(d_tm.mkTrue());
804 : 1 : ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException);
805 : : }
806 : :
807 : 4 : TEST_F(TestApiBlackSolver, getUnsatCore1)
808 : : {
809 : 1 : d_solver->setOption("incremental", "false");
810 : 1 : d_solver->assertFormula(d_tm.mkFalse());
811 : 1 : d_solver->checkSat();
812 : 1 : ASSERT_THROW(d_solver->getUnsatCore(), CVC5ApiException);
813 : : }
814 : :
815 : 4 : TEST_F(TestApiBlackSolver, getUnsatCore2)
816 : : {
817 : 1 : d_solver->setOption("incremental", "false");
818 : 1 : d_solver->setOption("produce-unsat-cores", "false");
819 : 1 : d_solver->assertFormula(d_tm.mkFalse());
820 : 1 : d_solver->checkSat();
821 : 1 : ASSERT_THROW(d_solver->getUnsatCore(), CVC5ApiException);
822 : : }
823 : :
824 : 4 : TEST_F(TestApiBlackSolver, getUnsatCoreAndProof)
825 : : {
826 : 1 : d_solver->setOption("incremental", "true");
827 : 1 : d_solver->setOption("produce-unsat-cores", "true");
828 : 1 : d_solver->setOption("produce-proofs", "true");
829 : :
830 : 3 : Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
831 : 3 : Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool);
832 : 1 : std::vector<Term> uc;
833 : :
834 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
835 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
836 : 1 : Term f = d_tm.mkConst(uToIntSort, "f");
837 : 1 : Term p = d_tm.mkConst(intPredSort, "p");
838 : 1 : Term zero = d_tm.mkInteger(0);
839 : 1 : Term one = d_tm.mkInteger(1);
840 : 4 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
841 : 4 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
842 : 4 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
843 : 4 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
844 : 4 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
845 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x}));
846 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y}));
847 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one}));
848 : 1 : d_solver->assertFormula(p_0);
849 : 1 : d_solver->assertFormula(p_f_y.notTerm());
850 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
851 : :
852 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(uc = d_solver->getUnsatCore());
[ + - ][ - - ]
853 [ - + ][ + - ]: 1 : ASSERT_FALSE(uc.empty());
854 : :
855 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getProof());
[ + - ][ - - ]
856 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getProof(modes::ProofComponent::SAT));
[ + - ][ - - ]
857 : :
858 : 1 : d_solver->resetAssertions();
859 [ + + ]: 4 : for (const auto& t : uc)
860 : : {
861 : 3 : d_solver->assertFormula(t);
862 : : }
863 : 1 : cvc5::Result res = d_solver->checkSat();
864 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.isUnsat());
865 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getProof());
[ + - ][ - - ]
866 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
867 : :
868 : 4 : TEST_F(TestApiBlackSolver, getUnsatCoreLemmas1)
869 : : {
870 : 1 : d_solver->setOption("produce-unsat-cores", "true");
871 : 1 : d_solver->setOption("unsat-cores-mode", "sat-proof");
872 : : // cannot ask before a check sat
873 : 1 : ASSERT_THROW(d_solver->getUnsatCoreLemmas(), CVC5ApiException);
874 : :
875 : 1 : d_solver->assertFormula(d_tm.mkFalse());
876 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
877 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getUnsatCoreLemmas());
[ + - ][ - - ]
878 : : }
879 : :
880 : 4 : TEST_F(TestApiBlackSolver, getUnsatCoreLemmas2)
881 : : {
882 : 1 : d_solver->setOption("incremental", "true");
883 : 1 : d_solver->setOption("produce-unsat-cores", "true");
884 : 1 : d_solver->setOption("produce-proofs", "true");
885 : :
886 : 3 : Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
887 : 3 : Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool);
888 : :
889 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
890 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
891 : 1 : Term f = d_tm.mkConst(uToIntSort, "f");
892 : 1 : Term p = d_tm.mkConst(intPredSort, "p");
893 : 1 : Term zero = d_tm.mkInteger(0);
894 : 1 : Term one = d_tm.mkInteger(1);
895 : 4 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
896 : 4 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
897 : 4 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
898 : 4 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
899 : 4 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
900 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x}));
901 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y}));
902 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one}));
903 : 1 : d_solver->assertFormula(p_0);
904 : 1 : d_solver->assertFormula(p_f_y.notTerm());
905 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
906 : :
907 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getUnsatCoreLemmas());
[ + - ][ - - ]
908 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
909 : :
910 : 4 : TEST_F(TestApiBlackSolver, getAbduct)
911 : : {
912 : 1 : d_solver->setLogic("QF_LIA");
913 : 1 : d_solver->setOption("produce-abducts", "true");
914 : 1 : d_solver->setOption("incremental", "false");
915 : :
916 : 1 : Term zero = d_tm.mkInteger(0);
917 : 1 : Term x = d_tm.mkConst(d_int, "x");
918 : 1 : Term y = d_tm.mkConst(d_int, "y");
919 : :
920 : : // Assumptions for abduction: x > 0
921 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero}));
922 : : // Conjecture for abduction: y > 0
923 : 4 : Term conj = d_tm.mkTerm(Kind::GT, {y, zero});
924 : : // Call the abduction api, while the resulting abduct is the output
925 : 1 : Term output = d_solver->getAbduct(conj);
926 : : // We expect the resulting output to be a boolean formula
927 [ + - ][ + - ]: 2 : ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean());
[ + - ][ - + ]
[ + - ][ - - ]
928 : :
929 : : // try with a grammar, a simple grammar admitting true
930 : 1 : Term truen = d_tm.mkBoolean(true);
931 : 1 : Term start = d_tm.mkVar(d_bool);
932 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
933 : 4 : Term conj2 = d_tm.mkTerm(Kind::GT, {x, zero});
934 : 1 : ASSERT_THROW(d_solver->getAbduct(conj2, g), CVC5ApiException);
935 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g.addRule(start, truen));
[ + - ][ - - ]
936 : : // Call the abduction api, while the resulting abduct is the output
937 : 1 : Term output2 = d_solver->getAbduct(conj2, g);
938 : : // abduct must be true
939 [ - + ][ + - ]: 1 : ASSERT_EQ(output2, truen);
940 : :
941 : 1 : TermManager tm;
942 : 1 : Solver slv(tm);
943 : 1 : slv.setOption("produce-abducts", "true");
944 : 1 : Sort intSort2 = tm.getIntegerSort();
945 : 1 : Term xx = tm.mkConst(intSort2, "x");
946 : 1 : Term yy = tm.mkConst(intSort2, "y");
947 : 1 : Term zzero = tm.mkInteger(0);
948 : 2 : Term sstart = tm.mkVar(tm.getBooleanSort());
949 : 1 : slv.assertFormula(
950 : 6 : tm.mkTerm(Kind::GT, {tm.mkTerm(Kind::ADD, {xx, yy}), zzero}));
951 : 3 : Grammar gg = slv.mkGrammar({}, {sstart});
952 : 1 : gg.addRule(sstart, tm.mkTrue());
953 : 4 : Term cconj2 = tm.mkTerm(Kind::EQUAL, {zzero, zzero});
954 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.getAbduct(cconj2, gg));
[ + - ][ - - ]
955 : 1 : ASSERT_THROW(slv.getAbduct(conj2), CVC5ApiException);
956 : 1 : ASSERT_THROW(slv.getAbduct(conj2, gg), CVC5ApiException);
957 : 1 : ASSERT_THROW(slv.getAbduct(cconj2, g), CVC5ApiException);
958 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
959 : :
960 : 4 : TEST_F(TestApiBlackSolver, getAbduct2)
961 : : {
962 : 1 : d_solver->setLogic("QF_LIA");
963 : 1 : d_solver->setOption("incremental", "false");
964 : 1 : Term zero = d_tm.mkInteger(0);
965 : 1 : Term x = d_tm.mkConst(d_int, "x");
966 : 1 : Term y = d_tm.mkConst(d_int, "y");
967 : : // Assumptions for abduction: x > 0
968 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero}));
969 : : // Conjecture for abduction: y > 0
970 : 4 : Term conj = d_tm.mkTerm(Kind::GT, {y, zero});
971 : : // Fails due to option not set
972 : 1 : ASSERT_THROW(d_solver->getAbduct(conj), CVC5ApiException);
973 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
974 : :
975 : 4 : TEST_F(TestApiBlackSolver, getAbductNext)
976 : : {
977 : 1 : d_solver->setLogic("QF_LIA");
978 : 1 : d_solver->setOption("produce-abducts", "true");
979 : 1 : d_solver->setOption("incremental", "true");
980 : :
981 : 1 : Term zero = d_tm.mkInteger(0);
982 : 1 : Term x = d_tm.mkConst(d_int, "x");
983 : 1 : Term y = d_tm.mkConst(d_int, "y");
984 : :
985 : : // Assumptions for abduction: x > 0
986 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero}));
987 : : // Conjecture for abduction: y > 0
988 : 4 : Term conj = d_tm.mkTerm(Kind::GT, {y, zero});
989 : : // Call the abduction api, while the resulting abduct is the output
990 : 1 : Term output = d_solver->getAbduct(conj);
991 : 1 : Term output2 = d_solver->getAbductNext();
992 : : // should produce a different output
993 [ - + ][ + - ]: 1 : ASSERT_TRUE(output != output2);
994 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
995 : :
996 : 4 : TEST_F(TestApiBlackSolver, getInterpolant)
997 : : {
998 : 1 : d_solver->setLogic("QF_LIA");
999 : 1 : d_solver->setOption("produce-interpolants", "true");
1000 : 1 : d_solver->setOption("incremental", "false");
1001 : :
1002 : 1 : Term zero = d_tm.mkInteger(0);
1003 : 1 : Term x = d_tm.mkConst(d_int, "x");
1004 : 1 : Term y = d_tm.mkConst(d_int, "y");
1005 : 1 : Term z = d_tm.mkConst(d_int, "z");
1006 : :
1007 : : // Assumptions for interpolation: x + y > 0 /\ x < 0
1008 : 2 : d_solver->assertFormula(
1009 : 6 : d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {x, y}), zero}));
1010 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::LT, {x, zero}));
1011 : : // Conjecture for interpolation: y + z > 0 \/ z < 0
1012 : 2 : Term conj = d_tm.mkTerm(
1013 : : Kind::OR,
1014 : 4 : {d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {y, z}), zero}),
1015 : 7 : d_tm.mkTerm(Kind::LT, {z, zero})});
1016 : : // Call the interpolation api, while the resulting interpolant is the output
1017 : 1 : Term output = d_solver->getInterpolant(conj);
1018 : : // We expect the resulting output to be a boolean formula
1019 [ - + ][ + - ]: 1 : ASSERT_TRUE(output.getSort().isBoolean());
1020 : :
1021 : : // try with a grammar, a simple grammar admitting true
1022 : 1 : Term truen = d_tm.mkBoolean(true);
1023 : 1 : Term start = d_tm.mkVar(d_bool);
1024 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
1025 : 4 : Term conj2 = d_tm.mkTerm(Kind::EQUAL, {zero, zero});
1026 : 1 : ASSERT_THROW(d_solver->getInterpolant(conj2, g), CVC5ApiException);
1027 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(g.addRule(start, truen));
[ + - ][ - - ]
1028 : : // Call the interpolation api, while the resulting interpolant is the output
1029 : 1 : Term output2 = d_solver->getInterpolant(conj2, g);
1030 : : // interpolant must be true
1031 [ - + ][ + - ]: 1 : ASSERT_EQ(output2, truen);
1032 : :
1033 : 1 : TermManager tm;
1034 : 1 : Solver slv(tm);
1035 : 1 : slv.setOption("produce-interpolants", "true");
1036 : 1 : Term zzero = tm.mkInteger(0);
1037 : 2 : Term sstart = tm.mkVar(tm.getBooleanSort());
1038 : 3 : Grammar gg = slv.mkGrammar({}, {sstart});
1039 : 1 : gg.addRule(sstart, tm.mkTrue());
1040 : 4 : Term cconj2 = tm.mkTerm(Kind::EQUAL, {zzero, zzero});
1041 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.getInterpolant(cconj2, gg));
[ + - ][ - - ]
1042 : 1 : ASSERT_THROW(slv.getInterpolant(conj2), CVC5ApiException);
1043 : 1 : ASSERT_THROW(slv.getInterpolant(conj2, gg), CVC5ApiException);
1044 : 1 : ASSERT_THROW(slv.getInterpolant(cconj2, g), CVC5ApiException);
1045 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1046 : :
1047 : 4 : TEST_F(TestApiBlackSolver, getInterpolantNext)
1048 : : {
1049 : 1 : d_solver->setLogic("QF_LIA");
1050 : 1 : d_solver->setOption("produce-interpolants", "true");
1051 : 1 : d_solver->setOption("incremental", "true");
1052 : :
1053 : 1 : Term zero = d_tm.mkInteger(0);
1054 : 1 : Term x = d_tm.mkConst(d_int, "x");
1055 : 1 : Term y = d_tm.mkConst(d_int, "y");
1056 : 1 : Term z = d_tm.mkConst(d_int, "z");
1057 : : // Assumptions for interpolation: x + y > 0 /\ x < 0
1058 : 2 : d_solver->assertFormula(
1059 : 6 : d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {x, y}), zero}));
1060 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::LT, {x, zero}));
1061 : : // Conjecture for interpolation: y + z > 0 \/ z < 0
1062 : 2 : Term conj = d_tm.mkTerm(
1063 : : Kind::OR,
1064 : 4 : {d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {y, z}), zero}),
1065 : 7 : d_tm.mkTerm(Kind::LT, {z, zero})});
1066 : 1 : Term output = d_solver->getInterpolant(conj);
1067 : 1 : Term output2 = d_solver->getInterpolantNext();
1068 : :
1069 : : // We expect the next output to be distinct
1070 [ - + ][ + - ]: 1 : ASSERT_TRUE(output != output2);
1071 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1072 : :
1073 : 4 : TEST_F(TestApiBlackSolver, declarePool)
1074 : : {
1075 : 1 : Sort setSort = d_tm.mkSetSort(d_int);
1076 : 1 : Term zero = d_tm.mkInteger(0);
1077 : 1 : Term x = d_tm.mkConst(d_int, "x");
1078 : 1 : Term y = d_tm.mkConst(d_int, "y");
1079 : : // declare a pool with initial value { 0, x, y }
1080 : 5 : Term p = d_solver->declarePool("p", d_int, {zero, x, y});
1081 : : // pool should have the same sort
1082 [ - + ][ + - ]: 1 : ASSERT_TRUE(p.getSort() == setSort);
1083 : : // cannot pass null sort
1084 : 1 : Sort nullSort;
1085 : 4 : ASSERT_THROW(d_solver->declarePool("i", nullSort, {}), CVC5ApiException);
1086 : :
1087 : 1 : TermManager tm;
1088 : 1 : Solver slv(tm);
1089 : 1 : Sort tm_int = tm.getIntegerSort();
1090 : 1 : Term tm_zero = tm.mkInteger(0);
1091 : 1 : Term tm_x = tm.mkConst(tm_int, "x");
1092 : 1 : Term tm_y = tm.mkConst(tm_int, "y");
1093 : 9 : ASSERT_THROW(slv.declarePool("p", d_int, {tm_zero, tm_x, tm_y}),
1094 [ + - ]: 1 : CVC5ApiException);
1095 : 9 : ASSERT_THROW(slv.declarePool("p", tm_int, {zero, tm_x, tm_y}),
1096 [ + - ]: 1 : CVC5ApiException);
1097 : 9 : ASSERT_THROW(slv.declarePool("p", tm_int, {tm_zero, x, tm_y}),
1098 [ + - ]: 1 : CVC5ApiException);
1099 : 9 : ASSERT_THROW(slv.declarePool("p", tm_int, {tm_zero, tm_x, y}),
1100 [ + - ]: 1 : CVC5ApiException);
1101 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
1102 : :
1103 : 4 : TEST_F(TestApiBlackSolver, getDriverOptions)
1104 : : {
1105 : 1 : auto dopts = d_solver->getDriverOptions();
1106 [ - + ][ + - ]: 1 : ASSERT_EQ(dopts.err().rdbuf(), std::cerr.rdbuf());
1107 [ - + ][ + - ]: 1 : ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf());
1108 [ - + ][ + - ]: 1 : ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf());
1109 : : }
1110 : :
1111 : 4 : TEST_F(TestApiBlackSolver, getStatistics)
1112 : : {
1113 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(cvc5::Stat());
[ + - ][ - - ]
1114 : : // do some array reasoning to make sure we have statistics
1115 : : {
1116 : 1 : Sort s2 = d_tm.mkArraySort(d_int, d_int);
1117 : 1 : Term t1 = d_tm.mkConst(d_int, "i");
1118 : 1 : Term t2 = d_tm.mkConst(s2, "a");
1119 : 4 : Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1});
1120 : 1 : d_solver->assertFormula(t3.eqTerm(t1));
1121 : 1 : d_solver->checkSat();
1122 : 1 : }
1123 : 1 : cvc5::Statistics stats = d_solver->getStatistics();
1124 : 1 : std::stringstream ss;
1125 : 1 : ss << stats;
1126 : : {
1127 : 2 : auto s = stats.get("global::totalTime");
1128 [ - + ][ + - ]: 1 : ASSERT_FALSE(s.isInternal());
1129 [ - + ][ + - ]: 1 : ASSERT_FALSE(s.isDefault());
1130 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.isString());
1131 : 1 : std::string time = s.getString();
1132 [ - + ][ + - ]: 1 : ASSERT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms"
1133 [ - + ][ + - ]: 1 : ASSERT_FALSE(s.isDouble());
1134 : 1 : ss << s << s.toString();
1135 : 1 : s = stats.get("resource::resourceUnitsUsed");
1136 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.isInternal());
1137 [ - + ][ + - ]: 1 : ASSERT_FALSE(s.isDefault());
1138 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.isInt());
1139 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.getInt() >= 0);
1140 : 1 : ss << s << s.toString();
1141 [ + - ]: 1 : }
1142 : 1 : bool hasstats = false;
1143 [ + + ]: 517 : for (const auto& s : stats)
1144 : : {
1145 : 516 : hasstats = true;
1146 [ - + ][ + - ]: 516 : ASSERT_FALSE(s.first.empty());
1147 : : }
1148 [ - + ][ + - ]: 1 : ASSERT_TRUE(hasstats);
1149 : 1 : hasstats = false;
1150 [ + + ]: 517 : for (auto it = stats.begin(true, true); it != stats.end(); ++it)
1151 : : {
1152 : 516 : hasstats = true;
1153 : : {
1154 : 516 : auto tmp1 = it, tmp2 = it;
1155 : 516 : ++tmp1;
1156 : 516 : tmp2++;
1157 [ - + ][ + - ]: 516 : ASSERT_EQ(tmp1, tmp2);
1158 : 516 : --tmp1;
1159 : 516 : tmp2--;
1160 [ - + ][ + - ]: 516 : ASSERT_EQ(tmp1, tmp2);
1161 [ - + ][ + - ]: 516 : ASSERT_EQ(tmp1, it);
1162 [ - + ][ + - ]: 516 : ASSERT_EQ(it, tmp2);
1163 : : }
1164 : 516 : const auto& s = *it;
1165 : : // check some basic utility methods
1166 [ - + ][ + - ]: 516 : ASSERT_TRUE(!(it == stats.end()));
1167 [ - + ][ + - ]: 516 : ASSERT_EQ(s.first, it->first);
1168 [ + + ]: 516 : if (s.first == "theory::arrays::avgIndexListLength")
1169 : : {
1170 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.second.isInternal());
1171 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.second.isDouble());
1172 [ - + ][ + - ]: 1 : ASSERT_TRUE(std::isnan(s.second.getDouble()));
1173 : : }
1174 : : }
1175 [ - + ][ + - ]: 1 : ASSERT_TRUE(hasstats);
1176 : : }
1177 : :
1178 : 4 : TEST_F(TestApiBlackSolver, printStatisticsSafe)
1179 : : {
1180 : : // do some array reasoning to make sure we have statistics
1181 : : {
1182 : 1 : Sort s2 = d_tm.mkArraySort(d_int, d_int);
1183 : 1 : Term t1 = d_tm.mkConst(d_int, "i");
1184 : 1 : Term t2 = d_tm.mkConst(s2, "a");
1185 : 4 : Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1});
1186 : 1 : d_solver->assertFormula(t3.eqTerm(t1));
1187 : 1 : d_solver->checkSat();
1188 : 1 : }
1189 : 1 : testing::internal::CaptureStdout();
1190 : 1 : d_solver->printStatisticsSafe(STDOUT_FILENO);
1191 : 1 : testing::internal::GetCapturedStdout();
1192 : 1 : }
1193 : :
1194 : 4 : TEST_F(TestApiBlackSolver, getProofAndProofToString)
1195 : : {
1196 : 1 : d_solver->setOption("produce-proofs", "true");
1197 : :
1198 : 3 : Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
1199 : 3 : Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool);
1200 : 1 : std::vector<Proof> proofs;
1201 : :
1202 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1203 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1204 : 1 : Term f = d_tm.mkConst(uToIntSort, "f");
1205 : 1 : Term p = d_tm.mkConst(intPredSort, "p");
1206 : 1 : Term zero = d_tm.mkInteger(0);
1207 : 1 : Term one = d_tm.mkInteger(1);
1208 : 4 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
1209 : 4 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
1210 : 4 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
1211 : 4 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
1212 : 4 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
1213 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x}));
1214 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y}));
1215 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one}));
1216 : 1 : d_solver->assertFormula(p_0);
1217 : 1 : d_solver->assertFormula(p_f_y.notTerm());
1218 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
1219 : :
1220 : 1 : std::string printedProof;
1221 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proofs = d_solver->getProof());
[ + - ][ - - ]
1222 [ - + ][ + - ]: 1 : ASSERT_FALSE(proofs.empty());
1223 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(printedProof = d_solver->proofToString(proofs[0]));
[ + - ][ - - ]
1224 [ - + ][ + - ]: 1 : ASSERT_FALSE(printedProof.empty());
1225 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(printedProof = d_solver->proofToString(
[ - - ]
1226 [ + - ]: 1 : proofs[0], modes::ProofFormat::ALETHE));
1227 [ - + ][ + - ]: 1 : ASSERT_FALSE(printedProof.empty());
1228 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proofs = d_solver->getProof(modes::ProofComponent::SAT));
[ + - ][ - - ]
1229 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(printedProof = d_solver->proofToString(
[ - - ]
1230 [ + - ]: 1 : proofs[0], modes::ProofFormat::NONE));
1231 [ - + ][ + - ]: 1 : ASSERT_FALSE(printedProof.empty());
1232 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
1233 : :
1234 : 4 : TEST_F(TestApiBlackSolver, proofToStringAssertionNames)
1235 : : {
1236 : 1 : d_solver->setOption("produce-proofs", "true");
1237 : :
1238 : 1 : std::vector<Proof> proofs;
1239 : :
1240 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1241 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1242 : :
1243 : 4 : Term x_eq_y = d_tm.mkTerm(Kind::EQUAL, {x, y});
1244 : 3 : Term not_x_eq_y = d_tm.mkTerm(Kind::NOT, {x_eq_y});
1245 : :
1246 : 1 : std::map<cvc5::Term, std::string> assertionNames;
1247 : 1 : assertionNames.emplace(x_eq_y, "as1");
1248 : 1 : assertionNames.emplace(not_x_eq_y, "as2");
1249 : :
1250 : 1 : d_solver->assertFormula(x_eq_y);
1251 : 1 : d_solver->assertFormula(not_x_eq_y);
1252 : :
1253 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
1254 : :
1255 : 1 : std::string printedProof;
1256 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proofs = d_solver->getProof());
[ + - ][ - - ]
1257 [ - + ][ + - ]: 1 : ASSERT_FALSE(proofs.empty());
1258 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(printedProof = d_solver->proofToString(
[ - - ]
1259 [ + - ]: 1 : proofs[0], modes::ProofFormat::ALETHE, assertionNames));
1260 [ - + ][ + - ]: 1 : ASSERT_FALSE(printedProof.empty());
1261 [ - + ][ + - ]: 1 : ASSERT_LT(printedProof.find("as1"), std::string::npos);
1262 [ - + ][ + - ]: 1 : ASSERT_LT(printedProof.find("as2"), std::string::npos);
1263 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1264 : :
1265 : 4 : TEST_F(TestApiBlackSolver, getDifficulty)
1266 : : {
1267 : 1 : d_solver->setOption("produce-difficulty", "true");
1268 : : // cannot ask before a check sat
1269 : 1 : ASSERT_THROW(d_solver->getDifficulty(), CVC5ApiException);
1270 : 1 : d_solver->checkSat();
1271 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getDifficulty());
[ + - ][ - - ]
1272 : : }
1273 : :
1274 : 4 : TEST_F(TestApiBlackSolver, getDifficulty2)
1275 : : {
1276 : 1 : d_solver->checkSat();
1277 : : // option is not set
1278 : 1 : ASSERT_THROW(d_solver->getDifficulty(), CVC5ApiException);
1279 : : }
1280 : :
1281 : 4 : TEST_F(TestApiBlackSolver, getDifficulty3)
1282 : : {
1283 : 1 : d_solver->setOption("produce-difficulty", "true");
1284 : 1 : Term x = d_tm.mkConst(d_int, "x");
1285 : 1 : Term zero = d_tm.mkInteger(0);
1286 : 1 : Term ten = d_tm.mkInteger(10);
1287 : 4 : Term f0 = d_tm.mkTerm(Kind::GEQ, {x, ten});
1288 : 4 : Term f1 = d_tm.mkTerm(Kind::GEQ, {zero, x});
1289 : 1 : d_solver->assertFormula(f0);
1290 : 1 : d_solver->assertFormula(f1);
1291 : 1 : d_solver->checkSat();
1292 : 1 : std::map<Term, Term> dmap;
1293 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(dmap = d_solver->getDifficulty());
[ + - ][ - - ]
1294 : : // difficulty should map assertions to integer values
1295 [ + + ]: 3 : for (const std::pair<const Term, Term>& t : dmap)
1296 : : {
1297 [ + + ][ + - ]: 2 : ASSERT_TRUE(t.first == f0 || t.first == f1);
[ - + ][ + - ]
1298 [ - + ][ + - ]: 2 : ASSERT_TRUE(t.second.getKind() == Kind::CONST_INTEGER);
1299 : : }
1300 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1301 : :
1302 : 4 : TEST_F(TestApiBlackSolver, getLearnedLiterals)
1303 : : {
1304 : 1 : d_solver->setOption("produce-learned-literals", "true");
1305 : : // cannot ask before a check sat
1306 : 1 : ASSERT_THROW(d_solver->getLearnedLiterals(), CVC5ApiException);
1307 : 1 : d_solver->checkSat();
1308 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getLearnedLiterals());
[ + - ][ - - ]
1309 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(
[ - - ]
1310 [ + - ]: 1 : d_solver->getLearnedLiterals(modes::LearnedLitType::PREPROCESS));
1311 : : }
1312 : :
1313 : 4 : TEST_F(TestApiBlackSolver, getLearnedLiterals2)
1314 : : {
1315 : 1 : d_solver->setOption("produce-learned-literals", "true");
1316 : 1 : Term x = d_tm.mkConst(d_int, "x");
1317 : 1 : Term y = d_tm.mkConst(d_int, "y");
1318 : 1 : Term zero = d_tm.mkInteger(0);
1319 : 1 : Term ten = d_tm.mkInteger(10);
1320 : 4 : Term f0 = d_tm.mkTerm(Kind::GEQ, {x, ten});
1321 : 2 : Term f1 = d_tm.mkTerm(
1322 : : Kind::OR,
1323 : 8 : {d_tm.mkTerm(Kind::GEQ, {zero, x}), d_tm.mkTerm(Kind::GEQ, {y, zero})});
1324 : 1 : d_solver->assertFormula(f0);
1325 : 1 : d_solver->assertFormula(f1);
1326 : 1 : d_solver->checkSat();
1327 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getLearnedLiterals());
[ + - ][ - - ]
1328 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1329 : :
1330 : 4 : TEST_F(TestApiBlackSolver, getTimeoutCore)
1331 : : {
1332 : 1 : d_solver->setOption("timeout-core-timeout", "100");
1333 : 1 : d_solver->setOption("produce-unsat-cores", "true");
1334 : 1 : Term x = d_tm.mkConst(d_int, "x");
1335 : 1 : Term tt = d_tm.mkBoolean(true);
1336 : : Term hard =
1337 : 2 : d_tm.mkTerm(Kind::EQUAL,
1338 : 2 : {d_tm.mkTerm(Kind::MULT, {x, x}),
1339 : 3 : d_tm.mkInteger("501240912901901249014210220059591")});
1340 : 1 : d_solver->assertFormula(tt);
1341 : 1 : d_solver->assertFormula(hard);
1342 : 1 : std::pair<cvc5::Result, std::vector<Term>> res = d_solver->getTimeoutCore();
1343 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.first.isUnknown());
1344 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.second.size() == 1);
1345 [ - + ][ + - ]: 1 : ASSERT_EQ(res.second[0], hard);
1346 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1347 : :
1348 : 4 : TEST_F(TestApiBlackSolver, getTimeoutCoreUnsat)
1349 : : {
1350 : 1 : d_solver->setOption("produce-unsat-cores", "true");
1351 : 1 : Term ff = d_tm.mkBoolean(false);
1352 : 1 : Term tt = d_tm.mkBoolean(true);
1353 : 1 : d_solver->assertFormula(tt);
1354 : 1 : d_solver->assertFormula(ff);
1355 : 1 : d_solver->assertFormula(tt);
1356 : 1 : std::pair<cvc5::Result, std::vector<Term>> res = d_solver->getTimeoutCore();
1357 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.first.isUnsat());
1358 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.second.size() == 1);
1359 [ - + ][ + - ]: 1 : ASSERT_EQ(res.second[0], ff);
1360 [ + - ][ + - ]: 1 : }
[ + - ]
1361 : :
1362 : 4 : TEST_F(TestApiBlackSolver, getTimeoutCoreAssuming)
1363 : : {
1364 : 1 : d_solver->setOption("produce-unsat-cores", "true");
1365 : 1 : Term ff = d_tm.mkBoolean(false);
1366 : 1 : Term tt = d_tm.mkBoolean(true);
1367 : 1 : d_solver->assertFormula(tt);
1368 : : std::pair<cvc5::Result, std::vector<Term>> res =
1369 : 4 : d_solver->getTimeoutCoreAssuming({ff, tt});
1370 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.first.isUnsat());
1371 [ - + ][ + - ]: 1 : ASSERT_TRUE(res.second.size() == 1);
1372 [ - + ][ + - ]: 1 : ASSERT_EQ(res.second[0], ff);
1373 [ + - ][ + - ]: 1 : }
[ + - ]
1374 : :
1375 : 4 : TEST_F(TestApiBlackSolver, getTimeoutCoreAssumingEmpty)
1376 : : {
1377 : 1 : d_solver->setOption("produce-unsat-cores", "true");
1378 : 2 : ASSERT_THROW(d_solver->getTimeoutCoreAssuming({}), CVC5ApiException);
1379 : : }
1380 : :
1381 : 4 : TEST_F(TestApiBlackSolver, getValue1)
1382 : : {
1383 : 1 : d_solver->setOption("produce-models", "false");
1384 : 1 : Term t = d_tm.mkTrue();
1385 : 1 : d_solver->assertFormula(t);
1386 : 1 : d_solver->checkSat();
1387 : 1 : ASSERT_THROW(d_solver->getValue(t), CVC5ApiException);
1388 [ + - ]: 1 : }
1389 : :
1390 : 4 : TEST_F(TestApiBlackSolver, getValue2)
1391 : : {
1392 : 1 : d_solver->setOption("produce-models", "true");
1393 : 1 : Term t = d_tm.mkFalse();
1394 : 1 : d_solver->assertFormula(t);
1395 : 1 : d_solver->checkSat();
1396 : 1 : ASSERT_THROW(d_solver->getValue(t), CVC5ApiException);
1397 [ + - ]: 1 : }
1398 : :
1399 : 4 : TEST_F(TestApiBlackSolver, getValue3)
1400 : : {
1401 : 1 : d_solver->setOption("produce-models", "true");
1402 : 3 : Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int);
1403 : 3 : Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool);
1404 : 1 : std::vector<Term> unsat_core;
1405 : :
1406 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1407 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1408 : 1 : Term z = d_tm.mkConst(d_uninterpreted, "z");
1409 : 1 : Term f = d_tm.mkConst(uToIntSort, "f");
1410 : 1 : Term p = d_tm.mkConst(intPredSort, "p");
1411 : 1 : Term zero = d_tm.mkInteger(0);
1412 : 1 : Term one = d_tm.mkInteger(1);
1413 : 4 : Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
1414 : 4 : Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y});
1415 : 4 : Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y});
1416 : 4 : Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero});
1417 : 4 : Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y});
1418 : :
1419 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {zero, f_x}));
1420 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {zero, f_y}));
1421 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {sum, one}));
1422 : 1 : d_solver->assertFormula(p_0.notTerm());
1423 : 1 : d_solver->assertFormula(p_f_y);
1424 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
1425 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValue(x));
[ + - ][ - - ]
1426 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValue(y));
[ + - ][ - - ]
1427 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValue(z));
[ + - ][ - - ]
1428 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValue(sum));
[ + - ][ - - ]
1429 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValue(p_f_y));
[ + - ][ - - ]
1430 : :
1431 : 1 : std::vector<Term> a;
1432 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(x)));
[ + - ][ - - ]
1433 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(y)));
[ + - ][ - - ]
1434 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(z)));
[ + - ][ - - ]
1435 : 1 : std::vector<Term> b;
1436 : 4 : ASSERT_NO_THROW(b = d_solver->getValue({x, y, z}));
1437 [ - + ][ + - ]: 1 : ASSERT_EQ(a, b);
1438 : :
1439 : 2 : ASSERT_THROW(Solver(d_tm).getValue(x), CVC5ApiException);
1440 : : {
1441 : 1 : Solver slv(d_tm);
1442 : 1 : slv.setOption("produce-models", "true");
1443 : 1 : ASSERT_THROW(slv.getValue(x), CVC5ApiException);
1444 [ + - ]: 1 : }
1445 : : {
1446 : 1 : Solver slv(d_tm);
1447 : 1 : slv.setOption("produce-models", "true");
1448 : 1 : slv.checkSat();
1449 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.getValue(x));
[ + - ][ - - ]
1450 [ + - ]: 1 : }
1451 : :
1452 : 1 : TermManager tm;
1453 : 1 : Solver slv(tm);
1454 : 1 : slv.setOption("produce-models", "true");
1455 : 1 : slv.checkSat();
1456 : 3 : ASSERT_THROW(slv.getValue(d_tm.mkConst(d_bool, "x")), CVC5ApiException);
1457 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1458 : :
1459 : 4 : TEST_F(TestApiBlackSolver, getModelDomainElements)
1460 : : {
1461 : 1 : d_solver->setOption("produce-models", "true");
1462 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1463 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1464 : 1 : Term z = d_tm.mkConst(d_uninterpreted, "z");
1465 : 5 : Term f = d_tm.mkTerm(Kind::DISTINCT, {x, y, z});
1466 : 1 : d_solver->assertFormula(f);
1467 : 1 : d_solver->checkSat();
1468 : 1 : auto elems = d_solver->getModelDomainElements(d_uninterpreted);
1469 [ - + ][ + - ]: 1 : ASSERT_TRUE(elems.size() >= 3);
1470 : 1 : ASSERT_THROW(d_solver->getModelDomainElements(d_int), CVC5ApiException);
1471 : :
1472 : 1 : TermManager tm;
1473 : 1 : Solver slv(tm);
1474 : 1 : slv.setOption("produce-models", "true");
1475 : 1 : slv.checkSat();
1476 : 1 : ASSERT_THROW(slv.getModelDomainElements(d_uninterpreted), CVC5ApiException);
1477 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
1478 : :
1479 : 4 : TEST_F(TestApiBlackSolver, getModelDomainElements2)
1480 : : {
1481 : 1 : d_solver->setOption("produce-models", "true");
1482 : 1 : d_solver->setOption("finite-model-find", "true");
1483 : 1 : Term x = d_tm.mkVar(d_uninterpreted, "x");
1484 : 1 : Term y = d_tm.mkVar(d_uninterpreted, "y");
1485 : 4 : Term eq = d_tm.mkTerm(Kind::EQUAL, {x, y});
1486 : 4 : Term bvl = d_tm.mkTerm(Kind::VARIABLE_LIST, {x, y});
1487 : 4 : Term f = d_tm.mkTerm(Kind::FORALL, {bvl, eq});
1488 : 1 : d_solver->assertFormula(f);
1489 : 1 : d_solver->checkSat();
1490 : 1 : auto elems = d_solver->getModelDomainElements(d_uninterpreted);
1491 : : // a model for the above must interpret u as size 1
1492 [ - + ][ + - ]: 1 : ASSERT_TRUE(elems.size() == 1);
1493 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1494 : :
1495 : 4 : TEST_F(TestApiBlackSolver, isModelCoreSymbol)
1496 : : {
1497 : 1 : d_solver->setOption("produce-models", "true");
1498 : 1 : d_solver->setOption("model-cores", "simple");
1499 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1500 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1501 : 1 : Term z = d_tm.mkConst(d_uninterpreted, "z");
1502 : 1 : Term zero = d_tm.mkInteger(0);
1503 : 6 : Term f = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::EQUAL, {x, y})});
1504 : 1 : d_solver->assertFormula(f);
1505 : 1 : d_solver->checkSat();
1506 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->isModelCoreSymbol(x));
1507 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->isModelCoreSymbol(y));
1508 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_solver->isModelCoreSymbol(z));
1509 : 1 : ASSERT_THROW(d_solver->isModelCoreSymbol(zero), CVC5ApiException);
1510 : :
1511 : 1 : TermManager tm;
1512 : 1 : Solver slv(tm);
1513 : 1 : slv.setOption("produce-models", "true");
1514 : 1 : slv.checkSat();
1515 : 3 : ASSERT_THROW(slv.isModelCoreSymbol(d_tm.mkConst(d_uninterpreted, "x")),
1516 [ + - ]: 1 : CVC5ApiException);
1517 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
1518 : :
1519 : 4 : TEST_F(TestApiBlackSolver, getModel)
1520 : : {
1521 : 1 : d_solver->setOption("produce-models", "true");
1522 : 1 : Term x = d_tm.mkConst(d_uninterpreted, "x");
1523 : 1 : Term y = d_tm.mkConst(d_uninterpreted, "y");
1524 : 1 : Term z = d_tm.mkConst(d_uninterpreted, "z");
1525 : 6 : Term f = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::EQUAL, {x, y})});
1526 : 1 : d_solver->assertFormula(f);
1527 : 1 : d_solver->checkSat();
1528 : 3 : std::vector<Sort> sorts{d_uninterpreted};
1529 : 4 : std::vector<Term> terms{x, y};
1530 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getModel(sorts, terms));
[ + - ][ - - ]
1531 : 1 : Term null;
1532 : 1 : terms.push_back(null);
1533 : 1 : ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException);
1534 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
1535 : :
1536 : 4 : TEST_F(TestApiBlackSolver, getModel2)
1537 : : {
1538 : 1 : d_solver->setOption("produce-models", "true");
1539 : 1 : std::vector<Sort> sorts;
1540 : 1 : std::vector<Term> terms;
1541 : 1 : ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException);
1542 [ + - ][ + - ]: 1 : }
1543 : :
1544 : 4 : TEST_F(TestApiBlackSolver, getModel3)
1545 : : {
1546 : 1 : d_solver->setOption("produce-models", "true");
1547 : 1 : std::vector<Sort> sorts;
1548 : 1 : std::vector<Term> terms;
1549 : 1 : d_solver->checkSat();
1550 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getModel(sorts, terms));
[ + - ][ - - ]
1551 : 1 : sorts.push_back(d_int);
1552 : 1 : ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException);
1553 [ + - ][ + - ]: 1 : }
1554 : :
1555 : 4 : TEST_F(TestApiBlackSolver, getQuantifierElimination)
1556 : : {
1557 : 1 : Term x = d_tm.mkVar(d_bool, "x");
1558 : : Term forall =
1559 : 2 : d_tm.mkTerm(Kind::FORALL,
1560 : 1 : {d_tm.mkTerm(Kind::VARIABLE_LIST, {x}),
1561 : 8 : d_tm.mkTerm(Kind::OR, {x, d_tm.mkTerm(Kind::NOT, {x})})});
1562 : 2 : ASSERT_THROW(d_solver->getQuantifierElimination(Term()), CVC5ApiException);
1563 : 2 : ASSERT_THROW(d_solver->getQuantifierElimination(d_tm.mkBoolean(false)),
1564 [ + - ]: 1 : CVC5ApiException);
1565 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getQuantifierElimination(forall));
[ + - ][ - - ]
1566 : :
1567 : 1 : TermManager tm;
1568 : 1 : Solver slv(tm);
1569 : 1 : slv.checkSat();
1570 : 1 : ASSERT_THROW(slv.getQuantifierElimination(forall), CVC5ApiException);
1571 [ + - ][ + - ]: 1 : }
1572 : :
1573 : 4 : TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
1574 : : {
1575 : 1 : Term x = d_tm.mkVar(d_bool, "x");
1576 : : Term forall =
1577 : 2 : d_tm.mkTerm(Kind::FORALL,
1578 : 1 : {d_tm.mkTerm(Kind::VARIABLE_LIST, {x}),
1579 : 8 : d_tm.mkTerm(Kind::OR, {x, d_tm.mkTerm(Kind::NOT, {x})})});
1580 : 2 : ASSERT_THROW(d_solver->getQuantifierEliminationDisjunct(Term()),
1581 [ + - ]: 1 : CVC5ApiException);
1582 : 2 : ASSERT_THROW(
1583 : : d_solver->getQuantifierEliminationDisjunct(d_tm.mkBoolean(false)),
1584 [ + - ]: 1 : CVC5ApiException);
1585 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getQuantifierEliminationDisjunct(forall));
[ + - ][ - - ]
1586 : :
1587 : 1 : TermManager tm;
1588 : 1 : Solver slv(tm);
1589 : 1 : slv.checkSat();
1590 : 1 : ASSERT_THROW(slv.getQuantifierEliminationDisjunct(forall), CVC5ApiException);
1591 [ + - ][ + - ]: 1 : }
1592 : :
1593 : 4 : TEST_F(TestApiBlackSolver, declareSepHeap)
1594 : : {
1595 : 1 : d_solver->setLogic("ALL");
1596 : 1 : d_solver->setOption("incremental", "false");
1597 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSepHeap(d_int, d_int));
[ + - ][ - - ]
1598 : : // cannot declare separation logic heap more than once
1599 : 1 : ASSERT_THROW(d_solver->declareSepHeap(d_int, d_int), CVC5ApiException);
1600 : :
1601 : 1 : TermManager tm;
1602 : : {
1603 : 1 : Solver slv(tm);
1604 : : // no logic set yet
1605 : 3 : ASSERT_THROW(slv.declareSepHeap(tm.getIntegerSort(), tm.getIntegerSort()),
1606 [ + - ]: 1 : CVC5ApiException);
1607 [ + - ]: 1 : }
1608 : : {
1609 : 1 : Solver slv(tm);
1610 : 1 : slv.setLogic("ALL");
1611 : 2 : ASSERT_THROW(slv.declareSepHeap(d_int, tm.getRealSort()), CVC5ApiException);
1612 [ + - ]: 1 : }
1613 : : {
1614 : 1 : Solver slv(tm);
1615 : 1 : slv.setLogic("ALL");
1616 : 2 : ASSERT_THROW(slv.declareSepHeap(tm.getBooleanSort(), d_int),
1617 [ + - ]: 1 : CVC5ApiException);
1618 [ + - ]: 1 : }
1619 : : }
1620 : :
1621 : : namespace {
1622 : : /**
1623 : : * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
1624 : : * some simple separation logic constraints.
1625 : : */
1626 : 4 : void checkSimpleSeparationConstraints(Solver* solver)
1627 : : {
1628 : 4 : TermManager& tm = solver->getTermManager();
1629 : 4 : Sort integer = tm.getIntegerSort();
1630 : : // declare the separation heap
1631 : 4 : solver->declareSepHeap(integer, integer);
1632 : 4 : Term x = tm.mkConst(integer, "x");
1633 : 4 : Term p = tm.mkConst(integer, "p");
1634 : 16 : Term heap = tm.mkTerm(cvc5::Kind::SEP_PTO, {p, x});
1635 : 4 : solver->assertFormula(heap);
1636 : 4 : Term nil = tm.mkSepNil(integer);
1637 : 4 : solver->assertFormula(nil.eqTerm(tm.mkInteger(5)));
1638 : 4 : solver->checkSat();
1639 : 4 : }
1640 : : } // namespace
1641 : :
1642 : 4 : TEST_F(TestApiBlackSolver, getValueSepHeap1)
1643 : : {
1644 : 1 : d_solver->setLogic("QF_BV");
1645 : 1 : d_solver->setOption("incremental", "false");
1646 : 1 : d_solver->setOption("produce-models", "true");
1647 : 1 : Term t = d_tm.mkTrue();
1648 : 1 : d_solver->assertFormula(t);
1649 : 1 : ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException);
1650 [ + - ]: 1 : }
1651 : :
1652 : 4 : TEST_F(TestApiBlackSolver, getValueSepHeap2)
1653 : : {
1654 : 1 : d_solver->setLogic("ALL");
1655 : 1 : d_solver->setOption("incremental", "false");
1656 : 1 : d_solver->setOption("produce-models", "false");
1657 : 1 : checkSimpleSeparationConstraints(d_solver.get());
1658 : 1 : ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException);
1659 : : }
1660 : :
1661 : 4 : TEST_F(TestApiBlackSolver, getValueSepHeap3)
1662 : : {
1663 : 1 : d_solver->setLogic("ALL");
1664 : 1 : d_solver->setOption("incremental", "false");
1665 : 1 : d_solver->setOption("produce-models", "true");
1666 : 1 : Term t = d_tm.mkFalse();
1667 : 1 : d_solver->assertFormula(t);
1668 : 1 : d_solver->checkSat();
1669 : 1 : ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException);
1670 [ + - ]: 1 : }
1671 : :
1672 : 4 : TEST_F(TestApiBlackSolver, getValueSepHeap4)
1673 : : {
1674 : 1 : d_solver->setLogic("ALL");
1675 : 1 : d_solver->setOption("incremental", "false");
1676 : 1 : d_solver->setOption("produce-models", "true");
1677 : 1 : Term t = d_tm.mkTrue();
1678 : 1 : d_solver->assertFormula(t);
1679 : 1 : d_solver->checkSat();
1680 : 1 : ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException);
1681 [ + - ]: 1 : }
1682 : :
1683 : 4 : TEST_F(TestApiBlackSolver, getValueSepHeap5)
1684 : : {
1685 : 1 : d_solver->setLogic("ALL");
1686 : 1 : d_solver->setOption("incremental", "false");
1687 : 1 : d_solver->setOption("produce-models", "true");
1688 : 1 : checkSimpleSeparationConstraints(d_solver.get());
1689 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValueSepHeap());
[ + - ][ - - ]
1690 : : }
1691 : :
1692 : 4 : TEST_F(TestApiBlackSolver, getValueSepNil1)
1693 : : {
1694 : 1 : d_solver->setLogic("QF_BV");
1695 : 1 : d_solver->setOption("incremental", "false");
1696 : 1 : d_solver->setOption("produce-models", "true");
1697 : 1 : Term t = d_tm.mkTrue();
1698 : 1 : d_solver->assertFormula(t);
1699 : 1 : ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException);
1700 [ + - ]: 1 : }
1701 : :
1702 : 4 : TEST_F(TestApiBlackSolver, getValueSepNil2)
1703 : : {
1704 : 1 : d_solver->setLogic("ALL");
1705 : 1 : d_solver->setOption("incremental", "false");
1706 : 1 : d_solver->setOption("produce-models", "false");
1707 : 1 : checkSimpleSeparationConstraints(d_solver.get());
1708 : 1 : ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException);
1709 : : }
1710 : :
1711 : 4 : TEST_F(TestApiBlackSolver, getValueSepNil3)
1712 : : {
1713 : 1 : d_solver->setLogic("ALL");
1714 : 1 : d_solver->setOption("incremental", "false");
1715 : 1 : d_solver->setOption("produce-models", "true");
1716 : 1 : Term t = d_tm.mkFalse();
1717 : 1 : d_solver->assertFormula(t);
1718 : 1 : d_solver->checkSat();
1719 : 1 : ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException);
1720 [ + - ]: 1 : }
1721 : :
1722 : 4 : TEST_F(TestApiBlackSolver, getValueSepNil4)
1723 : : {
1724 : 1 : d_solver->setLogic("ALL");
1725 : 1 : d_solver->setOption("incremental", "false");
1726 : 1 : d_solver->setOption("produce-models", "true");
1727 : 1 : Term t = d_tm.mkTrue();
1728 : 1 : d_solver->assertFormula(t);
1729 : 1 : d_solver->checkSat();
1730 : 1 : ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException);
1731 [ + - ]: 1 : }
1732 : :
1733 : 4 : TEST_F(TestApiBlackSolver, getValueSepNil5)
1734 : : {
1735 : 1 : d_solver->setLogic("ALL");
1736 : 1 : d_solver->setOption("incremental", "false");
1737 : 1 : d_solver->setOption("produce-models", "true");
1738 : 1 : checkSimpleSeparationConstraints(d_solver.get());
1739 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getValueSepNil());
[ + - ][ - - ]
1740 : : }
1741 : :
1742 : 4 : TEST_F(TestApiBlackSolver, push1)
1743 : : {
1744 : 1 : d_solver->setOption("incremental", "true");
1745 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->push(1));
[ + - ][ - - ]
1746 : 5 : ASSERT_THROW(d_solver->setOption("incremental", "false"), CVC5ApiException);
1747 : 5 : ASSERT_THROW(d_solver->setOption("incremental", "true"), CVC5ApiException);
1748 : : }
1749 : :
1750 : 4 : TEST_F(TestApiBlackSolver, push2)
1751 : : {
1752 : 1 : d_solver->setOption("incremental", "false");
1753 : 1 : ASSERT_THROW(d_solver->push(1), CVC5ApiException);
1754 : : }
1755 : :
1756 : 4 : TEST_F(TestApiBlackSolver, pop1)
1757 : : {
1758 : 1 : d_solver->setOption("incremental", "false");
1759 : 1 : ASSERT_THROW(d_solver->pop(1), CVC5ApiException);
1760 : : }
1761 : :
1762 : 4 : TEST_F(TestApiBlackSolver, pop2)
1763 : : {
1764 : 1 : d_solver->setOption("incremental", "true");
1765 : 1 : ASSERT_THROW(d_solver->pop(1), CVC5ApiException);
1766 : : }
1767 : :
1768 : 4 : TEST_F(TestApiBlackSolver, pop3)
1769 : : {
1770 : 1 : d_solver->setOption("incremental", "true");
1771 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->push(1));
[ + - ][ - - ]
1772 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->pop(1));
[ + - ][ - - ]
1773 : 1 : ASSERT_THROW(d_solver->pop(1), CVC5ApiException);
1774 : : }
1775 : :
1776 : 4 : TEST_F(TestApiBlackSolver, blockModel1)
1777 : : {
1778 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1779 : 1 : d_solver->assertFormula(x.eqTerm(x));
1780 : 1 : d_solver->checkSat();
1781 : 1 : ASSERT_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS),
1782 [ + - ]: 1 : CVC5ApiException);
1783 [ + - ]: 1 : }
1784 : :
1785 : 4 : TEST_F(TestApiBlackSolver, blockModel2)
1786 : : {
1787 : 1 : d_solver->setOption("produce-models", "true");
1788 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1789 : 1 : d_solver->assertFormula(x.eqTerm(x));
1790 : 1 : ASSERT_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS),
1791 [ + - ]: 1 : CVC5ApiException);
1792 [ + - ]: 1 : }
1793 : :
1794 : 4 : TEST_F(TestApiBlackSolver, blockModel3)
1795 : : {
1796 : 1 : d_solver->setOption("produce-models", "true");
1797 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1798 : 1 : d_solver->assertFormula(x.eqTerm(x));
1799 : 1 : d_solver->checkSat();
1800 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS));
[ + - ][ - - ]
1801 [ + - ]: 1 : }
1802 : :
1803 : 4 : TEST_F(TestApiBlackSolver, blockModelValues1)
1804 : : {
1805 : 1 : d_solver->setOption("produce-models", "true");
1806 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1807 : 1 : d_solver->assertFormula(x.eqTerm(x));
1808 : 1 : d_solver->checkSat();
1809 : 2 : ASSERT_THROW(d_solver->blockModelValues({}), CVC5ApiException);
1810 : 5 : ASSERT_THROW(d_solver->blockModelValues({Term()}), CVC5ApiException);
1811 : 2 : ASSERT_NO_THROW(d_solver->blockModelValues({d_tm.mkBoolean(false)}));
1812 : :
1813 : 1 : TermManager tm;
1814 : 1 : Solver slv(tm);
1815 : 1 : slv.setOption("produce-models", "true");
1816 : 1 : slv.checkSat();
1817 : 5 : ASSERT_THROW(slv.blockModelValues({d_tm.mkFalse()}), CVC5ApiException);
1818 [ + - ]: 1 : }
1819 : :
1820 : 4 : TEST_F(TestApiBlackSolver, blockModelValues2)
1821 : : {
1822 : 1 : d_solver->setOption("produce-models", "true");
1823 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1824 : 1 : d_solver->assertFormula(x.eqTerm(x));
1825 : 1 : d_solver->checkSat();
1826 : 2 : ASSERT_NO_THROW(d_solver->blockModelValues({x}));
1827 [ + - ]: 1 : }
1828 : :
1829 : 4 : TEST_F(TestApiBlackSolver, blockModelValues3)
1830 : : {
1831 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1832 : 1 : d_solver->assertFormula(x.eqTerm(x));
1833 : 1 : d_solver->checkSat();
1834 : 5 : ASSERT_THROW(d_solver->blockModelValues({x}), CVC5ApiException);
1835 [ + - ]: 1 : }
1836 : :
1837 : 4 : TEST_F(TestApiBlackSolver, blockModelValues4)
1838 : : {
1839 : 1 : d_solver->setOption("produce-models", "true");
1840 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1841 : 1 : d_solver->assertFormula(x.eqTerm(x));
1842 : 5 : ASSERT_THROW(d_solver->blockModelValues({x}), CVC5ApiException);
1843 [ + - ]: 1 : }
1844 : :
1845 : 4 : TEST_F(TestApiBlackSolver, blockModelValues5)
1846 : : {
1847 : 1 : d_solver->setOption("produce-models", "true");
1848 : 1 : Term x = d_tm.mkConst(d_bool, "x");
1849 : 1 : d_solver->assertFormula(x.eqTerm(x));
1850 : 1 : d_solver->checkSat();
1851 : 2 : ASSERT_NO_THROW(d_solver->blockModelValues({x}));
1852 [ + - ]: 1 : }
1853 : :
1854 : 4 : TEST_F(TestApiBlackSolver, getInstantiations)
1855 : : {
1856 : 3 : Term p = d_solver->declareFun("p", {d_int}, d_bool);
1857 : 1 : Term x = d_tm.mkVar(d_int, "x");
1858 : 3 : Term bvl = d_tm.mkTerm(Kind::VARIABLE_LIST, {x});
1859 : 4 : Term app = d_tm.mkTerm(Kind::APPLY_UF, {p, x});
1860 : 4 : Term q = d_tm.mkTerm(Kind::FORALL, {bvl, app});
1861 : 1 : d_solver->assertFormula(q);
1862 : 1 : Term five = d_tm.mkInteger(5);
1863 : 6 : Term app2 = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::APPLY_UF, {p, five})});
1864 : 1 : d_solver->assertFormula(app2);
1865 : 1 : ASSERT_THROW(d_solver->getInstantiations(), CVC5ApiException);
1866 : 1 : d_solver->checkSat();
1867 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getInstantiations());
[ + - ][ - - ]
1868 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1869 : :
1870 : 4 : TEST_F(TestApiBlackSolver, setInfo)
1871 : : {
1872 : 5 : ASSERT_THROW(d_solver->setInfo("cvc5-lagic", "QF_BV"), CVC5ApiException);
1873 : 5 : ASSERT_THROW(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC5ApiException);
1874 : 5 : ASSERT_THROW(d_solver->setInfo("cvc5-logic", "asdf"), CVC5ApiException);
1875 : :
1876 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("source", "asdf"));
[ + - ][ - - ]
1877 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("category", "asdf"));
[ + - ][ - - ]
1878 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("difficulty", "asdf"));
[ + - ][ - - ]
1879 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("filename", "asdf"));
[ + - ][ - - ]
1880 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("license", "asdf"));
[ + - ][ - - ]
1881 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("name", "asdf"));
[ + - ][ - - ]
1882 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("notes", "asdf"));
[ + - ][ - - ]
1883 : :
1884 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2"));
[ + - ][ - - ]
1885 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.0"));
[ + - ][ - - ]
1886 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.5"));
[ + - ][ - - ]
1887 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.6"));
[ + - ][ - - ]
1888 : 5 : ASSERT_THROW(d_solver->setInfo("smt-lib-version", ".0"), CVC5ApiException);
1889 : :
1890 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("status", "sat"));
[ + - ][ - - ]
1891 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("status", "unsat"));
[ + - ][ - - ]
1892 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setInfo("status", "unknown"));
[ + - ][ - - ]
1893 : 5 : ASSERT_THROW(d_solver->setInfo("status", "asdf"), CVC5ApiException);
1894 : : }
1895 : :
1896 : 4 : TEST_F(TestApiBlackSolver, setLogic)
1897 : : {
1898 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setLogic("AUFLIRA"));
[ + - ][ - - ]
1899 : 3 : ASSERT_THROW(d_solver->setLogic("AF_BV"), CVC5ApiException);
1900 : 1 : d_solver->assertFormula(d_tm.mkTrue());
1901 : 3 : ASSERT_THROW(d_solver->setLogic("AUFLIRA"), CVC5ApiException);
1902 : : }
1903 : :
1904 : 4 : TEST_F(TestApiBlackSolver, isLogicSet)
1905 : : {
1906 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_solver->isLogicSet());
1907 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setLogic("QF_BV"));
[ + - ][ - - ]
1908 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->isLogicSet());
1909 : : }
1910 : :
1911 : 4 : TEST_F(TestApiBlackSolver, getLogic)
1912 : : {
1913 : 1 : ASSERT_THROW(d_solver->getLogic(), CVC5ApiException);
1914 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setLogic("QF_BV"));
[ + - ][ - - ]
1915 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getLogic(), "QF_BV");
1916 : : }
1917 : :
1918 : 4 : TEST_F(TestApiBlackSolver, setOption)
1919 : : {
1920 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->setOption("bv-sat-solver", "cadical"));
[ + - ][ - - ]
1921 : 5 : ASSERT_THROW(d_solver->setOption("bv-sat-solver", "1"), CVC5ApiException);
1922 : 1 : d_solver->assertFormula(d_tm.mkTrue());
1923 : 5 : ASSERT_THROW(d_solver->setOption("bv-sat-solver", "cadical"),
1924 [ + - ]: 1 : CVC5ApiException);
1925 : : }
1926 : :
1927 : 4 : TEST_F(TestApiBlackSolver, resetAssertions)
1928 : : {
1929 : 1 : d_solver->setOption("incremental", "true");
1930 : :
1931 : 1 : Sort bvSort = d_tm.mkBitVectorSort(4);
1932 : 1 : Term one = d_tm.mkBitVector(4, 1);
1933 : 1 : Term x = d_tm.mkConst(bvSort, "x");
1934 : 4 : Term ule = d_tm.mkTerm(Kind::BITVECTOR_ULE, {x, one});
1935 : 4 : Term srem = d_tm.mkTerm(Kind::BITVECTOR_SREM, {one, x});
1936 : 1 : d_solver->push(4);
1937 : 4 : Term slt = d_tm.mkTerm(Kind::BITVECTOR_SLT, {srem, one});
1938 : 1 : d_solver->resetAssertions();
1939 [ + + ][ - - ]: 3 : d_solver->checkSatAssuming({slt, ule});
1940 : 1 : }
1941 : :
1942 : 4 : TEST_F(TestApiBlackSolver, declareSygusVar)
1943 : : {
1944 : 1 : d_solver->setOption("sygus", "true");
1945 : 3 : Sort funSort = d_tm.mkFunctionSort({d_int}, d_bool);
1946 : :
1947 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSygusVar("", d_bool));
[ + - ][ - - ]
1948 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSygusVar("", funSort));
[ + - ][ - - ]
1949 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->declareSygusVar(std::string("b"), d_bool));
[ + - ][ - - ]
1950 : 4 : ASSERT_THROW(d_solver->declareSygusVar("", Sort()), CVC5ApiException);
1951 : 4 : ASSERT_THROW(d_solver->declareSygusVar("a", Sort()), CVC5ApiException);
1952 : :
1953 : 4 : ASSERT_THROW(Solver(d_tm).declareSygusVar("", d_bool), CVC5ApiException);
1954 : :
1955 : 1 : TermManager tm;
1956 : 1 : Solver slv(tm);
1957 : 1 : slv.setOption("sygus", "true");
1958 : 3 : ASSERT_THROW(slv.declareSygusVar("", d_bool), CVC5ApiException);
1959 [ + - ]: 1 : }
1960 : :
1961 : 4 : TEST_F(TestApiBlackSolver, mkGrammar)
1962 : : {
1963 : 1 : Term nullTerm;
1964 : 1 : Term boolTerm = d_tm.mkBoolean(true);
1965 : 1 : Term boolVar = d_tm.mkVar(d_bool);
1966 : 1 : Term intVar = d_tm.mkVar(d_int);
1967 : :
1968 : 2 : ASSERT_NO_THROW(d_solver->mkGrammar({}, {intVar}));
1969 : 3 : ASSERT_NO_THROW(d_solver->mkGrammar({boolVar}, {intVar}));
1970 : 3 : ASSERT_THROW(d_solver->mkGrammar({}, {}), CVC5ApiException);
1971 : 6 : ASSERT_THROW(d_solver->mkGrammar({}, {nullTerm}), CVC5ApiException);
1972 : 6 : ASSERT_THROW(d_solver->mkGrammar({}, {boolTerm}), CVC5ApiException);
1973 : 9 : ASSERT_THROW(d_solver->mkGrammar({boolTerm}, {intVar}), CVC5ApiException);
1974 : :
1975 : 1 : TermManager tm;
1976 : 1 : Solver slv(tm);
1977 : 2 : Term boolVar2 = tm.mkVar(tm.getBooleanSort());
1978 : 2 : Term intVar2 = tm.mkVar(tm.getIntegerSort());
1979 : 3 : ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar2}));
1980 : 9 : ASSERT_THROW(slv.mkGrammar({boolVar}, {intVar2}), CVC5ApiException);
1981 : 9 : ASSERT_THROW(slv.mkGrammar({boolVar2}, {intVar}), CVC5ApiException);
1982 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1983 : :
1984 : 4 : TEST_F(TestApiBlackSolver, synthFun)
1985 : : {
1986 : 1 : d_solver->setOption("sygus", "true");
1987 : 1 : Sort null;
1988 : :
1989 : 1 : Term nullTerm;
1990 : 1 : Term x = d_tm.mkVar(d_bool);
1991 : :
1992 : 1 : Term start1 = d_tm.mkVar(d_bool);
1993 : 1 : Term start2 = d_tm.mkVar(d_int);
1994 : :
1995 : 5 : Grammar g1 = d_solver->mkGrammar({x}, {start1});
1996 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->synthFun("", {}, d_bool));
[ + - ][ - - ]
1997 : 2 : ASSERT_NO_THROW(d_solver->synthFun("f1", {x}, d_bool));
1998 : 8 : ASSERT_THROW(d_solver->synthFun("f2", {x}, d_bool, g1), CVC5ApiException);
1999 : 1 : g1.addRule(start1, d_tm.mkBoolean(false));
2000 : :
2001 : 5 : Grammar g2 = d_solver->mkGrammar({x}, {start2});
2002 : 1 : g2.addRule(start2, d_tm.mkInteger(0));
2003 : :
2004 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->synthFun("", {}, d_bool));
[ + - ][ - - ]
2005 : 2 : ASSERT_NO_THROW(d_solver->synthFun("f1", {x}, d_bool));
2006 : 2 : ASSERT_NO_THROW(d_solver->synthFun("f2", {x}, d_bool, g1));
2007 : :
2008 : 7 : ASSERT_THROW(d_solver->synthFun("f3", {nullTerm}, d_bool), CVC5ApiException);
2009 : 4 : ASSERT_THROW(d_solver->synthFun("f4", {}, null), CVC5ApiException);
2010 : 8 : ASSERT_THROW(d_solver->synthFun("f6", {x}, d_bool, g2), CVC5ApiException);
2011 : :
2012 : 1 : TermManager tm;
2013 : 1 : Solver slv(tm);
2014 : 1 : slv.setOption("sygus", "true");
2015 : 2 : Term x2 = tm.mkVar(tm.getBooleanSort());
2016 : 7 : ASSERT_THROW(slv.synthFun("f1", {x2}, d_bool), CVC5ApiException);
2017 : 4 : ASSERT_THROW(slv.synthFun("", {}, d_bool), CVC5ApiException);
2018 : 8 : ASSERT_THROW(slv.synthFun("f1", {x}, tm.getBooleanSort()), CVC5ApiException);
2019 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
2020 : :
2021 : 4 : TEST_F(TestApiBlackSolver, addSygusConstraint)
2022 : : {
2023 : 1 : d_solver->setOption("sygus", "true");
2024 : 1 : Term nullTerm;
2025 : 1 : Term boolTerm = d_tm.mkBoolean(true);
2026 : 1 : Term intTerm = d_tm.mkInteger(1);
2027 : :
2028 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->addSygusConstraint(boolTerm));
[ + - ][ - - ]
2029 : 1 : ASSERT_THROW(d_solver->addSygusConstraint(nullTerm), CVC5ApiException);
2030 : 1 : ASSERT_THROW(d_solver->addSygusConstraint(intTerm), CVC5ApiException);
2031 : :
2032 : 1 : TermManager tm;
2033 : 1 : Solver slv(tm);
2034 : 1 : slv.setOption("sygus", "true");
2035 : 1 : ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException);
2036 [ + - ][ + - ]: 1 : }
[ + - ]
2037 : :
2038 : 4 : TEST_F(TestApiBlackSolver, getSygusConstraints)
2039 : : {
2040 : 1 : d_solver->setOption("sygus", "true");
2041 : 1 : Term trueTerm = d_tm.mkBoolean(true);
2042 : 1 : Term falseTerm = d_tm.mkBoolean(false);
2043 : 1 : d_solver->addSygusConstraint(trueTerm);
2044 : 1 : d_solver->addSygusConstraint(falseTerm);
2045 : 4 : std::vector<Term> constraints{trueTerm, falseTerm};
2046 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getSygusConstraints(), constraints);
2047 [ + - ][ + - ]: 1 : }
[ + - ]
2048 : :
2049 : 4 : TEST_F(TestApiBlackSolver, addSygusAssume)
2050 : : {
2051 : 1 : d_solver->setOption("sygus", "true");
2052 : 1 : Term nullTerm;
2053 : 1 : Term boolTerm = d_tm.mkBoolean(false);
2054 : 1 : Term intTerm = d_tm.mkInteger(1);
2055 : :
2056 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->addSygusAssume(boolTerm));
[ + - ][ - - ]
2057 : 1 : ASSERT_THROW(d_solver->addSygusAssume(nullTerm), CVC5ApiException);
2058 : 1 : ASSERT_THROW(d_solver->addSygusAssume(intTerm), CVC5ApiException);
2059 : :
2060 : 1 : TermManager tm;
2061 : 1 : Solver slv(tm);
2062 : 1 : slv.setOption("sygus", "true");
2063 : 1 : ASSERT_THROW(slv.addSygusAssume(boolTerm), CVC5ApiException);
2064 [ + - ][ + - ]: 1 : }
[ + - ]
2065 : :
2066 : 4 : TEST_F(TestApiBlackSolver, getSygusAssumptions)
2067 : : {
2068 : 1 : d_solver->setOption("sygus", "true");
2069 : 1 : Term trueTerm = d_tm.mkBoolean(true);
2070 : 1 : Term falseTerm = d_tm.mkBoolean(false);
2071 : 1 : d_solver->addSygusAssume(trueTerm);
2072 : 1 : d_solver->addSygusAssume(falseTerm);
2073 : 4 : std::vector<Term> assumptions{trueTerm, falseTerm};
2074 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getSygusAssumptions(), assumptions);
2075 [ + - ][ + - ]: 1 : }
[ + - ]
2076 : :
2077 : 4 : TEST_F(TestApiBlackSolver, addSygusInvConstraint)
2078 : : {
2079 : 1 : d_solver->setOption("sygus", "true");
2080 : :
2081 : 1 : Term nullTerm;
2082 : 1 : Term intTerm = d_tm.mkInteger(1);
2083 : :
2084 : 3 : Term inv = d_solver->declareFun("inv", {d_real}, d_bool);
2085 : 3 : Term pre = d_solver->declareFun("pre", {d_real}, d_bool);
2086 : 4 : Term trans = d_solver->declareFun("trans", {d_real, d_real}, d_bool);
2087 : 3 : Term post = d_solver->declareFun("post", {d_real}, d_bool);
2088 : :
2089 : 3 : Term inv1 = d_solver->declareFun("inv1", {d_real}, d_real);
2090 : :
2091 : 4 : Term trans1 = d_solver->declareFun("trans1", {d_bool, d_real}, d_bool);
2092 : 4 : Term trans2 = d_solver->declareFun("trans2", {d_real, d_bool}, d_bool);
2093 : 4 : Term trans3 = d_solver->declareFun("trans3", {d_real, d_real}, d_real);
2094 : :
2095 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, post));
[ + - ][ - - ]
2096 : :
2097 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(nullTerm, pre, trans, post),
2098 [ + - ]: 1 : CVC5ApiException);
2099 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, nullTerm, trans, post),
2100 [ + - ]: 1 : CVC5ApiException);
2101 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, nullTerm, post),
2102 [ + - ]: 1 : CVC5ApiException);
2103 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, nullTerm),
2104 [ + - ]: 1 : CVC5ApiException);
2105 : :
2106 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(intTerm, pre, trans, post),
2107 [ + - ]: 1 : CVC5ApiException);
2108 : :
2109 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv1, pre, trans, post),
2110 [ + - ]: 1 : CVC5ApiException);
2111 : :
2112 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, trans, trans, post),
2113 [ + - ]: 1 : CVC5ApiException);
2114 : :
2115 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, intTerm, post),
2116 [ + - ]: 1 : CVC5ApiException);
2117 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, pre, post),
2118 [ + - ]: 1 : CVC5ApiException);
2119 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans1, post),
2120 [ + - ]: 1 : CVC5ApiException);
2121 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans2, post),
2122 [ + - ]: 1 : CVC5ApiException);
2123 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans3, post),
2124 [ + - ]: 1 : CVC5ApiException);
2125 : :
2126 : 1 : ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, trans),
2127 [ + - ]: 1 : CVC5ApiException);
2128 : :
2129 : 1 : TermManager tm;
2130 : 1 : Solver slv(tm);
2131 : 1 : slv.setOption("sygus", "true");
2132 : 1 : Sort boolean2 = tm.getBooleanSort();
2133 : 1 : Sort real2 = tm.getRealSort();
2134 : 3 : Term inv22 = slv.declareFun("inv", {real2}, boolean2);
2135 : 3 : Term pre22 = slv.declareFun("pre", {real2}, boolean2);
2136 : 4 : Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
2137 : 3 : Term post22 = slv.declareFun("post", {real2}, boolean2);
2138 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
[ + - ][ - - ]
2139 : 1 : ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
2140 [ + - ]: 1 : CVC5ApiException);
2141 : 1 : ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
2142 [ + - ]: 1 : CVC5ApiException);
2143 : 1 : ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
2144 [ + - ]: 1 : CVC5ApiException);
2145 : 1 : ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
2146 [ + - ]: 1 : CVC5ApiException);
2147 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2148 : :
2149 : 4 : TEST_F(TestApiBlackSolver, checkSynth)
2150 : : {
2151 : : // requires option to be set
2152 : 1 : ASSERT_THROW(d_solver->checkSynth(), CVC5ApiException);
2153 : 1 : d_solver->setOption("sygus", "true");
2154 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->checkSynth());
[ + - ][ - - ]
2155 : : }
2156 : :
2157 : 4 : TEST_F(TestApiBlackSolver, getSynthSolution)
2158 : : {
2159 : 1 : d_solver->setOption("sygus", "true");
2160 : 1 : d_solver->setOption("incremental", "false");
2161 : :
2162 : 1 : Term nullTerm;
2163 : 1 : Term x = d_tm.mkBoolean(false);
2164 : 2 : Term f = d_solver->synthFun("f", {}, d_bool);
2165 : :
2166 : 1 : ASSERT_THROW(d_solver->getSynthSolution(f), CVC5ApiException);
2167 : :
2168 : 1 : cvc5::SynthResult sr = d_solver->checkSynth();
2169 [ - + ][ + - ]: 1 : ASSERT_TRUE(sr.hasSolution());
2170 : :
2171 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getSynthSolution(f));
[ + - ][ - - ]
2172 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_solver->getSynthSolution(f));
[ + - ][ - - ]
2173 : :
2174 : 1 : ASSERT_THROW(d_solver->getSynthSolution(nullTerm), CVC5ApiException);
2175 : 1 : ASSERT_THROW(d_solver->getSynthSolution(x), CVC5ApiException);
2176 : :
2177 : 2 : ASSERT_THROW(Solver(d_tm).getSynthSolution(f), CVC5ApiException);
2178 [ + - ][ + - ]: 1 : }
[ + - ]
2179 : :
2180 : 4 : TEST_F(TestApiBlackSolver, getSynthSolutions)
2181 : : {
2182 : 1 : d_solver->setOption("sygus", "true");
2183 : 1 : d_solver->setOption("incremental", "false");
2184 : :
2185 : 1 : Term nullTerm;
2186 : 1 : Term x = d_tm.mkBoolean(false);
2187 : 2 : Term f = d_solver->synthFun("f", {}, d_bool);
2188 : :
2189 : 2 : ASSERT_THROW(d_solver->getSynthSolutions({}), CVC5ApiException);
2190 : 5 : ASSERT_THROW(d_solver->getSynthSolutions({f}), CVC5ApiException);
2191 : :
2192 : 1 : d_solver->checkSynth();
2193 : :
2194 : 2 : ASSERT_NO_THROW(d_solver->getSynthSolutions({f}));
2195 : 3 : ASSERT_NO_THROW(d_solver->getSynthSolutions({f, f}));
2196 : :
2197 : 2 : ASSERT_THROW(d_solver->getSynthSolutions({}), CVC5ApiException);
2198 : 5 : ASSERT_THROW(d_solver->getSynthSolutions({nullTerm}), CVC5ApiException);
2199 : 5 : ASSERT_THROW(d_solver->getSynthSolutions({x}), CVC5ApiException);
2200 : :
2201 : 6 : ASSERT_THROW(Solver(d_tm).getSynthSolutions({x}), CVC5ApiException);
2202 [ + - ][ + - ]: 1 : }
[ + - ]
2203 : :
2204 : 4 : TEST_F(TestApiBlackSolver, checkSynthNext)
2205 : : {
2206 : 1 : d_solver->setOption("sygus", "true");
2207 : 1 : d_solver->setOption("incremental", "true");
2208 : 2 : Term f = d_solver->synthFun("f", {}, d_bool);
2209 : :
2210 : 1 : cvc5::SynthResult sr = d_solver->checkSynth();
2211 [ - + ][ + - ]: 1 : ASSERT_TRUE(sr.hasSolution());
2212 : 2 : ASSERT_NO_THROW(d_solver->getSynthSolutions({f}));
2213 : 1 : sr = d_solver->checkSynthNext();
2214 [ - + ][ + - ]: 1 : ASSERT_TRUE(sr.hasSolution());
2215 : 2 : ASSERT_NO_THROW(d_solver->getSynthSolutions({f}));
2216 [ + - ][ + - ]: 1 : }
2217 : :
2218 : 4 : TEST_F(TestApiBlackSolver, checkSynthNext2)
2219 : : {
2220 : 1 : d_solver->setOption("sygus", "true");
2221 : 1 : d_solver->setOption("incremental", "false");
2222 : 1 : (void)d_solver->synthFun("f", {}, d_bool);
2223 : 1 : d_solver->checkSynth();
2224 : 1 : ASSERT_THROW(d_solver->checkSynthNext(), CVC5ApiException);
2225 : : }
2226 : :
2227 : 4 : TEST_F(TestApiBlackSolver, checkSynthNext3)
2228 : : {
2229 : 1 : d_solver->setOption("sygus", "true");
2230 : 1 : d_solver->setOption("incremental", "true");
2231 : 1 : (void)d_solver->synthFun("f", {}, d_bool);
2232 : 1 : ASSERT_THROW(d_solver->checkSynthNext(), CVC5ApiException);
2233 : : }
2234 : :
2235 : 4 : TEST_F(TestApiBlackSolver, findSynth)
2236 : : {
2237 : 1 : d_solver->setOption("sygus", "true");
2238 : 1 : Term start = d_tm.mkVar(d_bool);
2239 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
2240 : 5 : ASSERT_THROW(d_solver->synthFun("f", {}, d_bool, g), CVC5ApiException);
2241 : :
2242 : 1 : Term truen = d_tm.mkBoolean(true);
2243 : 1 : Term falsen = d_tm.mkBoolean(false);
2244 : 1 : g.addRule(start, truen);
2245 : 1 : g.addRule(start, falsen);
2246 : 1 : (void)d_solver->synthFun("f", {}, d_bool, g);
2247 : :
2248 : : // should enumerate based on the grammar of the function to synthesize above
2249 : 1 : cvc5::Term t = d_solver->findSynth(modes::FindSynthTarget::ENUM);
2250 [ + - ][ + - ]: 2 : ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean());
[ + - ][ - + ]
[ + - ][ - - ]
2251 [ + - ][ + - ]: 1 : }
2252 : :
2253 : 4 : TEST_F(TestApiBlackSolver, findSynth2)
2254 : : {
2255 : 1 : d_solver->setOption("sygus", "true");
2256 : 1 : d_solver->setOption("incremental", "true");
2257 : 1 : Term start = d_tm.mkVar(d_bool);
2258 : 3 : Grammar g = d_solver->mkGrammar({}, {start});
2259 : 1 : Term truen = d_tm.mkBoolean(true);
2260 : 1 : Term falsen = d_tm.mkBoolean(false);
2261 : 1 : g.addRule(start, truen);
2262 : 1 : g.addRule(start, falsen);
2263 : :
2264 : : // should enumerate true/false
2265 : 1 : cvc5::Term t = d_solver->findSynth(modes::FindSynthTarget::ENUM, g);
2266 [ + - ][ + - ]: 2 : ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean());
[ + - ][ - + ]
[ + - ][ - - ]
2267 : 1 : t = d_solver->findSynthNext();
2268 [ + - ][ + - ]: 2 : ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean());
[ + - ][ - + ]
[ + - ][ - - ]
2269 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
2270 : :
2271 : 4 : TEST_F(TestApiBlackSolver, tupleProject)
2272 : : {
2273 : : std::vector<Term> elements = {
2274 : : d_tm.mkBoolean(true),
2275 : : d_tm.mkInteger(3),
2276 : : d_tm.mkString("C"),
2277 : 9 : d_tm.mkTerm(Kind::SET_SINGLETON, {d_tm.mkString("Z")})};
2278 : :
2279 : 1 : Term tuple = d_tm.mkTuple(elements);
2280 : :
2281 : 1 : std::vector<uint32_t> indices1 = {};
2282 : 1 : std::vector<uint32_t> indices2 = {0};
2283 : 1 : std::vector<uint32_t> indices3 = {0, 1};
2284 : 1 : std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
2285 : 1 : std::vector<uint32_t> indices5 = {4};
2286 : 1 : std::vector<uint32_t> indices6 = {0, 4};
2287 : :
2288 : 2 : ASSERT_NO_THROW(
2289 [ + - ]: 1 : d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices1), {tuple}));
2290 : 2 : ASSERT_NO_THROW(
2291 [ + - ]: 1 : d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices2), {tuple}));
2292 : 2 : ASSERT_NO_THROW(
2293 [ + - ]: 1 : d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices3), {tuple}));
2294 : 2 : ASSERT_NO_THROW(
2295 [ + - ]: 1 : d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices4), {tuple}));
2296 : :
2297 : 6 : ASSERT_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices5), {tuple}),
2298 [ + - ]: 1 : CVC5ApiException);
2299 : 6 : ASSERT_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices6), {tuple}),
2300 [ + - ]: 1 : CVC5ApiException);
2301 : :
2302 : 1 : std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
2303 : :
2304 : 1 : Op op = d_tm.mkOp(Kind::TUPLE_PROJECT, indices);
2305 : 3 : Term projection = d_tm.mkTerm(op, {tuple});
2306 : :
2307 : 1 : Datatype datatype = tuple.getSort().getDatatype();
2308 : 1 : DatatypeConstructor constructor = datatype[0];
2309 : :
2310 [ + + ]: 7 : for (size_t i = 0; i < indices.size(); i++)
2311 : : {
2312 : 6 : Term selectorTerm = constructor[indices[i]].getTerm();
2313 : : Term selectedTerm =
2314 : 24 : d_tm.mkTerm(Kind::APPLY_SELECTOR, {selectorTerm, tuple});
2315 : 6 : Term simplifiedTerm = d_solver->simplify(selectedTerm);
2316 [ - + ][ + - ]: 6 : ASSERT_EQ(elements[indices[i]], simplifiedTerm);
2317 [ + - ][ + - ]: 6 : }
[ + - ]
2318 : :
2319 [ - + ]: 2 : ASSERT_EQ(
2320 : : "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton "
2321 : : "\"Z\")))",
2322 [ + - ]: 1 : projection.toString());
2323 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2324 : :
2325 : 4 : TEST_F(TestApiBlackSolver, output)
2326 : : {
2327 : 3 : ASSERT_THROW(d_solver->isOutputOn("foo-invalid"), CVC5ApiException);
2328 : 3 : ASSERT_THROW(d_solver->getOutput("foo-invalid"), CVC5ApiException);
2329 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_solver->isOutputOn("inst"));
2330 [ - + ][ + - ]: 1 : ASSERT_EQ(null_os.rdbuf(), d_solver->getOutput("inst").rdbuf());
2331 : 1 : d_solver->setOption("output", "inst");
2332 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->isOutputOn("inst"));
2333 [ - + ][ + - ]: 1 : ASSERT_NE(null_os.rdbuf(), d_solver->getOutput("inst").rdbuf());
2334 : : }
2335 : :
2336 : 4 : TEST_F(TestApiBlackSolver, getDatatypeArity)
2337 : : {
2338 : 2 : DatatypeConstructorDecl ctor1 = d_tm.mkDatatypeConstructorDecl("_x21");
2339 : 2 : DatatypeConstructorDecl ctor2 = d_tm.mkDatatypeConstructorDecl("_x31");
2340 : 4 : Sort s3 = d_solver->declareDatatype(std::string("_x17"), {ctor1, ctor2});
2341 [ - + ][ + - ]: 1 : ASSERT_EQ(s3.getDatatypeArity(), 0);
2342 [ + - ][ + - ]: 1 : }
[ + - ]
2343 : :
2344 : 4 : TEST_F(TestApiBlackSolver, declareOracleFunError)
2345 : : {
2346 : : // cannot declare without option
2347 : 8 : ASSERT_THROW(d_solver->declareOracleFun(
2348 : : "f",
2349 : : {d_int},
2350 : : d_int,
2351 : : [&](const std::vector<Term>&) { return d_tm.mkInteger(0); });
2352 [ + - ]: 1 : , CVC5ApiException);
2353 : 1 : d_solver->setOption("oracles", "true");
2354 : 1 : Sort nullSort;
2355 : : // bad sort
2356 : 8 : ASSERT_THROW(d_solver->declareOracleFun(
2357 : : "f",
2358 : : {nullSort},
2359 : : d_int,
2360 : : [&](const std::vector<Term>&) { return d_tm.mkInteger(0); });
2361 [ + - ]: 1 : , CVC5ApiException);
2362 : : }
2363 : :
2364 : 4 : TEST_F(TestApiBlackSolver, declareOracleFunUnsat)
2365 : : {
2366 : 1 : d_solver->setOption("oracles", "true");
2367 : : // f is the function implementing (lambda ((x Int)) (+ x 1))
2368 : 1 : Term f = d_solver->declareOracleFun(
2369 : 2 : "f", {d_int}, d_int, [&](const std::vector<Term>& input) {
2370 [ + - ]: 1 : if (input[0].isUInt32Value())
2371 : : {
2372 : 1 : return d_tm.mkInteger(input[0].getUInt32Value() + 1);
2373 : : }
2374 : 0 : return d_tm.mkInteger(0);
2375 : 3 : });
2376 : 1 : Term three = d_tm.mkInteger(3);
2377 : 1 : Term five = d_tm.mkInteger(5);
2378 : : Term eq =
2379 : 7 : d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::APPLY_UF, {f, three}), five});
2380 : 1 : d_solver->assertFormula(eq);
2381 : : // (f 3) = 5
2382 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
2383 : :
2384 : 1 : TermManager tm;
2385 : 1 : Solver slv(tm);
2386 : 1 : slv.setOption("oracles", "true");
2387 : 1 : Sort iiSort = tm.getIntegerSort();
2388 [ - - ]: 8 : ASSERT_THROW(slv.declareOracleFun("f",
2389 : : {iiSort},
2390 : : d_int,
2391 : : [&](const std::vector<Term>& input) {
2392 : : if (input[0].isUInt32Value())
2393 : : {
2394 : : return tm.mkInteger(
2395 : : input[0].getUInt32Value() + 1);
2396 : : }
2397 : : return tm.mkInteger(0);
2398 : : }),
2399 [ + - ]: 1 : CVC5ApiException);
2400 [ - - ]: 8 : ASSERT_THROW(slv.declareOracleFun("f",
2401 : : {d_int},
2402 : : iiSort,
2403 : : [&](const std::vector<Term>& input) {
2404 : : if (input[0].isUInt32Value())
2405 : : {
2406 : : return tm.mkInteger(
2407 : : input[0].getUInt32Value() + 1);
2408 : : }
2409 : : return tm.mkInteger(0);
2410 : : }),
2411 [ + - ]: 1 : CVC5ApiException);
2412 : : // this cannot be caught during declaration, is caught during check-sat
2413 : 1 : Term f2 = slv.declareOracleFun(
2414 : 1 : "f2", {iiSort}, iiSort, [&](const std::vector<Term>& input) {
2415 [ + - ]: 1 : if (input[0].isUInt32Value())
2416 : : {
2417 : 1 : return d_tm.mkInteger(input[0].getUInt32Value() + 1);
2418 : : }
2419 : 0 : return d_tm.mkInteger(0);
2420 : 3 : });
2421 : 2 : Term eq2 = tm.mkTerm(
2422 : : Kind::EQUAL,
2423 : 5 : {tm.mkTerm(Kind::APPLY_UF, {f2, tm.mkInteger(3)}), tm.mkInteger(5)});
2424 : 1 : slv.assertFormula(eq2);
2425 : 1 : ASSERT_THROW(slv.checkSat(), CVC5ApiException);
2426 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
2427 : :
2428 : 4 : TEST_F(TestApiBlackSolver, declareOracleFunSat)
2429 : : {
2430 : 1 : d_solver->setOption("oracles", "true");
2431 : 1 : d_solver->setOption("produce-models", "true");
2432 : : // f is the function implementing (lambda ((x Int)) (% x 10))
2433 : 1 : Term f = d_solver->declareOracleFun(
2434 : 9 : "f", {d_int}, d_int, [&](const std::vector<Term>& input) {
2435 [ + - ]: 8 : if (input[0].isUInt32Value())
2436 : : {
2437 : 8 : return d_tm.mkInteger(input[0].getUInt32Value() % 10);
2438 : : }
2439 : 0 : return d_tm.mkInteger(0);
2440 : 3 : });
2441 : 1 : Term seven = d_tm.mkInteger(7);
2442 : 1 : Term x = d_tm.mkConst(d_int, "x");
2443 : 4 : Term lb = d_tm.mkTerm(Kind::GEQ, {x, d_tm.mkInteger(0)});
2444 : 1 : d_solver->assertFormula(lb);
2445 : 4 : Term ub = d_tm.mkTerm(Kind::LEQ, {x, d_tm.mkInteger(100)});
2446 : 1 : d_solver->assertFormula(ub);
2447 : : Term eq =
2448 : 7 : d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::APPLY_UF, {f, x}), seven});
2449 : 1 : d_solver->assertFormula(eq);
2450 : : // x >= 0 ^ x <= 100 ^ (f x) = 7
2451 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
2452 : 1 : Term xval = d_solver->getValue(x);
2453 [ - + ][ + - ]: 1 : ASSERT_TRUE(xval.isUInt32Value());
2454 [ - + ][ + - ]: 1 : ASSERT_TRUE(xval.getUInt32Value() % 10 == 7);
2455 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
2456 : :
2457 : 4 : TEST_F(TestApiBlackSolver, declareOracleFunSat2)
2458 : : {
2459 : 1 : d_solver->setOption("oracles", "true");
2460 : 1 : d_solver->setOption("produce-models", "true");
2461 : : // f is the function implementing (lambda ((x Int) (y Int)) (= x y))
2462 : 2 : Term eq = d_solver->declareOracleFun(
2463 : 4 : "eq", {d_int, d_int}, d_bool, [&](const std::vector<Term>& input) {
2464 : 2 : return d_tm.mkBoolean(input[0] == input[1]);
2465 : 3 : });
2466 : 1 : Term x = d_tm.mkConst(d_int, "x");
2467 : 1 : Term y = d_tm.mkConst(d_int, "y");
2468 : 7 : Term neq = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::APPLY_UF, {eq, x, y})});
2469 : 1 : d_solver->assertFormula(neq);
2470 : : // (not (eq x y))
2471 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
2472 : 1 : Term xval = d_solver->getValue(x);
2473 : 1 : Term yval = d_solver->getValue(y);
2474 [ - + ][ + - ]: 1 : ASSERT_TRUE(xval != yval);
2475 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
2476 : :
2477 : : class PluginUnsat : public Plugin
2478 : : {
2479 : : public:
2480 : 1 : PluginUnsat(TermManager& tm) : Plugin(tm), d_tm(tm) {}
2481 : 1 : virtual ~PluginUnsat() {}
2482 : 1 : std::vector<Term> check() override
2483 : : {
2484 : 1 : std::vector<Term> lemmas;
2485 : : // add the "false" lemma.
2486 : 1 : Term flem = d_tm.mkBoolean(false);
2487 : 1 : lemmas.push_back(flem);
2488 : 2 : return lemmas;
2489 : 1 : }
2490 : 2 : std::string getName() override { return "PluginUnsat"; }
2491 : :
2492 : : private:
2493 : : /** Reference to the term manager */
2494 : : TermManager& d_tm;
2495 : : };
2496 : :
2497 : 4 : TEST_F(TestApiBlackSolver, pluginUnsat)
2498 : : {
2499 : 1 : PluginUnsat pu(d_tm);
2500 : 1 : d_solver->addPlugin(pu);
2501 [ - + ][ + - ]: 1 : ASSERT_TRUE(pu.getName() == "PluginUnsat");
2502 : : // should be unsat since the plugin above asserts "false" as a lemma
2503 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isUnsat());
2504 [ + - ]: 1 : }
2505 : :
2506 : : class PluginListen : public Plugin
2507 : : {
2508 : : public:
2509 : 2 : PluginListen(TermManager& tm)
2510 : 2 : : Plugin(tm), d_hasSeenTheoryLemma(false), d_hasSeenSatClause(false)
2511 : : {
2512 : 2 : }
2513 : 2 : virtual ~PluginListen() {}
2514 : 4 : void notifySatClause(const Term& cl) override
2515 : : {
2516 : 4 : Plugin::notifySatClause(cl); // Cover default implementation
2517 : 4 : d_hasSeenSatClause = true;
2518 : 4 : }
2519 : 2 : bool hasSeenSatClause() const { return d_hasSeenSatClause; }
2520 : 10 : void notifyTheoryLemma(const Term& lem) override
2521 : : {
2522 : 10 : Plugin::notifyTheoryLemma(lem); // Cover default implementation
2523 : 10 : d_hasSeenTheoryLemma = true;
2524 : 10 : }
2525 : 2 : bool hasSeenTheoryLemma() const { return d_hasSeenTheoryLemma; }
2526 : 2 : std::string getName() override { return "PluginListen"; }
2527 : :
2528 : : private:
2529 : : /** have we seen a theory lemma? */
2530 : : bool d_hasSeenTheoryLemma;
2531 : : /** have we seen a SAT clause? */
2532 : : bool d_hasSeenSatClause;
2533 : : };
2534 : :
2535 : 4 : TEST_F(TestApiBlackSolver, pluginListen)
2536 : : {
2537 : : // NOTE: this shouldn't be necessary but ensures notifySatClause is called
2538 : : // here.
2539 : 1 : d_solver->setOption("plugin-notify-sat-clause-in-solve", "false");
2540 : 1 : PluginListen pl(d_tm);
2541 : 1 : d_solver->addPlugin(pl);
2542 : 1 : Term x = d_tm.mkConst(d_string, "x");
2543 : 1 : Term y = d_tm.mkConst(d_string, "y");
2544 : 4 : Term ctn1 = d_tm.mkTerm(Kind::STRING_CONTAINS, {x, y});
2545 : 4 : Term ctn2 = d_tm.mkTerm(Kind::STRING_CONTAINS, {y, x});
2546 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::OR, {ctn1, ctn2}));
2547 : 3 : Term lx = d_tm.mkTerm(Kind::STRING_LENGTH, {x});
2548 : 3 : Term ly = d_tm.mkTerm(Kind::STRING_LENGTH, {y});
2549 : 4 : Term lc = d_tm.mkTerm(Kind::GT, {lx, ly});
2550 : 1 : d_solver->assertFormula(lc);
2551 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
2552 : : // above input formulas should induce a theory lemma and SAT clause learning
2553 [ - + ][ + - ]: 1 : ASSERT_TRUE(pl.hasSeenTheoryLemma());
2554 [ - + ][ + - ]: 1 : ASSERT_TRUE(pl.hasSeenSatClause());
2555 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2556 : :
2557 : 4 : TEST_F(TestApiBlackSolver, pluginListenCadical)
2558 : : {
2559 : 1 : cvc5::Solver solver(d_tm);
2560 : 1 : solver.setOption("sat-solver", "cadical");
2561 : 1 : solver.setOption("plugin-notify-sat-clause-in-solve", "true");
2562 : 1 : PluginListen pl(d_tm);
2563 : 1 : solver.addPlugin(pl);
2564 : 1 : Sort bv1 = d_tm.mkBitVectorSort(8);
2565 : 1 : Sort bv16 = d_tm.mkBitVectorSort(8);
2566 : 1 : Term x = d_tm.mkConst(d_bool, "x");
2567 : 1 : Term z16 = d_tm.mkBitVector(16, 0);
2568 : 1 : Term o16 = d_tm.mkBitVector(16, 1);
2569 : 1 : Term z1 = d_tm.mkBitVector(1, 0);
2570 : 1 : Term o1 = d_tm.mkBitVector(1, 1);
2571 : :
2572 : 5 : Term ite1 = d_tm.mkTerm(Kind::ITE, {x, z16, o16});
2573 : 4 : Term add = d_tm.mkTerm(Kind::BITVECTOR_ADD, {o16, ite1});
2574 : 4 : Term eq1 = d_tm.mkTerm(Kind::EQUAL, {z16, add});
2575 : 5 : Term ite2 = d_tm.mkTerm(Kind::ITE, {eq1, o1, z1});
2576 : : Term eq2 =
2577 : 6 : d_tm.mkTerm(Kind::EQUAL, {z1, d_tm.mkTerm(Kind::BITVECTOR_NOT, {ite2})});
2578 : 1 : solver.assertFormula(eq2);
2579 [ - + ][ + - ]: 1 : ASSERT_TRUE(solver.checkSat().isUnsat());
2580 : : // above input formulas should induce a theory lemma and SAT clause learning
2581 [ - + ][ + - ]: 1 : ASSERT_TRUE(pl.hasSeenTheoryLemma());
2582 [ - + ][ + - ]: 1 : ASSERT_TRUE(pl.hasSeenSatClause());
2583 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2584 : :
2585 : 4 : TEST_F(TestApiBlackSolver, verticalBars)
2586 : : {
2587 : 2 : Term a = d_solver->declareFun("|a |", {}, d_real);
2588 [ - + ][ + - ]: 2 : ASSERT_EQ("|a |", a.toString());
2589 [ + - ]: 1 : }
2590 : :
2591 : 4 : TEST_F(TestApiBlackSolver, getVersion)
2592 : : {
2593 : 1 : std::cout << d_solver->getVersion() << std::endl;
2594 : 1 : }
2595 : :
2596 : 4 : TEST_F(TestApiBlackSolver, multipleSolvers)
2597 : : {
2598 : 1 : Term function1, function2, value1, value2, definedFunction;
2599 : 1 : Term zero;
2600 : : {
2601 : 1 : Solver s1(d_tm);
2602 : 1 : s1.setLogic("ALL");
2603 : 1 : s1.setOption("produce-models", "true");
2604 : 1 : function1 = s1.declareFun("f1", {}, d_int);
2605 : 1 : Term x = d_tm.mkVar(d_int, "x");
2606 : 1 : zero = d_tm.mkInteger(0);
2607 : 2 : definedFunction = s1.defineFun("f", {x}, d_int, zero);
2608 : 1 : s1.assertFormula(function1.eqTerm(zero));
2609 : 1 : s1.checkSat();
2610 : 1 : value1 = s1.getValue(function1);
2611 : 1 : }
2612 [ - + ][ + - ]: 1 : ASSERT_EQ(zero, value1);
2613 : : {
2614 : 1 : Solver s2(d_tm);
2615 : 1 : s2.setLogic("ALL");
2616 : 1 : s2.setOption("produce-models", "true");
2617 : 1 : function2 = s2.declareFun("function2", {}, d_int);
2618 : 1 : s2.assertFormula(function2.eqTerm(value1));
2619 : 1 : s2.checkSat();
2620 : 1 : value2 = s2.getValue(function2);
2621 : 1 : }
2622 [ - + ][ + - ]: 1 : ASSERT_EQ(value1, value2);
2623 : : {
2624 : 1 : Solver s3(d_tm);
2625 : 1 : s3.setLogic("ALL");
2626 : 1 : s3.setOption("produce-models", "true");
2627 : 1 : function2 = s3.declareFun("function3", {}, d_int);
2628 : 4 : Term apply = d_tm.mkTerm(Kind::APPLY_UF, {definedFunction, zero});
2629 : 1 : s3.assertFormula(function2.eqTerm(apply));
2630 : 1 : s3.checkSat();
2631 : 1 : Term value3 = s3.getValue(function2);
2632 [ - + ][ + - ]: 1 : ASSERT_EQ(value1, value3);
2633 [ + - ][ + - ]: 1 : }
[ + - ]
2634 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
2635 : :
2636 : : #ifdef CVC5_USE_COCOA
2637 : :
2638 : 4 : TEST_F(TestApiBlackSolver, basicFiniteField)
2639 : : {
2640 : 1 : d_solver->setOption("produce-models", "true");
2641 : :
2642 : 2 : Sort F = d_tm.mkFiniteFieldSort("5");
2643 : 1 : Term a = d_tm.mkConst(F, "a");
2644 : 1 : Term b = d_tm.mkConst(F, "b");
2645 [ - + ][ + - ]: 2 : ASSERT_EQ("5", F.getFiniteFieldSize());
2646 : :
2647 : 2 : Term inv = d_tm.mkTerm(Kind::EQUAL,
2648 : 2 : {d_tm.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}),
2649 : 3 : d_tm.mkFiniteFieldElem("1", F)});
2650 : 5 : Term aIsTwo = d_tm.mkTerm(Kind::EQUAL, {a, d_tm.mkFiniteFieldElem("2", F)});
2651 : :
2652 : 1 : d_solver->assertFormula(inv);
2653 : 1 : d_solver->assertFormula(aIsTwo);
2654 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
2655 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getValue(a).getFiniteFieldValue(), "2");
2656 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getValue(b).getFiniteFieldValue(), "-2");
2657 : :
2658 : 5 : Term bIsTwo = d_tm.mkTerm(Kind::EQUAL, {b, d_tm.mkFiniteFieldElem("2", F)});
2659 : 1 : d_solver->assertFormula(bIsTwo);
2660 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_solver->checkSat().isSat());
2661 [ + - ][ + - ]: 1 : }
[ + - ]
2662 : :
2663 : 4 : TEST_F(TestApiBlackSolver, basicFiniteFieldBase)
2664 : : {
2665 : 1 : d_solver->setOption("produce-models", "true");
2666 : :
2667 : 2 : Sort F = d_tm.mkFiniteFieldSort("101", 2);
2668 : 1 : Term a = d_tm.mkConst(F, "a");
2669 : 1 : Term b = d_tm.mkConst(F, "b");
2670 [ - + ][ + - ]: 2 : ASSERT_EQ("5", F.getFiniteFieldSize());
2671 : :
2672 : 2 : Term inv = d_tm.mkTerm(Kind::EQUAL,
2673 : 2 : {d_tm.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}),
2674 : 3 : d_tm.mkFiniteFieldElem("1", F, 3)});
2675 : : Term aIsTwo =
2676 : 5 : d_tm.mkTerm(Kind::EQUAL, {a, d_tm.mkFiniteFieldElem("10", F, 2)});
2677 : :
2678 : 1 : d_solver->assertFormula(inv);
2679 : 1 : d_solver->assertFormula(aIsTwo);
2680 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
2681 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getValue(a).getFiniteFieldValue(), "2");
2682 [ - + ][ + - ]: 2 : ASSERT_EQ(d_solver->getValue(b).getFiniteFieldValue(), "-2");
2683 : :
2684 : 5 : Term bIsTwo = d_tm.mkTerm(Kind::EQUAL, {b, d_tm.mkFiniteFieldElem("2", F)});
2685 : 1 : d_solver->assertFormula(bIsTwo);
2686 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_solver->checkSat().isSat());
2687 [ + - ][ + - ]: 1 : }
[ + - ]
2688 : :
2689 : : #endif // CVC5_USE_COCOA
2690 : :
2691 : : } // namespace test
2692 : : } // namespace cvc5::internal
|
