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 : 51315 : EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
26 : 51315 : : EnvObj(env), d_qstate(qs), d_tdb(tdb)
27 : : {
28 : 51315 : d_true = nodeManager()->mkConst(true);
29 : 51315 : d_false = nodeManager()->mkConst(false);
30 : 51315 : }
31 : :
32 : 101934 : EntailmentCheck::~EntailmentCheck() {}
33 : :
34 : 125012 : 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 : 125012 : std::map<TNode, Node>::iterator itv = visited.find(n);
42 [ + + ]: 125012 : if (itv != visited.end())
43 : : {
44 : 18653 : return itv->second;
45 : : }
46 [ + - ]: 106359 : Trace("term-db-eval") << "evaluate term : " << n << std::endl;
47 : 106359 : Node ret = n;
48 : 106359 : Kind k = n.getKind();
49 [ + + ]: 106359 : if (k == Kind::FORALL)
50 : : {
51 : : // do nothing
52 : : }
53 [ + + ]: 106319 : else if (k == Kind::BOUND_VARIABLE)
54 : : {
55 : 44241 : std::map<TNode, TNode>::iterator it = subs.find(n);
56 [ + + ]: 44241 : if (it != subs.end())
57 : : {
58 [ + - ]: 20351 : if (!subsRep)
59 : : {
60 : 20351 : ret = d_qstate.getRepresentative(it->second);
61 : : }
62 : : else
63 : : {
64 : 0 : ret = it->second;
65 : : }
66 : : }
67 : : }
68 [ + + ]: 62078 : else if (d_qstate.hasTerm(n))
69 : : {
70 [ + - ]: 2902 : Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
71 : 2902 : ret = d_qstate.getRepresentative(n);
72 : 2902 : reqHasTerm = false;
73 : : }
74 [ + + ]: 59176 : else if (n.hasOperator())
75 : : {
76 : 58488 : std::vector<TNode> args;
77 : 58488 : bool ret_set = false;
78 [ + + ]: 157039 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
79 : : {
80 : 209168 : TNode c = evaluateTerm2(
81 : 104584 : n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
82 [ + + ]: 104584 : if (c.isNull())
83 : : {
84 : 6027 : ret = Node::null();
85 : 6027 : ret_set = true;
86 : 6027 : break;
87 : : }
88 [ + + ][ + + ]: 98557 : 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 [ + - ]: 98551 : Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
112 : 98551 : args.push_back(c);
113 [ + + ]: 104584 : }
114 [ + + ]: 58488 : if (!ret_set)
115 : : {
116 : : // get the (indexed) operator of n, if it exists
117 : 104910 : TNode f = d_tdb.getMatchOperator(n);
118 : : // if it is an indexed term, return the congruent term
119 [ + + ]: 52455 : if (!f.isNull())
120 : : {
121 : : // if f is congruent to a term indexed by this class
122 : 49361 : TNode nn = d_tdb.getCongruentTerm(f, args);
123 [ + - ]: 98722 : Trace("term-db-eval") << " got congruent term " << nn
124 : 49361 : << " from DB for " << n << std::endl;
125 [ + + ]: 49361 : if (!nn.isNull())
126 : : {
127 : 23371 : ret = d_qstate.getRepresentative(nn);
128 [ + - ]: 23371 : Trace("term-db-eval") << "return rep" << std::endl;
129 : 23371 : ret_set = true;
130 : 23371 : reqHasTerm = false;
131 [ - + ][ - + ]: 23371 : Assert(!ret.isNull());
[ - - ]
132 : : }
133 : 49361 : }
134 [ + + ]: 52455 : if (!ret_set)
135 : : {
136 [ + - ]: 29084 : Trace("term-db-eval") << "return rewrite" << std::endl;
137 : : // a theory symbol or a new UF term
138 [ + + ]: 29084 : if (n.getMetaKind() == metakind::PARAMETERIZED)
139 : : {
140 : 25990 : args.insert(args.begin(), n.getOperator());
141 : : }
142 : 29084 : ret = nodeManager()->mkNode(n.getKind(), args);
143 : 29084 : ret = rewrite(ret);
144 [ + + ]: 29084 : if (ret.getKind() == Kind::EQUAL)
145 : : {
146 [ - + ]: 72 : if (d_qstate.areDisequal(ret[0], ret[1]))
147 : : {
148 : 0 : ret = d_false;
149 : : }
150 : : }
151 [ + + ]: 29084 : 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 : 52455 : }
171 : 58488 : }
172 : : // must have the term
173 [ + + ][ + + ]: 106359 : if (reqHasTerm && !ret.isNull())
[ + + ]
174 : : {
175 : 27534 : Kind rk = ret.getKind();
176 [ + - ][ + - ]: 27534 : if (rk != Kind::OR && rk != Kind::AND && rk != Kind::EQUAL
[ + + ]
177 [ + - ][ + - ]: 27462 : && rk != Kind::ITE && rk != Kind::NOT && rk != Kind::FORALL)
[ + + ]
178 : : {
179 [ + + ]: 27382 : if (!d_qstate.hasTerm(ret))
180 : : {
181 : 4049 : ret = Node::null();
182 : : }
183 : : }
184 : : }
185 [ + - ]: 212718 : Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
186 : 106359 : << ", reqHasTerm = " << reqHasTerm << std::endl;
187 : 106359 : visited[n] = ret;
188 : 106359 : return ret;
189 : 106359 : }
190 : :
191 : 35847827 : TNode EntailmentCheck::getEntailedTerm2(TNode n,
192 : : std::map<TNode, TNode>& subs,
193 : : bool subsRep)
194 : : {
195 [ + - ]: 35847827 : Trace("term-db-entail") << "get entailed term : " << n << std::endl;
196 [ + + ]: 35847827 : if (d_qstate.hasTerm(n))
197 : : {
198 [ + - ]: 2654086 : Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
199 : 2654086 : return n;
200 : : }
201 [ + + ]: 33193741 : else if (n.getKind() == Kind::BOUND_VARIABLE)
202 : : {
203 : 17144048 : std::map<TNode, TNode>::iterator it = subs.find(n);
204 [ + + ]: 17144048 : if (it != subs.end())
205 : : {
206 [ + - ]: 12429488 : Trace("term-db-entail")
207 : 6214744 : << "...substitution is : " << it->second << std::endl;
208 [ + + ]: 6214744 : if (subsRep)
209 : : {
210 [ - + ][ - + ]: 4031969 : Assert(d_qstate.hasTerm(it->second));
[ - - ]
211 [ - + ][ - + ]: 4031969 : Assert(d_qstate.getRepresentative(it->second) == it->second);
[ - - ]
212 : 10246713 : return it->second;
213 : : }
214 : 2182775 : return getEntailedTerm2(it->second, subs, subsRep);
215 : : }
216 : : }
217 [ + + ]: 16049693 : else if (n.getKind() == Kind::ITE)
218 : : {
219 [ + + ]: 112950 : for (uint32_t i = 0; i < 2; i++)
220 : : {
221 [ + + ]: 85834 : if (isEntailed2(n[0], subs, subsRep, i == 0))
222 : : {
223 [ + + ]: 18148 : return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
224 : : }
225 : : }
226 : : }
227 : : else
228 : : {
229 [ + + ]: 16004429 : if (n.hasOperator())
230 : : {
231 : 31985666 : TNode f = d_tdb.getMatchOperator(n);
232 [ + + ]: 15992833 : if (!f.isNull())
233 : : {
234 : 15976456 : std::vector<TNode> args;
235 [ + + ]: 22873214 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
236 : : {
237 : 21784264 : TNode c = getEntailedTerm2(n[i], subs, subsRep);
238 [ + + ]: 21784264 : if (c.isNull())
239 : : {
240 : 14887506 : return TNode::null();
241 : : }
242 : 6896758 : c = d_qstate.getRepresentative(c);
243 [ + - ]: 6896758 : Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
244 : 6896758 : args.push_back(c);
245 [ + + ]: 21784264 : }
246 : 1088950 : TNode nn = d_tdb.getCongruentTerm(f, args);
247 [ + - ]: 2177900 : Trace("term-db-entail")
248 : 1088950 : << " got congruent term " << nn << " for " << n << std::endl;
249 : 1088950 : return nn;
250 : 15976456 : }
251 [ + + ]: 15992833 : }
252 : : }
253 : 10984393 : return TNode::null();
254 : : }
255 : :
256 : 6897 : Node EntailmentCheck::evaluateTerm(TNode n,
257 : : std::map<TNode, TNode>& subs,
258 : : bool subsRep,
259 : : bool useEntailmentTests,
260 : : bool reqHasTerm)
261 : : {
262 : 6897 : std::map<TNode, Node> visited;
263 : : return evaluateTerm2(
264 : 13794 : n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
265 : 6897 : }
266 : :
267 : 13531 : Node EntailmentCheck::evaluateTerm(TNode n,
268 : : bool useEntailmentTests,
269 : : bool reqHasTerm)
270 : : {
271 : 13531 : std::map<TNode, Node> visited;
272 : 13531 : std::map<TNode, TNode> subs;
273 : 27062 : return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
274 : 13531 : }
275 : :
276 : 10930955 : TNode EntailmentCheck::getEntailedTerm(TNode n,
277 : : std::map<TNode, TNode>& subs,
278 : : bool subsRep)
279 : : {
280 : 10930955 : return getEntailedTerm2(n, subs, subsRep);
281 : : }
282 : :
283 : 205054 : TNode EntailmentCheck::getEntailedTerm(TNode n)
284 : : {
285 : 205054 : std::map<TNode, TNode> subs;
286 : 410108 : return getEntailedTerm2(n, subs, false);
287 : 205054 : }
288 : :
289 : 1372137 : bool EntailmentCheck::isEntailed2(TNode n,
290 : : std::map<TNode, TNode>& subs,
291 : : bool subsRep,
292 : : bool pol)
293 : : {
294 [ + - ]: 2744274 : Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
295 : 1372137 : << std::endl;
296 [ - + ][ - + ]: 1372137 : Assert(n.getType().isBoolean());
[ - - ]
297 : 1372137 : Kind k = n.getKind();
298 : 1372137 : if (k == Kind::EQUAL && !n[0].getType().isBoolean())
299 : : {
300 [ + + ][ + + ]: 433369 : TNode n1 = n[0].isConst() ? n[0] : getEntailedTerm2(n[0], subs, subsRep);
[ - - ]
301 [ + + ]: 235736 : if (!n1.isNull())
302 : : {
303 [ + + ][ + + ]: 344964 : TNode n2 = n[1].isConst() ? n[1] : getEntailedTerm2(n[1], subs, subsRep);
[ - - ]
304 [ + + ]: 179557 : if (!n2.isNull())
305 : : {
306 [ + + ]: 120772 : if (pol)
307 : : {
308 : : // must check for equality here
309 : 69998 : return d_qstate.areEqual(n1, n2);
310 : : }
311 : 50774 : return d_qstate.areDisequal(n1, n2);
312 : : }
313 [ + + ]: 179557 : }
314 [ + + ]: 235736 : }
315 [ + + ]: 1136401 : else if (k == Kind::NOT)
316 : : {
317 : 406629 : return isEntailed2(n[0], subs, subsRep, !pol);
318 : : }
319 [ + + ][ + + ]: 729772 : else if (k == Kind::OR || k == Kind::AND)
320 : : {
321 [ + + ][ + + ]: 136610 : bool simPol = (pol && k == Kind::OR) || (!pol && k == Kind::AND);
[ + + ][ + + ]
322 [ + + ]: 646741 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
323 : : {
324 [ + + ]: 559776 : if (isEntailed2(n[i], subs, subsRep, pol))
325 : : {
326 [ + + ]: 29662 : if (simPol)
327 : : {
328 : 21932 : return true;
329 : : }
330 : : }
331 : : else
332 : : {
333 [ + + ]: 530114 : if (!simPol)
334 : : {
335 : 27713 : return false;
336 : : }
337 : : }
338 : : }
339 : 86965 : return !simPol;
340 : : // Boolean equality here
341 : : }
342 [ + + ][ + + ]: 593162 : else if (k == Kind::EQUAL || k == Kind::ITE)
343 : : {
344 [ - + ][ - + ]: 35928 : Assert(n[0].getType().isBoolean());
[ - - ]
345 [ + + ]: 74797 : for (size_t i = 0; i < 2; i++)
346 : : {
347 [ + + ]: 57644 : if (isEntailed2(n[0], subs, subsRep, i == 0))
348 : : {
349 [ + + ][ + + ]: 18775 : size_t ch = (k == Kind::EQUAL || i == 0) ? 1 : 2;
350 [ + + ][ + + ]: 18775 : bool reqPol = (k == Kind::ITE || i == 0) ? pol : !pol;
351 : 18775 : return isEntailed2(n[ch], subs, subsRep, reqPol);
352 : : }
353 : : }
354 : 17153 : }
355 [ + + ]: 557234 : else if (k == Kind::FORALL)
356 : : {
357 [ + + ]: 21031 : if (!pol)
358 : : {
359 : 13655 : return isEntailed2(n[1], subs, subsRep, pol);
360 : : }
361 : : }
362 [ + + ][ + + ]: 536203 : else if (k == Kind::BOUND_VARIABLE || k == Kind::APPLY_UF)
363 : : {
364 : : // handles APPLY_UF, Boolean variable cases
365 : 363591 : TNode n1 = getEntailedTerm2(n, subs, subsRep);
366 [ + + ]: 363591 : if (!n1.isNull())
367 : : {
368 [ - + ][ - + ]: 172849 : Assert(d_qstate.hasTerm(n1));
[ - - ]
369 : 172849 : n1 = d_qstate.getRepresentative(n1);
370 [ + + ]: 172849 : if (n1.isConst())
371 : : {
372 : 172363 : return n1.getConst<bool>() == pol;
373 : : }
374 : : }
375 [ + + ]: 363591 : }
376 : 503333 : return false;
377 : : }
378 : :
379 : 4314 : bool EntailmentCheck::isEntailed(TNode n, bool pol)
380 : : {
381 : 4314 : std::map<TNode, TNode> subs;
382 : 8628 : return isEntailed2(n, subs, false, pol);
383 : 4314 : }
384 : :
385 : 225510 : bool EntailmentCheck::isEntailed(TNode n,
386 : : std::map<TNode, TNode>& subs,
387 : : bool subsRep,
388 : : bool pol)
389 : : {
390 : 225510 : return isEntailed2(n, subs, subsRep, pol);
391 : : }
392 : :
393 : : } // namespace quantifiers
394 : : } // namespace theory
395 : : } // namespace cvc5::internal
|
