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 lifetime guarantees of the C++ API.
11 : : *
12 : : * API wrapper objects (Sort, Op, Term, Datatype, Grammar, Proof, ...) keep
13 : : * the internal node manager alive while they are in use. They must therefore
14 : : * remain usable after the TermManager and/or Solver that created them have
15 : : * been destroyed.
16 : : */
17 : :
18 : : #include <gtest/gtest.h>
19 : :
20 : : #include <memory>
21 : :
22 : : #include "test_api.h"
23 : :
24 : : namespace cvc5::internal {
25 : :
26 : : namespace test {
27 : :
28 : : class TestApiBlackLifetime : public TestApi
29 : : {
30 : : };
31 : :
32 : 4 : TEST_F(TestApiBlackLifetime, sortOutlivesTermManager)
33 : : {
34 : 1 : Sort s;
35 : 1 : Sort arr;
36 : : {
37 : 1 : TermManager tm;
38 : 1 : s = tm.getIntegerSort();
39 : 1 : arr = tm.mkArraySort(s, tm.getBooleanSort());
40 : 1 : }
41 : : // tm is destroyed here; s and arr must still be usable.
42 [ - + ][ + - ]: 1 : ASSERT_TRUE(s.isInteger());
43 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isArray());
44 [ - + ][ + - ]: 2 : ASSERT_EQ(arr.getArrayIndexSort(), s);
45 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(s.toString());
[ + - ][ - - ]
46 [ - + ][ + - ]: 2 : ASSERT_EQ(s, arr.getArrayIndexSort());
47 [ + - ][ + - ]: 1 : }
48 : :
49 : 4 : TEST_F(TestApiBlackLifetime, termOutlivesTermManager)
50 : : {
51 : 1 : Term t;
52 : 1 : Sort s;
53 : : {
54 : 1 : TermManager tm;
55 : 1 : s = tm.getIntegerSort();
56 : 1 : Term x = tm.mkConst(s, "x");
57 [ + + ][ - - ]: 3 : t = tm.mkTerm(Kind::ADD, {x, tm.mkInteger(1)});
58 : 1 : }
59 : : // tm is destroyed here; t must still be usable.
60 [ - + ][ + - ]: 1 : ASSERT_EQ(t.getKind(), Kind::ADD);
61 [ - + ][ + - ]: 2 : ASSERT_EQ(t.getSort(), s);
62 [ - + ][ + - ]: 1 : ASSERT_EQ(t.getNumChildren(), 2);
63 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(t.toString());
[ + - ][ - - ]
64 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t);
65 [ + - ][ + - ]: 1 : }
66 : :
67 : 4 : TEST_F(TestApiBlackLifetime, opOutlivesTermManager)
68 : : {
69 : 1 : Op op;
70 : : {
71 : 1 : TermManager tm;
72 : 1 : op = tm.mkOp(Kind::BITVECTOR_EXTRACT, {4, 0});
73 : 1 : }
74 : : // tm is destroyed here; op must still be usable.
75 [ - + ][ + - ]: 1 : ASSERT_TRUE(op.isIndexed());
76 [ - + ][ + - ]: 1 : ASSERT_EQ(op.getKind(), Kind::BITVECTOR_EXTRACT);
77 [ - + ][ + - ]: 1 : ASSERT_EQ(op.getNumIndices(), 2);
78 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(op[0]);
[ + - ][ - - ]
79 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(op.toString());
[ + - ][ - - ]
80 [ + - ]: 1 : }
81 : :
82 : 4 : TEST_F(TestApiBlackLifetime, termIteratorOutlivesTermManager)
83 : : {
84 : 1 : Term t;
85 : : {
86 : 1 : TermManager tm;
87 : 1 : Sort b = tm.getBooleanSort();
88 [ + + ][ - - ]: 3 : t = tm.mkTerm(Kind::AND, {tm.mkConst(b, "x"), tm.mkConst(b, "y")});
89 : 1 : }
90 : : // tm is destroyed here; iterating over t (which constructs
91 : : // Term::const_iterator objects) must still be safe.
92 : 1 : size_t count = 0;
93 [ + + ]: 3 : for (const Term& child : t)
94 : : {
95 [ - + ][ + - ]: 2 : ASSERT_FALSE(child.isNull());
96 : 2 : count++;
97 [ + - ][ + - ]: 3 : }
[ + - ]
98 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 2);
99 [ + - ]: 1 : }
100 : :
101 : 4 : TEST_F(TestApiBlackLifetime, datatypeOutlivesTermManager)
102 : : {
103 : 1 : Sort listSort;
104 : : {
105 : 1 : TermManager tm;
106 : 2 : DatatypeDecl decl = tm.mkDatatypeDecl("list");
107 : 2 : DatatypeConstructorDecl cons = tm.mkDatatypeConstructorDecl("cons");
108 : 1 : cons.addSelector("head", tm.getIntegerSort());
109 : 1 : cons.addSelectorSelf("tail");
110 : 1 : decl.addConstructor(cons);
111 : 2 : DatatypeConstructorDecl nil = tm.mkDatatypeConstructorDecl("nil");
112 : 1 : decl.addConstructor(nil);
113 : 1 : listSort = tm.mkDatatypeSort(decl);
114 : 1 : }
115 : : // tm is destroyed here; the datatype, its constructors and selectors
116 : : // (and their iterators) must still be usable.
117 : 1 : Datatype dt = listSort.getDatatype();
118 [ - + ][ + - ]: 2 : ASSERT_EQ(dt.getName(), "list");
119 [ - + ][ + - ]: 1 : ASSERT_EQ(dt.getNumConstructors(), 2);
120 : :
121 : 1 : size_t numCtors = 0;
122 [ + + ]: 3 : for (const auto& ctor : dt)
123 : : {
124 [ - + ][ + - ]: 2 : ASSERT_FALSE(ctor.getName().empty());
125 [ + + ]: 4 : for (const auto& sel : ctor)
126 : : {
127 [ - + ][ + - ]: 2 : ASSERT_FALSE(sel.getName().empty());
128 [ + - ][ + - ]: 2 : }
129 : 2 : ++numCtors;
130 [ + - ][ + - ]: 1 : }
131 [ - + ][ + - ]: 1 : ASSERT_EQ(numCtors, 2);
132 : :
133 : 2 : DatatypeConstructor consCtor = dt.getConstructor("cons");
134 [ - + ][ + - ]: 2 : ASSERT_EQ(consCtor.getName(), "cons");
135 : 2 : DatatypeSelector head = consCtor.getSelector("head");
136 [ - + ][ + - ]: 2 : ASSERT_EQ(head.getName(), "head");
137 [ - + ][ + - ]: 1 : ASSERT_TRUE(head.getCodomainSort().isInteger());
138 [ + - ][ + - ]: 1 : }
139 : :
140 : 4 : TEST_F(TestApiBlackLifetime, solverOutlivesTermManager)
141 : : {
142 : : // The Solver stores its own copy of the TermManager (sharing the
143 : : // underlying node manager), so it stays usable after the TermManager
144 : : // that constructed it has been destroyed.
145 : 1 : std::unique_ptr<Solver> slv;
146 : : {
147 : 1 : TermManager tm;
148 : 1 : slv = std::make_unique<Solver>(tm);
149 : 1 : }
150 : : // tm is destroyed here; the solver and the term manager returned by
151 : : // getTermManager() must still be usable.
152 : 1 : TermManager& tm2 = slv->getTermManager();
153 : 1 : Sort b = tm2.getBooleanSort();
154 : 1 : Term x = tm2.mkConst(b, "x");
155 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv->assertFormula(x));
[ + - ][ - - ]
156 [ - + ][ + - ]: 1 : ASSERT_TRUE(slv->checkSat().isSat());
157 [ + - ][ + - ]: 1 : }
[ + - ]
158 : :
159 : 4 : TEST_F(TestApiBlackLifetime, valueOutlivesSolverAndTermManager)
160 : : {
161 : 1 : Term value;
162 : : {
163 : 1 : TermManager tm;
164 : 1 : Solver slv(tm);
165 : 1 : slv.setOption("produce-models", "true");
166 : 1 : Sort intSort = tm.getIntegerSort();
167 : 1 : Term x = tm.mkConst(intSort, "x");
168 [ + + ][ - - ]: 3 : slv.assertFormula(tm.mkTerm(Kind::GT, {x, tm.mkInteger(0)}));
169 [ - + ][ + - ]: 1 : ASSERT_TRUE(slv.checkSat().isSat());
170 : 1 : value = slv.getValue(x);
171 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
172 : : // Both the solver and the term manager are destroyed here; the value
173 : : // term obtained from the solver must still be usable.
174 [ - + ][ + - ]: 1 : ASSERT_FALSE(value.isNull());
175 [ - + ][ + - ]: 1 : ASSERT_TRUE(value.getSort().isInteger());
176 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(value.toString());
[ + - ][ - - ]
177 [ + - ]: 1 : }
178 : :
179 : 4 : TEST_F(TestApiBlackLifetime, grammarOutlivesSolverAndTermManager)
180 : : {
181 : 1 : Grammar g;
182 : : {
183 : 1 : TermManager tm;
184 : 1 : Solver slv(tm);
185 : 1 : slv.setOption("sygus", "true");
186 : 1 : Sort b = tm.getBooleanSort();
187 : 1 : Term start = tm.mkVar(b);
188 : 2 : g = slv.mkGrammar({}, {start});
189 : 1 : g.addRule(start, tm.mkBoolean(false));
190 : 1 : }
191 : : // Both the solver and the term manager are destroyed here; the grammar
192 : : // must still be usable.
193 [ - + ][ + - ]: 2 : ASSERT_NE(g.toString(), "");
194 [ + - ]: 1 : }
195 : :
196 : 4 : TEST_F(TestApiBlackLifetime, proofOutlivesSolverAndTermManager)
197 : : {
198 : 1 : Proof proof;
199 : : {
200 : 1 : TermManager tm;
201 : 1 : Solver slv(tm);
202 : 1 : slv.setOption("produce-proofs", "true");
203 : 1 : Sort b = tm.getBooleanSort();
204 : 1 : Term x = tm.mkConst(b, "x");
205 : 1 : slv.assertFormula(x);
206 : 1 : slv.assertFormula(x.notTerm());
207 [ - + ][ + - ]: 1 : ASSERT_FALSE(slv.checkSat().isSat());
208 : 1 : proof = slv.getProof().front();
209 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
210 : : // Both the solver and the term manager are destroyed here; the proof
211 : : // must still be usable.
212 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getRule());
[ + - ][ - - ]
213 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getResult());
[ + - ][ - - ]
214 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(proof.getChildren());
[ + - ][ - - ]
215 [ + - ]: 1 : }
216 : :
217 : : } // namespace test
218 : : } // namespace cvc5::internal
|
