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 : : * State for instantiation evaluator
11 : : */
12 : :
13 : : #include "theory/quantifiers/ieval/state.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "theory/quantifiers/quantifiers_state.h"
18 : : #include "theory/quantifiers/term_database.h"
19 : :
20 : : using namespace cvc5::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace quantifiers {
25 : : namespace ieval {
26 : :
27 : 69001 : State::State(Env& env, context::Context* c, QuantifiersState& qs, TermDb& tdb)
28 : : : EnvObj(env),
29 : 69001 : d_ctx(c),
30 : 69001 : d_qstate(qs),
31 : 69001 : d_tdb(tdb),
32 : 69001 : d_tevMode(ieval::TermEvaluatorMode::NONE),
33 : 69001 : d_registeredTerms(c),
34 : 69001 : d_registeredBaseTerms(c),
35 : 69001 : d_initialized(c, false),
36 : 138002 : d_numActiveQuant(c, 0)
37 : : {
38 : 69001 : NodeManager* nm = nodeManager();
39 : 69001 : SkolemManager* sm = nm->getSkolemManager();
40 : 69001 : TypeNode btype = nm->booleanType();
41 : 69001 : d_none = sm->mkInternalSkolemFunction(InternalSkolemId::IEVAL_NONE, btype);
42 : 69001 : d_some = sm->mkInternalSkolemFunction(InternalSkolemId::IEVAL_SOME, btype);
43 : 69001 : }
44 : :
45 : 7079770 : bool State::hasInitialized() const { return d_initialized.get(); }
46 : :
47 : 183493 : bool State::initialize()
48 : : {
49 [ - + ][ - + ]: 183493 : Assert(!d_initialized.get());
[ - - ]
50 [ + - ]: 183493 : Trace("ieval") << "INITIALIZE" << std::endl;
51 : : // should have set a valid evaluator mode
52 [ - + ][ - + ]: 183493 : Assert(d_tec != nullptr);
[ - - ]
53 : 183493 : d_initialized = true;
54 [ + + ]: 404562 : for (const Node& b : d_registeredBaseTerms)
55 : : {
56 : 482990 : Node bev = d_tec->evaluateBase(*this, b);
57 [ - + ][ - + ]: 241495 : Assert(!bev.isNull());
[ - - ]
58 [ + - ]: 482990 : Trace("ieval") << " " << b << " := " << bev << " (initialize)"
59 : 241495 : << std::endl;
60 : 241495 : notifyPatternEqGround(b, bev);
61 [ + + ]: 241495 : if (isFinished())
62 : : {
63 : 20426 : return false;
64 : : }
65 [ + + ][ + + ]: 261921 : }
66 : 163067 : return true;
67 : : }
68 : :
69 : 69001 : void State::setEvaluatorMode(TermEvaluatorMode tev)
70 : : {
71 : 69001 : d_tevMode = tev;
72 : : // initialize the term evaluator, which is freshly allocated
73 [ + + ][ + + ]: 69001 : if (tev == TermEvaluatorMode::CONFLICT || tev == TermEvaluatorMode::PROP
74 [ + - ]: 28712 : || tev == TermEvaluatorMode::NO_ENTAIL)
75 : : {
76 : : // finding conflict, propagating, or non-entailed instances all
77 : : // involve the entailment term evaluator
78 : 69001 : d_tec.reset(new TermEvaluatorEntailed(d_env, tev, d_qstate, d_tdb));
79 : : }
80 : 69001 : }
81 : :
82 : 69001 : void State::watch(Node q, const std::vector<Node>& vars, Node body)
83 : : {
84 : : // Note this method does not rely on d_tec, since evaluation may be
85 : : // context dependent.
86 : 69001 : std::map<Node, QuantInfo>::iterator it = d_quantInfo.find(q);
87 [ - + ]: 69001 : if (it != d_quantInfo.end())
88 : : {
89 : : // already initialized
90 : 0 : return;
91 : : }
92 : 69001 : d_quantInfo.emplace(q, d_ctx);
93 : 69001 : it = d_quantInfo.find(q);
94 : : // initialize the quantifier info, which stores basic constraint information
95 : 69001 : it->second.initialize(q, body);
96 : : // add to free variable lists
97 [ + + ]: 236882 : for (const Node& v : vars)
98 : : {
99 : 167881 : FreeVarInfo& finfo = getOrMkFreeVarInfo(v);
100 : 167881 : finfo.d_quantList.push_back(q);
101 : : }
102 : : // initialize pattern terms
103 : 69001 : NodeSet::const_iterator itr;
104 : 69001 : std::vector<TNode> visit;
105 : : // we traverse its constraint terms to set up the parent notification lists
106 : 69001 : const std::map<TNode, bool>& cterms = it->second.getConstraints();
107 [ + + ]: 197791 : for (const std::pair<const TNode, bool>& c : cterms)
108 : : {
109 : : // we will notify the quantified formula when the pattern becomes set
110 : 128790 : PatTermInfo& pi = getOrMkPatTermInfo(c.first);
111 : : // when the constraint term is assigned, we notify q
112 : 128790 : pi.d_parentNotify.push_back(q);
113 : : // we visit the constraint term below
114 : 128790 : visit.push_back(c.first);
115 : : }
116 : :
117 : 69001 : TNode cur;
118 : : do
119 : : {
120 : 1031120 : cur = visit.back();
121 : 1031120 : visit.pop_back();
122 : 1031120 : itr = d_registeredTerms.find(cur);
123 [ + + ]: 1031120 : if (itr == d_registeredTerms.end())
124 : : {
125 : 700348 : d_registeredTerms.insert(cur);
126 [ + + ]: 700348 : if (cur.getKind() == Kind::BOUND_VARIABLE)
127 : : {
128 : : // should be one of the free variables of the quantified formula
129 [ - + ][ - + ]: 164751 : Assert(std::find(vars.begin(), vars.end(), cur) != vars.end());
[ - - ]
130 : 164751 : continue;
131 : : }
132 : 535597 : size_t nchild = 0;
133 [ + + ]: 535597 : if (QuantInfo::isTraverseTerm(cur))
134 : : {
135 : : // get the unique children
136 : 522920 : std::set<TNode> children;
137 : : // we don't traverse into operators here
138 : 522920 : children.insert(cur.begin(), cur.end());
139 [ + + ]: 1448723 : for (TNode cc : children)
140 : : {
141 : : // skip constants
142 [ + + ]: 925803 : if (cc.isConst())
143 : : {
144 : 23473 : continue;
145 : : }
146 : 902330 : nchild++;
147 : : // require notifications to parent
148 : 902330 : PatTermInfo& pic = getOrMkPatTermInfo(cc);
149 : 902330 : pic.d_parentNotify.push_back(cur);
150 : 902330 : visit.push_back(cc);
151 [ + + ]: 925803 : }
152 : 522920 : }
153 [ + + ]: 535597 : if (nchild > 0)
154 : : {
155 : : // set the number of watched children
156 : 429678 : PatTermInfo& pi = getPatTermInfo(cur);
157 : 429678 : pi.d_numUnassigned = nchild;
158 : : }
159 : : else
160 : : {
161 [ - + ][ - + ]: 105919 : Assert(d_pInfo.find(cur) != d_pInfo.end());
[ - - ]
162 : : // no notifying children, this term will be initialized immediately
163 : 105919 : d_registeredBaseTerms.insert(cur);
164 : : }
165 : : }
166 [ + + ]: 1031120 : } while (!visit.empty());
167 : : // increment the count of quantified formulas
168 : 69001 : d_numActiveQuant = d_numActiveQuant + 1;
169 : 69001 : }
170 : :
171 : 5371843 : bool State::assignVar(TNode v,
172 : : TNode r,
173 : : std::vector<Node>& assignedQuants,
174 : : bool trackAssignedQuant)
175 : : {
176 : : // notify that the variable is equal to the ground term
177 [ + - ]: 5371843 : Trace("ieval") << "ASSIGN: " << v << " := " << r << std::endl;
178 [ - + ][ - + ]: 5371843 : Assert(d_initialized.get());
[ - - ]
179 : : // note that we allow setting patterns to terms that evaluate to "none",
180 : : // e.g. for conflict-based instantiation where a variable is entailed
181 : : // equal to a term in the body of the quantified formula that is not
182 : : // registered to the term database.
183 : 10743686 : Assert(isNone(getValue(r)) || getValue(r) == r)
184 : 5371843 : << "Unexpected value " << getValue(r) << " for " << r;
185 : 5371843 : notifyPatternEqGround(v, r);
186 : : // might the inactive now
187 [ + + ]: 5371843 : if (isFinished())
188 : : {
189 : 2960682 : return false;
190 : : }
191 [ - + ]: 2411161 : if (trackAssignedQuant)
192 : : {
193 : : // decrement the unassigned variable counts for all quantified formulas
194 : : // containing this variable
195 : 0 : FreeVarInfo& finfo = getFreeVarInfo(v);
196 [ - - ]: 0 : for (const Node& q : finfo.d_quantList)
197 : : {
198 : 0 : QuantInfo& qinfo = getQuantInfo(q);
199 [ - - ]: 0 : if (!qinfo.isActive())
200 : : {
201 : : // marked inactive, skip
202 : 0 : continue;
203 : : }
204 [ - - ]: 0 : if (qinfo.getNumUnassignedVars() == 1)
205 : : {
206 : : // now fully assigned
207 : 0 : assignedQuants.push_back(q);
208 : : // set inactive
209 : 0 : setQuantInactive(qinfo);
210 : : }
211 : : else
212 : : {
213 : : // decrement the variable
214 : 0 : qinfo.decrementUnassignedVar();
215 : : }
216 : : }
217 : : }
218 : 2411161 : return true;
219 : : }
220 : :
221 : 73660 : void State::getFailureExp(Node q, std::unordered_set<Node>& processed) const
222 : : {
223 : 73660 : const QuantInfo& qi = getQuantInfo(q);
224 : 73660 : TNode failConstraint = qi.getFailureConstraint();
225 [ - + ][ - + ]: 73660 : Assert(!failConstraint.isNull());
[ - - ]
226 : 73660 : std::vector<TNode> visit;
227 : 73660 : visit.push_back(failConstraint);
228 : : do
229 : : {
230 : 347264 : TNode cur = visit.back();
231 : 347264 : visit.pop_back();
232 [ + + ]: 347264 : if (processed.find(cur) == processed.end())
233 : : {
234 : 336354 : processed.insert(cur);
235 : : // as an optimization, only visit children of terms that have bound
236 : : // variables
237 : 336354 : if (!expr::hasBoundVar(cur) || !QuantInfo::isTraverseTerm(cur))
238 : : {
239 : 23217 : continue;
240 : : }
241 : 313137 : Assert(d_pInfo.find(cur) != d_pInfo.end())
242 : 0 : << "Missing pattern info for " << cur;
243 : 313137 : const PatTermInfo& pi = getPatTermInfo(cur);
244 : 313137 : TNode pcexp = pi.d_evalExpChild.get();
245 [ + + ]: 313137 : if (!pcexp.isNull())
246 : : {
247 : : // partial evaluation was forced by single child
248 : 112948 : visit.push_back(pcexp);
249 : : }
250 : : else
251 : : {
252 : : // used all children to evaluate, add all to visit list
253 : 200189 : visit.insert(visit.end(), cur.begin(), cur.end());
254 : : }
255 : 313137 : }
256 [ + + ][ + + ]: 694528 : } while (!visit.empty());
257 : 73660 : }
258 : :
259 : 15729283 : bool State::isFinished() const { return d_numActiveQuant == 0; }
260 : :
261 : 4653461 : QuantInfo& State::getQuantInfo(TNode q)
262 : : {
263 : 4653461 : std::map<Node, QuantInfo>::iterator it = d_quantInfo.find(q);
264 [ - + ][ - + ]: 4653461 : Assert(it != d_quantInfo.end());
[ - - ]
265 : 4653461 : return it->second;
266 : : }
267 : :
268 : 73660 : const QuantInfo& State::getQuantInfo(TNode q) const
269 : : {
270 : 73660 : std::map<Node, QuantInfo>::const_iterator it = d_quantInfo.find(q);
271 [ - + ][ - + ]: 73660 : Assert(it != d_quantInfo.end());
[ - - ]
272 : 73660 : return it->second;
273 : : }
274 : :
275 : 167881 : FreeVarInfo& State::getOrMkFreeVarInfo(TNode v)
276 : : {
277 : 167881 : std::map<Node, FreeVarInfo>::iterator it = d_fvInfo.find(v);
278 [ + - ]: 167881 : if (it == d_fvInfo.end())
279 : : {
280 : 167881 : d_fvInfo.emplace(v, d_ctx);
281 : 167881 : it = d_fvInfo.find(v);
282 : : }
283 : 167881 : return it->second;
284 : : }
285 : :
286 : 0 : FreeVarInfo& State::getFreeVarInfo(TNode v)
287 : : {
288 : 0 : std::map<Node, FreeVarInfo>::iterator it = d_fvInfo.find(v);
289 : 0 : Assert(it != d_fvInfo.end());
290 : 0 : return it->second;
291 : : }
292 : :
293 : 1031120 : PatTermInfo& State::getOrMkPatTermInfo(TNode p)
294 : : {
295 : 1031120 : std::map<Node, PatTermInfo>::iterator it = d_pInfo.find(p);
296 [ + + ]: 1031120 : if (it == d_pInfo.end())
297 : : {
298 : 700348 : it = d_pInfo.emplace(p, d_ctx).first;
299 : : // initialize the pattern
300 : 700348 : it->second.initialize(p);
301 : : }
302 : 1031120 : return it->second;
303 : : }
304 : :
305 : 429678 : PatTermInfo& State::getPatTermInfo(TNode p)
306 : : {
307 : 429678 : std::map<Node, PatTermInfo>::iterator it = d_pInfo.find(p);
308 [ - + ][ - + ]: 429678 : Assert(it != d_pInfo.end());
[ - - ]
309 : 429678 : return it->second;
310 : : }
311 : :
312 : 313137 : const PatTermInfo& State::getPatTermInfo(TNode p) const
313 : : {
314 : 313137 : std::map<Node, PatTermInfo>::const_iterator it = d_pInfo.find(p);
315 [ - + ][ - + ]: 313137 : Assert(it != d_pInfo.end());
[ - - ]
316 : 313137 : return it->second;
317 : : }
318 : :
319 : 5613338 : void State::notifyPatternEqGround(TNode p, TNode g)
320 : : {
321 [ + - ]: 11226676 : Trace("ieval-state-debug")
322 : 5613338 : << "Notify pattern eq ground: " << p << " == " << g << std::endl;
323 [ - + ][ - + ]: 5613338 : Assert(!g.isNull());
[ - - ]
324 [ - + ][ - + ]: 5613338 : Assert(!expr::hasFreeVar(g));
[ - - ]
325 : : // note that we allow setting patterns to terms that evaluate to "none",
326 : : // e.g. for conflict-based instantiation where a variable is entailed
327 : : // equal to a term in the body of the quantified formula that is not
328 : : // registered to the term database.
329 : 11226676 : Assert(isNone(d_tec->evaluateBase(*this, g))
330 : : || d_tec->evaluateBase(*this, g) == g)
331 : 5613338 : << "Bad eval: " << d_tec->evaluateBase(*this, g) << " " << g;
332 : 5613338 : std::map<Node, PatTermInfo>::iterator it = d_pInfo.find(p);
333 [ + + ]: 5613338 : if (it == d_pInfo.end())
334 : : {
335 : : // in rare cases, we may be considering a quantified formula not containing
336 : : // one of its bound variables, e.g. if the variable is in an annotation
337 : : // (pattern) only, or if only in nested quantification.
338 : 18832 : return;
339 : : }
340 [ + + ]: 5594546 : if (!it->second.isActive())
341 : : {
342 : : // already assigned
343 : 40 : return;
344 : : }
345 : 5594506 : it->second.d_eq = g;
346 : : // run notifications until fixed point
347 : 5594506 : size_t tnIndex = 0;
348 : 5594506 : std::vector<std::map<Node, PatTermInfo>::iterator> toNotify;
349 : 5594506 : toNotify.push_back(it);
350 [ + + ]: 30972093 : while (tnIndex < toNotify.size())
351 : : {
352 : 25377587 : it = toNotify[tnIndex];
353 : 25377587 : ++tnIndex;
354 [ - + ][ - + ]: 25377587 : Assert(it != d_pInfo.end());
[ - - ]
355 : 25377587 : p = it->second.d_pattern;
356 : 25377587 : g = it->second.d_eq;
357 [ + - ]: 50755174 : Trace("ieval-state-debug")
358 : 25377587 : << "process notifications (" << p << ", " << g << ")" << std::endl;
359 [ - + ][ - + ]: 25377587 : Assert(!g.isNull());
[ - - ]
360 : 25377587 : context::CDList<Node>& notifyList = it->second.d_parentNotify;
361 [ + + ]: 58094836 : for (TNode pp : notifyList)
362 : : {
363 [ + + ]: 35992209 : if (pp.getKind() == Kind::FORALL)
364 : : {
365 : : // if we have a quantified formula as a parent, notify is a special
366 : : // method, which will test the constraints
367 : 4653461 : notifyQuant(pp, p, g);
368 : : // could be finished now
369 [ + + ]: 4653461 : if (isFinished())
370 : : {
371 : 3274960 : break;
372 : : }
373 : 1378501 : continue;
374 : : }
375 : : // otherwise, notify the parent pattern
376 : 31338748 : it = d_pInfo.find(pp);
377 [ - + ][ - + ]: 31338748 : Assert(it != d_pInfo.end());
[ - - ]
378 : : // returns true if we have evaluated
379 [ + + ]: 31338748 : if (it->second.notifyChild(*this, p, g, d_tec.get()))
380 : : {
381 : 19783081 : toNotify.push_back(it);
382 : : }
383 [ + + ][ + ]: 35992209 : }
384 : : }
385 : 5594506 : }
386 : :
387 : 4653461 : void State::notifyQuant(TNode q, TNode p, TNode val)
388 : : {
389 [ - + ][ - + ]: 4653461 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
390 : 4653461 : QuantInfo& qi = getQuantInfo(q);
391 [ + + ]: 4653461 : if (!qi.isActive())
392 : : {
393 : : // quantified formula is already inactive
394 : 293852 : return;
395 : : }
396 [ - + ][ - + ]: 4359609 : Assert(!val.isNull());
[ - - ]
397 [ - + ][ - + ]: 4359609 : Assert(val.getType().isBoolean());
[ - - ]
398 [ + + ][ + + ]: 4359609 : if (!val.isConst() && val != d_none)
[ + + ]
399 : : {
400 : : // in the rare case that we evaluate to non-constant, we treat this as
401 : : // "some" here instead. This can happen if a term is congruent to an
402 : : // (unassigned) Boolean term.
403 : 193244 : val = d_some;
404 : : }
405 [ + - ]: 8719218 : Trace("ieval-state-debug") << "Notify quant constraint " << q.getId() << " "
406 : 4359609 : << p << " == " << val << std::endl;
407 [ - + ][ - + ]: 4359609 : Assert(d_numActiveQuant.get() > 0);
[ - - ]
408 : : // check whether we should set inactive
409 : 4359609 : bool setInactive = false;
410 : 4359609 : std::stringstream inactiveReason;
411 [ + + ]: 4359609 : if (isNone(val))
412 : : {
413 : : // a top-level constraint is "none", i.e. this instantiation will generate
414 : : // a predicate over new terms.
415 [ + + ]: 2179441 : if (d_tevMode == TermEvaluatorMode::CONFLICT
416 [ + + ]: 1089609 : || d_tevMode == TermEvaluatorMode::PROP)
417 : : {
418 : : // if we are looking for conflicts and propagations only, we are now
419 : : // inactive
420 [ - + ]: 1411167 : if (TraceIsOn("ieval"))
421 : : {
422 : 0 : inactiveReason << "none, req conflict/prop";
423 : : }
424 : 1411167 : setInactive = true;
425 : : }
426 : : else
427 : : {
428 : 768274 : qi.setNoConflict();
429 : : }
430 : : }
431 [ + + ]: 2180168 : else if (isSome(val))
432 : : {
433 : : // it has the "some" value, and we have any constraint, we remain
434 : : // active but are not strictly a conflict
435 [ + + ]: 193244 : if (d_tevMode == TermEvaluatorMode::CONFLICT)
436 : : {
437 : : // if we require conflicts, we are inactive now
438 [ - + ]: 54872 : if (TraceIsOn("ieval"))
439 : : {
440 : 0 : inactiveReason << "some, req conflict";
441 : : }
442 : 54872 : setInactive = true;
443 : : }
444 : : else
445 : : {
446 : 138372 : qi.setNoConflict();
447 : : }
448 : : }
449 : : else
450 : : {
451 [ - + ][ - + ]: 1986924 : Assert(val.isConst());
[ - - ]
452 : 1986924 : const std::map<TNode, bool>& cs = qi.getConstraints();
453 : 1986924 : std::map<TNode, bool>::const_iterator itm = cs.find(p);
454 [ - + ][ - + ]: 1986924 : Assert(itm != cs.end());
[ - - ]
455 [ + + ]: 1986924 : if (val.getConst<bool>() != itm->second)
456 : : {
457 : 1515069 : setInactive = true;
458 [ - + ]: 1515069 : if (TraceIsOn("ieval"))
459 : : {
460 : 0 : inactiveReason << "constraint-true";
461 : : }
462 : : }
463 : : else
464 : : {
465 [ + - ]: 943710 : Trace("ieval-state-debug")
466 : 471855 : << "...satisfied constraint " << p << std::endl;
467 : : }
468 : : }
469 : : // if we should set inactive, update qi and decrement d_numActiveQuant
470 [ + + ]: 4359609 : if (setInactive)
471 : : {
472 : 2981108 : qi.setFailureConstraint(p);
473 : 2981108 : setQuantInactive(qi);
474 [ + - ]: 5962216 : Trace("ieval") << " -> " << q << " inactive due to "
475 [ - + ][ - - ]: 2981108 : << inactiveReason.str() << ", from " << p << std::endl;
476 : : }
477 : : else
478 : : {
479 [ + - ]: 1378501 : Trace("ieval-state-debug") << "...still active" << std::endl;
480 : : }
481 : : // otherwise, we could have an instantiation, but we do not check for this
482 : : // here; instead this is handled based on watching the number of free
483 : : // variables assigned.
484 : 4359609 : }
485 : :
486 : 2981108 : void State::setQuantInactive(QuantInfo& qi)
487 : : {
488 [ + - ]: 2981108 : if (qi.isActive())
489 : : {
490 : 2981108 : qi.setActive(false);
491 [ - + ][ - + ]: 2981108 : Assert(d_numActiveQuant.get() > 0);
[ - - ]
492 : 2981108 : d_numActiveQuant = d_numActiveQuant - 1;
493 : : }
494 : 2981108 : }
495 : :
496 : 13367354 : TNode State::getNone() const { return d_none; }
497 : :
498 : 45478121 : bool State::isNone(TNode n) const { return n == d_none; }
499 : :
500 : 491883 : TNode State::getSome() const { return d_some; }
501 : :
502 : 11235505 : bool State::isSome(TNode n) const { return n == d_some; }
503 : :
504 : 633380 : Node State::doRewrite(Node n) const { return rewrite(n); }
505 : :
506 : 0 : bool State::isQuantActive(TNode q) const
507 : : {
508 : 0 : std::map<Node, QuantInfo>::const_iterator it = d_quantInfo.find(q);
509 : 0 : Assert(it != d_quantInfo.end());
510 : 0 : return it->second.isActive();
511 : : }
512 : :
513 : 5375653 : TNode State::evaluate(TNode n) const
514 : : {
515 [ + + ]: 5375653 : if (n.isConst())
516 : : {
517 : 2008704 : return n;
518 : : }
519 : : // all pattern terms should have been assigned pattern term info
520 [ - + ][ - + ]: 3366949 : Assert(!expr::hasFreeVar(n));
[ - - ]
521 : 3366949 : return d_tec->evaluateBase(*this, n);
522 : : }
523 : :
524 : 37843019 : TNode State::getValue(TNode p) const
525 : : {
526 [ + + ]: 37843019 : if (p.isConst())
527 : : {
528 : 5666643 : return p;
529 : : }
530 : 32176376 : std::map<Node, PatTermInfo>::const_iterator it = d_pInfo.find(p);
531 [ + + ]: 32176376 : if (it != d_pInfo.end())
532 : : {
533 : 25688058 : return it->second.d_eq;
534 : : }
535 : : // all pattern terms should have been assigned pattern term info
536 [ - + ][ - + ]: 6488318 : Assert(!expr::hasFreeVar(p));
[ - - ]
537 : 6488318 : return d_tec->evaluateBase(*this, p);
538 : : }
539 : :
540 : 0 : std::string State::toString() const
541 : : {
542 : 0 : std::stringstream ss;
543 : 0 : ss << "#patterns = " << d_pInfo.size() << std::endl;
544 : 0 : ss << "#freeVars = " << d_fvInfo.size() << std::endl;
545 : 0 : ss << "#quants = " << d_numActiveQuant.get() << " / " << d_quantInfo.size()
546 : 0 : << std::endl;
547 : 0 : return ss.str();
548 : 0 : }
549 : :
550 : 0 : std::string State::toStringSearch() const
551 : : {
552 : 0 : std::stringstream ss;
553 : 0 : ss << "activeQuants = " << d_numActiveQuant.get();
554 : 0 : return ss.str();
555 : 0 : }
556 : :
557 : 0 : std::string State::toStringDebugSearch() const
558 : : {
559 : 0 : std::stringstream ss;
560 : 0 : ss << "activeQuants = " << d_numActiveQuant.get() << "[";
561 : 0 : size_t nqc = 0;
562 [ - - ]: 0 : for (const std::pair<const Node, QuantInfo>& q : d_quantInfo)
563 : : {
564 [ - - ]: 0 : if (q.second.isActive())
565 : : {
566 : 0 : ss << " " << q.first.getId();
567 : 0 : nqc++;
568 : : }
569 : : }
570 : 0 : ss << " ]";
571 : : (void)nqc;
572 : 0 : Assert(nqc == d_numActiveQuant.get()) << "Active quant mismatch " << ss.str();
573 : 0 : return ss.str();
574 : 0 : }
575 : :
576 : : } // namespace ieval
577 : : } // namespace quantifiers
578 : : } // namespace theory
579 : : } // namespace cvc5::internal
|
