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 : : * Implementation of entailment check class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/entailment_check.h"
14 : :
15 : : #include "theory/quantifiers/quantifiers_state.h"
16 : : #include "theory/quantifiers/term_database.h"
17 : :
18 : : using namespace cvc5::internal::kind;
19 : : using namespace cvc5::context;
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace quantifiers {
24 : :
25 : 28931 : EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
26 : 28931 : : EnvObj(env), d_qstate(qs), d_tdb(tdb)
27 : : {
28 : 28931 : d_true = nodeManager()->mkConst(true);
29 : 28931 : d_false = nodeManager()->mkConst(false);
30 : 28931 : }
31 : :
32 : 57836 : EntailmentCheck::~EntailmentCheck() {}
33 : :
34 : 124448 : Node EntailmentCheck::evaluateTerm2(TNode n,
35 : : std::map<TNode, Node>& visited,
36 : : std::map<TNode, TNode>& subs,
37 : : bool subsRep,
38 : : bool useEntailmentTests,
39 : : bool reqHasTerm)
40 : : {
41 : 124448 : std::map<TNode, Node>::iterator itv = visited.find(n);
42 [ + + ]: 124448 : if (itv != visited.end())
43 : : {
44 : 18447 : return itv->second;
45 : : }
46 [ + - ]: 106001 : Trace("term-db-eval") << "evaluate term : " << n << std::endl;
47 : 106001 : Node ret = n;
48 : 106001 : Kind k = n.getKind();
49 [ + + ]: 106001 : if (k == Kind::FORALL)
50 : : {
51 : : // do nothing
52 : : }
53 [ + + ]: 105961 : else if (k == Kind::BOUND_VARIABLE)
54 : : {
55 : 44106 : std::map<TNode, TNode>::iterator it = subs.find(n);
56 [ + + ]: 44106 : if (it != subs.end())
57 : : {
58 [ + - ]: 20228 : if (!subsRep)
59 : : {
60 : 20228 : ret = d_qstate.getRepresentative(it->second);
61 : : }
62 : : else
63 : : {
64 : 0 : ret = it->second;
65 : : }
66 : : }
67 : : }
68 [ + + ]: 61855 : else if (d_qstate.hasTerm(n))
69 : : {
70 [ + - ]: 2896 : Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
71 : 2896 : ret = d_qstate.getRepresentative(n);
72 : 2896 : reqHasTerm = false;
73 : : }
74 [ + + ]: 58959 : else if (n.hasOperator())
75 : : {
76 : 58271 : std::vector<TNode> args;
77 : 58271 : bool ret_set = false;
78 [ + + ]: 156218 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
79 : : {
80 : 208134 : TNode c = evaluateTerm2(
81 : 104067 : n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
82 [ + + ]: 104067 : if (c.isNull())
83 : : {
84 : 6114 : ret = Node::null();
85 : 6114 : ret_set = true;
86 : 6114 : break;
87 : : }
88 [ + + ][ + + ]: 97953 : else if (c == d_true || c == d_false)
[ + + ]
89 : : {
90 : : // short-circuiting
91 [ + + ][ - + ]: 604 : if ((k == Kind::AND && c == d_false) || (k == Kind::OR && c == d_true))
[ + + ][ - + ]
[ + + ]
92 : : {
93 : 6 : ret = c;
94 : 6 : ret_set = true;
95 : 6 : reqHasTerm = false;
96 : 6 : break;
97 : : }
98 [ - + ][ - - ]: 598 : else if (k == Kind::ITE && i == 0)
99 : : {
100 [ - - ]: 0 : ret = evaluateTerm2(n[c == d_true ? 1 : 2],
101 : : visited,
102 : : subs,
103 : : subsRep,
104 : : useEntailmentTests,
105 : 0 : reqHasTerm);
106 : 0 : ret_set = true;
107 : 0 : reqHasTerm = false;
108 : 0 : break;
109 : : }
110 : : }
111 [ + - ]: 97947 : Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
112 : 97947 : args.push_back(c);
113 [ + + ]: 104067 : }
114 [ + + ]: 58271 : if (!ret_set)
115 : : {
116 : : // get the (indexed) operator of n, if it exists
117 : 104302 : TNode f = d_tdb.getMatchOperator(n);
118 : : // if it is an indexed term, return the congruent term
119 [ + + ]: 52151 : if (!f.isNull())
120 : : {
121 : : // if f is congruent to a term indexed by this class
122 : 49102 : TNode nn = d_tdb.getCongruentTerm(f, args);
123 [ + - ]: 98204 : Trace("term-db-eval") << " got congruent term " << nn
124 : 49102 : << " from DB for " << n << std::endl;
125 [ + + ]: 49102 : if (!nn.isNull())
126 : : {
127 : 23120 : ret = d_qstate.getRepresentative(nn);
128 [ + - ]: 23120 : Trace("term-db-eval") << "return rep" << std::endl;
129 : 23120 : ret_set = true;
130 : 23120 : reqHasTerm = false;
131 [ - + ][ - + ]: 23120 : Assert(!ret.isNull());
[ - - ]
132 : : }
133 : 49102 : }
134 [ + + ]: 52151 : if (!ret_set)
135 : : {
136 [ + - ]: 29031 : Trace("term-db-eval") << "return rewrite" << std::endl;
137 : : // a theory symbol or a new UF term
138 [ + + ]: 29031 : if (n.getMetaKind() == metakind::PARAMETERIZED)
139 : : {
140 : 25982 : args.insert(args.begin(), n.getOperator());
141 : : }
142 : 29031 : ret = nodeManager()->mkNode(n.getKind(), args);
143 : 29031 : ret = rewrite(ret);
144 [ + + ]: 29031 : if (ret.getKind() == Kind::EQUAL)
145 : : {
146 [ - + ]: 61 : if (d_qstate.areDisequal(ret[0], ret[1]))
147 : : {
148 : 0 : ret = d_false;
149 : : }
150 : : }
151 [ + + ]: 29031 : if (useEntailmentTests)
152 : : {
153 [ + - ][ + + ]: 478 : if (ret.getKind() == Kind::EQUAL || ret.getKind() == Kind::GEQ)
[ + + ]
154 : : {
155 : 6 : Valuation& val = d_qstate.getValuation();
156 [ + - ]: 12 : for (unsigned j = 0; j < 2; j++)
157 : : {
158 : : std::pair<bool, Node> et = val.entailmentCheck(
159 : : options::TheoryOfMode::THEORY_OF_TYPE_BASED,
160 [ + + ]: 24 : j == 0 ? ret : ret.negate());
161 [ + + ]: 12 : if (et.first)
162 : : {
163 [ - + ]: 6 : ret = j == 0 ? d_true : d_false;
164 : 6 : break;
165 : : }
166 [ + + ]: 12 : }
167 : : }
168 : : }
169 : : }
170 : 52151 : }
171 : 58271 : }
172 : : // must have the term
173 [ + + ][ + + ]: 106001 : if (reqHasTerm && !ret.isNull())
[ + + ]
174 : : {
175 : 27370 : Kind rk = ret.getKind();
176 [ + - ][ + - ]: 27370 : if (rk != Kind::OR && rk != Kind::AND && rk != Kind::EQUAL
[ + + ]
177 [ + - ][ + - ]: 27309 : && rk != Kind::ITE && rk != Kind::NOT && rk != Kind::FORALL)
[ + + ]
178 : : {
179 [ + + ]: 27229 : if (!d_qstate.hasTerm(ret))
180 : : {
181 : 4053 : ret = Node::null();
182 : : }
183 : : }
184 : : }
185 [ + - ]: 212002 : Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
186 : 106001 : << ", reqHasTerm = " << reqHasTerm << std::endl;
187 : 106001 : visited[n] = ret;
188 : 106001 : return ret;
189 : 106001 : }
190 : :
191 : 35861076 : TNode EntailmentCheck::getEntailedTerm2(TNode n,
192 : : std::map<TNode, TNode>& subs,
193 : : bool subsRep)
194 : : {
195 [ + - ]: 35861076 : Trace("term-db-entail") << "get entailed term : " << n << std::endl;
196 [ + + ]: 35861076 : if (d_qstate.hasTerm(n))
197 : : {
198 [ + - ]: 2648069 : Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
199 : 2648069 : return n;
200 : : }
201 [ + + ]: 33213007 : else if (n.getKind() == Kind::BOUND_VARIABLE)
202 : : {
203 : 17153681 : std::map<TNode, TNode>::iterator it = subs.find(n);
204 [ + + ]: 17153681 : if (it != subs.end())
205 : : {
206 [ + - ]: 12451908 : Trace("term-db-entail")
207 : 6225954 : << "...substitution is : " << it->second << std::endl;
208 [ + + ]: 6225954 : if (subsRep)
209 : : {
210 [ - + ][ - + ]: 4034581 : Assert(d_qstate.hasTerm(it->second));
[ - - ]
211 [ - + ][ - + ]: 4034581 : Assert(d_qstate.getRepresentative(it->second) == it->second);
[ - - ]
212 : 10260535 : return it->second;
213 : : }
214 : 2191373 : return getEntailedTerm2(it->second, subs, subsRep);
215 : : }
216 : : }
217 [ + + ]: 16059326 : else if (n.getKind() == Kind::ITE)
218 : : {
219 [ + + ]: 112755 : for (uint32_t i = 0; i < 2; i++)
220 : : {
221 [ + + ]: 85664 : if (isEntailed2(n[0], subs, subsRep, i == 0))
222 : : {
223 [ + + ]: 18054 : return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
224 : : }
225 : : }
226 : : }
227 : : else
228 : : {
229 [ + + ]: 16014181 : if (n.hasOperator())
230 : : {
231 : 32005362 : TNode f = d_tdb.getMatchOperator(n);
232 [ + + ]: 16002681 : if (!f.isNull())
233 : : {
234 : 15983924 : std::vector<TNode> args;
235 [ + + ]: 22896833 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
236 : : {
237 : 21802258 : TNode c = getEntailedTerm2(n[i], subs, subsRep);
238 [ + + ]: 21802258 : if (c.isNull())
239 : : {
240 : 14889349 : return TNode::null();
241 : : }
242 : 6912909 : c = d_qstate.getRepresentative(c);
243 [ + - ]: 6912909 : Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
244 : 6912909 : args.push_back(c);
245 [ + + ]: 21802258 : }
246 : 1094575 : TNode nn = d_tdb.getCongruentTerm(f, args);
247 [ + - ]: 2189150 : Trace("term-db-entail")
248 : 1094575 : << " got congruent term " << nn << " for " << n << std::endl;
249 : 1094575 : return nn;
250 : 15983924 : }
251 [ + + ]: 16002681 : }
252 : : }
253 : 10985075 : return TNode::null();
254 : : }
255 : :
256 : 6856 : Node EntailmentCheck::evaluateTerm(TNode n,
257 : : std::map<TNode, TNode>& subs,
258 : : bool subsRep,
259 : : bool useEntailmentTests,
260 : : bool reqHasTerm)
261 : : {
262 : 6856 : std::map<TNode, Node> visited;
263 : : return evaluateTerm2(
264 : 13712 : n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
265 : 6856 : }
266 : :
267 : 13525 : Node EntailmentCheck::evaluateTerm(TNode n,
268 : : bool useEntailmentTests,
269 : : bool reqHasTerm)
270 : : {
271 : 13525 : std::map<TNode, Node> visited;
272 : 13525 : std::map<TNode, TNode> subs;
273 : 27050 : return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
274 : 13525 : }
275 : :
276 : 10929379 : TNode EntailmentCheck::getEntailedTerm(TNode n,
277 : : std::map<TNode, TNode>& subs,
278 : : bool subsRep)
279 : : {
280 : 10929379 : return getEntailedTerm2(n, subs, subsRep);
281 : : }
282 : :
283 : 188916 : TNode EntailmentCheck::getEntailedTerm(TNode n)
284 : : {
285 : 188916 : std::map<TNode, TNode> subs;
286 : 377832 : return getEntailedTerm2(n, subs, false);
287 : 188916 : }
288 : :
289 : 1367530 : bool EntailmentCheck::isEntailed2(TNode n,
290 : : std::map<TNode, TNode>& subs,
291 : : bool subsRep,
292 : : bool pol)
293 : : {
294 [ + - ]: 2735060 : Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
295 : 1367530 : << std::endl;
296 [ - + ][ - + ]: 1367530 : Assert(n.getType().isBoolean());
[ - - ]
297 : 1367530 : Kind k = n.getKind();
298 : 1367530 : if (k == Kind::EQUAL && !n[0].getType().isBoolean())
299 : : {
300 [ + + ][ + + ]: 446764 : TNode n1 = n[0].isConst() ? n[0] : getEntailedTerm2(n[0], subs, subsRep);
[ - - ]
301 [ + + ]: 242457 : if (!n1.isNull())
302 : : {
303 [ + + ][ + + ]: 346176 : TNode n2 = n[1].isConst() ? n[1] : getEntailedTerm2(n[1], subs, subsRep);
[ - - ]
304 [ + + ]: 181168 : if (!n2.isNull())
305 : : {
306 [ + + ]: 123420 : if (pol)
307 : : {
308 : : // must check for equality here
309 : 70765 : return d_qstate.areEqual(n1, n2);
310 : : }
311 : 52655 : return d_qstate.areDisequal(n1, n2);
312 : : }
313 [ + + ]: 181168 : }
314 [ + + ]: 242457 : }
315 [ + + ]: 1125073 : else if (k == Kind::NOT)
316 : : {
317 : 404082 : return isEntailed2(n[0], subs, subsRep, !pol);
318 : : }
319 [ + + ][ + + ]: 720991 : else if (k == Kind::OR || k == Kind::AND)
320 : : {
321 [ + + ][ + + ]: 136441 : bool simPol = (pol && k == Kind::OR) || (!pol && k == Kind::AND);
[ + + ][ + + ]
322 [ + + ]: 641100 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
323 : : {
324 [ + + ]: 554656 : if (isEntailed2(n[i], subs, subsRep, pol))
325 : : {
326 [ + + ]: 30002 : if (simPol)
327 : : {
328 : 22057 : return true;
329 : : }
330 : : }
331 : : else
332 : : {
333 [ + + ]: 524654 : if (!simPol)
334 : : {
335 : 27940 : return false;
336 : : }
337 : : }
338 : : }
339 : 86444 : return !simPol;
340 : : // Boolean equality here
341 : : }
342 [ + + ][ + + ]: 584550 : else if (k == Kind::EQUAL || k == Kind::ITE)
343 : : {
344 [ - + ][ - + ]: 35908 : Assert(n[0].getType().isBoolean());
[ - - ]
345 [ + + ]: 75770 : for (size_t i = 0; i < 2; i++)
346 : : {
347 [ + + ]: 58462 : if (isEntailed2(n[0], subs, subsRep, i == 0))
348 : : {
349 [ + + ][ + + ]: 18600 : size_t ch = (k == Kind::EQUAL || i == 0) ? 1 : 2;
350 [ + + ][ + + ]: 18600 : bool reqPol = (k == Kind::ITE || i == 0) ? pol : !pol;
351 : 18600 : return isEntailed2(n[ch], subs, subsRep, reqPol);
352 : : }
353 : : }
354 : 17308 : }
355 [ + + ]: 548642 : else if (k == Kind::FORALL)
356 : : {
357 [ + + ]: 21168 : if (!pol)
358 : : {
359 : 13750 : return isEntailed2(n[1], subs, subsRep, pol);
360 : : }
361 : : }
362 [ + + ][ + + ]: 527474 : else if (k == Kind::BOUND_VARIABLE || k == Kind::APPLY_UF)
363 : : {
364 : : // handles APPLY_UF, Boolean variable cases
365 : 361781 : TNode n1 = getEntailedTerm2(n, subs, subsRep);
366 [ + + ]: 361781 : if (!n1.isNull())
367 : : {
368 [ - + ][ - + ]: 170992 : Assert(d_qstate.hasTerm(n1));
[ - - ]
369 : 170992 : n1 = d_qstate.getRepresentative(n1);
370 [ + + ]: 170992 : if (n1.isConst())
371 : : {
372 : 170508 : return n1.getConst<bool>() == pol;
373 : : }
374 : : }
375 [ + + ]: 361781 : }
376 : 500729 : return false;
377 : : }
378 : :
379 : 4614 : bool EntailmentCheck::isEntailed(TNode n, bool pol)
380 : : {
381 : 4614 : std::map<TNode, TNode> subs;
382 : 9228 : return isEntailed2(n, subs, false, pol);
383 : 4614 : }
384 : :
385 : 227702 : bool EntailmentCheck::isEntailed(TNode n,
386 : : std::map<TNode, TNode>& subs,
387 : : bool subsRep,
388 : : bool pol)
389 : : {
390 : 227702 : return isEntailed2(n, subs, subsRep, pol);
391 : : }
392 : :
393 : : } // namespace quantifiers
394 : : } // namespace theory
395 : : } // namespace cvc5::internal
|
