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 : 28708 : EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
26 : 28708 : : EnvObj(env), d_qstate(qs), d_tdb(tdb)
27 : : {
28 : 28708 : d_true = nodeManager()->mkConst(true);
29 : 28708 : d_false = nodeManager()->mkConst(false);
30 : 28708 : }
31 : :
32 : 57390 : EntailmentCheck::~EntailmentCheck() {}
33 : :
34 : 125000 : 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 : 125000 : std::map<TNode, Node>::iterator itv = visited.find(n);
42 [ + + ]: 125000 : if (itv != visited.end())
43 : : {
44 : 18673 : return itv->second;
45 : : }
46 [ + - ]: 106327 : Trace("term-db-eval") << "evaluate term : " << n << std::endl;
47 : 106327 : Node ret = n;
48 : 106327 : Kind k = n.getKind();
49 [ + + ]: 106327 : if (k == Kind::FORALL)
50 : : {
51 : : // do nothing
52 : : }
53 [ + + ]: 106287 : else if (k == Kind::BOUND_VARIABLE)
54 : : {
55 : 44229 : std::map<TNode, TNode>::iterator it = subs.find(n);
56 [ + + ]: 44229 : if (it != subs.end())
57 : : {
58 [ + - ]: 20339 : if (!subsRep)
59 : : {
60 : 20339 : ret = d_qstate.getRepresentative(it->second);
61 : : }
62 : : else
63 : : {
64 : 0 : ret = it->second;
65 : : }
66 : : }
67 : : }
68 [ + + ]: 62058 : 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 [ + + ]: 59156 : else if (n.hasOperator())
75 : : {
76 : 58468 : std::vector<TNode> args;
77 : 58468 : bool ret_set = false;
78 [ + + ]: 157054 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
79 : : {
80 : 209152 : TNode c = evaluateTerm2(
81 : 104576 : n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
82 [ + + ]: 104576 : if (c.isNull())
83 : : {
84 : 5984 : ret = Node::null();
85 : 5984 : ret_set = true;
86 : 5984 : break;
87 : : }
88 [ + + ][ + + ]: 98592 : 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 [ + - ]: 98586 : Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
112 : 98586 : args.push_back(c);
113 [ + + ]: 104576 : }
114 [ + + ]: 58468 : if (!ret_set)
115 : : {
116 : : // get the (indexed) operator of n, if it exists
117 : 104956 : TNode f = d_tdb.getMatchOperator(n);
118 : : // if it is an indexed term, return the congruent term
119 [ + + ]: 52478 : if (!f.isNull())
120 : : {
121 : : // if f is congruent to a term indexed by this class
122 : 49377 : TNode nn = d_tdb.getCongruentTerm(f, args);
123 [ + - ]: 98754 : Trace("term-db-eval") << " got congruent term " << nn
124 : 49377 : << " from DB for " << n << std::endl;
125 [ + + ]: 49377 : if (!nn.isNull())
126 : : {
127 : 23398 : ret = d_qstate.getRepresentative(nn);
128 [ + - ]: 23398 : Trace("term-db-eval") << "return rep" << std::endl;
129 : 23398 : ret_set = true;
130 : 23398 : reqHasTerm = false;
131 [ - + ][ - + ]: 23398 : Assert(!ret.isNull());
[ - - ]
132 : : }
133 : 49377 : }
134 [ + + ]: 52478 : if (!ret_set)
135 : : {
136 [ + - ]: 29080 : Trace("term-db-eval") << "return rewrite" << std::endl;
137 : : // a theory symbol or a new UF term
138 [ + + ]: 29080 : if (n.getMetaKind() == metakind::PARAMETERIZED)
139 : : {
140 : 25979 : args.insert(args.begin(), n.getOperator());
141 : : }
142 : 29080 : ret = nodeManager()->mkNode(n.getKind(), args);
143 : 29080 : ret = rewrite(ret);
144 [ + + ]: 29080 : 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 [ + + ]: 29080 : 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 : 52478 : }
171 : 58468 : }
172 : : // must have the term
173 [ + + ][ + + ]: 106327 : if (reqHasTerm && !ret.isNull())
[ + + ]
174 : : {
175 : 27518 : Kind rk = ret.getKind();
176 [ + - ][ + - ]: 27518 : if (rk != Kind::OR && rk != Kind::AND && rk != Kind::EQUAL
[ + + ]
177 [ + - ][ + - ]: 27446 : && rk != Kind::ITE && rk != Kind::NOT && rk != Kind::FORALL)
[ + + ]
178 : : {
179 [ + + ]: 27366 : if (!d_qstate.hasTerm(ret))
180 : : {
181 : 4038 : ret = Node::null();
182 : : }
183 : : }
184 : : }
185 [ + - ]: 212654 : Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
186 : 106327 : << ", reqHasTerm = " << reqHasTerm << std::endl;
187 : 106327 : visited[n] = ret;
188 : 106327 : return ret;
189 : 106327 : }
190 : :
191 : 35839237 : TNode EntailmentCheck::getEntailedTerm2(TNode n,
192 : : std::map<TNode, TNode>& subs,
193 : : bool subsRep)
194 : : {
195 [ + - ]: 35839237 : Trace("term-db-entail") << "get entailed term : " << n << std::endl;
196 [ + + ]: 35839237 : if (d_qstate.hasTerm(n))
197 : : {
198 [ + - ]: 2655997 : Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
199 : 2655997 : return n;
200 : : }
201 [ + + ]: 33183240 : else if (n.getKind() == Kind::BOUND_VARIABLE)
202 : : {
203 : 17139620 : std::map<TNode, TNode>::iterator it = subs.find(n);
204 [ + + ]: 17139620 : if (it != subs.end())
205 : : {
206 [ + - ]: 12429550 : Trace("term-db-entail")
207 : 6214775 : << "...substitution is : " << it->second << std::endl;
208 [ + + ]: 6214775 : if (subsRep)
209 : : {
210 [ - + ][ - + ]: 4030568 : Assert(d_qstate.hasTerm(it->second));
[ - - ]
211 [ - + ][ - + ]: 4030568 : Assert(d_qstate.getRepresentative(it->second) == it->second);
[ - - ]
212 : 10245343 : return it->second;
213 : : }
214 : 2184207 : return getEntailedTerm2(it->second, subs, subsRep);
215 : : }
216 : : }
217 [ + + ]: 16043620 : else if (n.getKind() == Kind::ITE)
218 : : {
219 [ + + ]: 112936 : for (uint32_t i = 0; i < 2; i++)
220 : : {
221 [ + + ]: 85831 : if (isEntailed2(n[0], subs, subsRep, i == 0))
222 : : {
223 [ + + ]: 18167 : return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
224 : : }
225 : : }
226 : : }
227 : : else
228 : : {
229 [ + + ]: 15998348 : if (n.hasOperator())
230 : : {
231 : 31973704 : TNode f = d_tdb.getMatchOperator(n);
232 [ + + ]: 15986852 : if (!f.isNull())
233 : : {
234 : 15970543 : std::vector<TNode> args;
235 [ + + ]: 22869032 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
236 : : {
237 : 21779850 : TNode c = getEntailedTerm2(n[i], subs, subsRep);
238 [ + + ]: 21779850 : if (c.isNull())
239 : : {
240 : 14881361 : return TNode::null();
241 : : }
242 : 6898489 : c = d_qstate.getRepresentative(c);
243 [ + - ]: 6898489 : Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
244 : 6898489 : args.push_back(c);
245 [ + + ]: 21779850 : }
246 : 1089182 : TNode nn = d_tdb.getCongruentTerm(f, args);
247 [ + - ]: 2178364 : Trace("term-db-entail")
248 : 1089182 : << " got congruent term " << nn << " for " << n << std::endl;
249 : 1089182 : return nn;
250 : 15970543 : }
251 [ + + ]: 15986852 : }
252 : : }
253 : 10979755 : return TNode::null();
254 : : }
255 : :
256 : 6893 : Node EntailmentCheck::evaluateTerm(TNode n,
257 : : std::map<TNode, TNode>& subs,
258 : : bool subsRep,
259 : : bool useEntailmentTests,
260 : : bool reqHasTerm)
261 : : {
262 : 6893 : std::map<TNode, Node> visited;
263 : : return evaluateTerm2(
264 : 13786 : n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
265 : 6893 : }
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 : 10926407 : TNode EntailmentCheck::getEntailedTerm(TNode n,
277 : : std::map<TNode, TNode>& subs,
278 : : bool subsRep)
279 : : {
280 : 10926407 : 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 : 1369809 : bool EntailmentCheck::isEntailed2(TNode n,
290 : : std::map<TNode, TNode>& subs,
291 : : bool subsRep,
292 : : bool pol)
293 : : {
294 [ + - ]: 2739618 : Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
295 : 1369809 : << std::endl;
296 [ - + ][ - + ]: 1369809 : Assert(n.getType().isBoolean());
[ - - ]
297 : 1369809 : Kind k = n.getKind();
298 : 1369809 : if (k == Kind::EQUAL && !n[0].getType().isBoolean())
299 : : {
300 [ + + ][ + + ]: 434146 : TNode n1 = n[0].isConst() ? n[0] : getEntailedTerm2(n[0], subs, subsRep);
[ - - ]
301 [ + + ]: 236144 : if (!n1.isNull())
302 : : {
303 [ + + ][ + + ]: 346054 : TNode n2 = n[1].isConst() ? n[1] : getEntailedTerm2(n[1], subs, subsRep);
[ - - ]
304 [ + + ]: 180102 : if (!n2.isNull())
305 : : {
306 [ + + ]: 120914 : if (pol)
307 : : {
308 : : // must check for equality here
309 : 70061 : return d_qstate.areEqual(n1, n2);
310 : : }
311 : 50853 : return d_qstate.areDisequal(n1, n2);
312 : : }
313 [ + + ]: 180102 : }
314 [ + + ]: 236144 : }
315 [ + + ]: 1133665 : else if (k == Kind::NOT)
316 : : {
317 : 406574 : return isEntailed2(n[0], subs, subsRep, !pol);
318 : : }
319 [ + + ][ + + ]: 727091 : else if (k == Kind::OR || k == Kind::AND)
320 : : {
321 [ + + ][ + + ]: 136479 : bool simPol = (pol && k == Kind::OR) || (!pol && k == Kind::AND);
[ + + ][ + + ]
322 [ + + ]: 646446 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
323 : : {
324 [ + + ]: 559500 : if (isEntailed2(n[i], subs, subsRep, pol))
325 : : {
326 [ + + ]: 29692 : if (simPol)
327 : : {
328 : 21932 : return true;
329 : : }
330 : : }
331 : : else
332 : : {
333 [ + + ]: 529808 : if (!simPol)
334 : : {
335 : 27601 : return false;
336 : : }
337 : : }
338 : : }
339 : 86946 : return !simPol;
340 : : // Boolean equality here
341 : : }
342 [ + + ][ + + ]: 590612 : else if (k == Kind::EQUAL || k == Kind::ITE)
343 : : {
344 [ - + ][ - + ]: 35063 : Assert(n[0].getType().isBoolean());
[ - - ]
345 [ + + ]: 74102 : for (size_t i = 0; i < 2; i++)
346 : : {
347 [ + + ]: 56878 : if (isEntailed2(n[0], subs, subsRep, i == 0))
348 : : {
349 [ + + ][ + + ]: 17839 : size_t ch = (k == Kind::EQUAL || i == 0) ? 1 : 2;
350 [ + + ][ + + ]: 17839 : bool reqPol = (k == Kind::ITE || i == 0) ? pol : !pol;
351 : 17839 : return isEntailed2(n[ch], subs, subsRep, reqPol);
352 : : }
353 : : }
354 : 17224 : }
355 [ + + ]: 555549 : else if (k == Kind::FORALL)
356 : : {
357 [ + + ]: 21085 : if (!pol)
358 : : {
359 : 13665 : return isEntailed2(n[1], subs, subsRep, pol);
360 : : }
361 : : }
362 [ + + ][ + + ]: 534464 : else if (k == Kind::BOUND_VARIABLE || k == Kind::APPLY_UF)
363 : : {
364 : : // handles APPLY_UF, Boolean variable cases
365 : 361598 : TNode n1 = getEntailedTerm2(n, subs, subsRep);
366 [ + + ]: 361598 : if (!n1.isNull())
367 : : {
368 [ - + ][ - + ]: 170866 : Assert(d_qstate.hasTerm(n1));
[ - - ]
369 : 170866 : n1 = d_qstate.getRepresentative(n1);
370 [ + + ]: 170866 : if (n1.isConst())
371 : : {
372 : 170380 : return n1.getConst<bool>() == pol;
373 : : }
374 : : }
375 [ + + ]: 361598 : }
376 : 503958 : return false;
377 : : }
378 : :
379 : 4566 : bool EntailmentCheck::isEntailed(TNode n, bool pol)
380 : : {
381 : 4566 : std::map<TNode, TNode> subs;
382 : 9132 : return isEntailed2(n, subs, false, pol);
383 : 4566 : }
384 : :
385 : 224956 : bool EntailmentCheck::isEntailed(TNode n,
386 : : std::map<TNode, TNode>& subs,
387 : : bool subsRep,
388 : : bool pol)
389 : : {
390 : 224956 : return isEntailed2(n, subs, subsRep, pol);
391 : : }
392 : :
393 : : } // namespace quantifiers
394 : : } // namespace theory
395 : : } // namespace cvc5::internal
|
