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 term database class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/term_database.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "expr/sort_to_term.h"
17 : : #include "options/base_options.h"
18 : : #include "options/printer_options.h"
19 : : #include "options/quantifiers_options.h"
20 : : #include "options/smt_options.h"
21 : : #include "options/theory_options.h"
22 : : #include "options/uf_options.h"
23 : : #include "proof/proof.h"
24 : : #include "proof/proof_generator.h"
25 : : #include "proof/proof_node_algorithm.h"
26 : : #include "proof/proof_node_manager.h"
27 : : #include "theory/quantifiers/ematching/trigger_term_info.h"
28 : : #include "theory/quantifiers/quantifiers_attributes.h"
29 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
30 : : #include "theory/quantifiers/quantifiers_registry.h"
31 : : #include "theory/quantifiers/quantifiers_state.h"
32 : : #include "theory/quantifiers/term_util.h"
33 : : #include "theory/rewriter.h"
34 : : #include "theory/uf/equality_engine.h"
35 : :
36 : : using namespace cvc5::internal::kind;
37 : : using namespace cvc5::context;
38 : :
39 : : namespace cvc5::internal {
40 : : namespace theory {
41 : : namespace quantifiers {
42 : :
43 : : /**
44 : : * A proof generator for proving simple congruence lemmas discovered by TermDb.
45 : : */
46 : : class DeqCongProofGenerator : protected EnvObj, public ProofGenerator
47 : : {
48 : : public:
49 : 19684 : DeqCongProofGenerator(Env& env) : EnvObj(env) {}
50 : 39340 : virtual ~DeqCongProofGenerator() {}
51 : : /**
52 : : * The lemma is of the form:
53 : : * (=> (and (= ti si) .. (= tj sj)) (= (f t1 ... tn) (f s1 ... sn)))
54 : : * which can be proven by a congruence step.
55 : : */
56 : 7 : std::shared_ptr<ProofNode> getProofFor(Node fact) override
57 : : {
58 [ - + ][ - + ]: 7 : Assert(fact.getKind() == Kind::IMPLIES);
[ - - ]
59 [ - + ][ - + ]: 7 : Assert(fact[1].getKind() == Kind::EQUAL);
[ - - ]
60 : 7 : Node a = fact[1][0];
61 : 7 : Node b = fact[1][1];
62 : 7 : std::vector<Node> assumps;
63 [ + + ]: 7 : if (fact[0].getKind() == Kind::AND)
64 : : {
65 : 3 : assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
66 : : }
67 : : else
68 : : {
69 : 4 : assumps.push_back(fact[0]);
70 : : }
71 : 14 : CDProof cdp(d_env);
72 [ - + ]: 7 : if (a.getOperator() != b.getOperator())
73 : : {
74 : : // TODO: wishue #158, likely corresponds to a higher-order term
75 : : // indexing conflict.
76 : 0 : cdp.addTrustedStep(fact, TrustId::QUANTIFIERS_PREPROCESS, {}, {});
77 : 0 : return cdp.getProofFor(fact);
78 : : }
79 [ - + ][ - + ]: 7 : Assert(a.getNumChildren() == b.getNumChildren());
[ - - ]
80 : 7 : std::vector<Node> cargs;
81 : 7 : ProofRule cr = expr::getCongRule(a, cargs);
82 : 7 : size_t nchild = a.getNumChildren();
83 : 7 : std::vector<Node> premises;
84 [ + + ]: 24 : for (size_t i = 0; i < nchild; i++)
85 : : {
86 : 34 : Node eq = a[i].eqNode(b[i]);
87 : 17 : premises.push_back(eq);
88 [ + + ]: 17 : if (a[i] == b[i])
89 : : {
90 : 14 : cdp.addStep(eq, ProofRule::REFL, {}, {a[i]});
91 : : }
92 : : else
93 : : {
94 [ - + ][ - + ]: 10 : Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end());
[ - - ]
95 : : }
96 : 17 : }
97 : 7 : cdp.addStep(fact[1], cr, premises, cargs);
98 : 7 : std::shared_ptr<ProofNode> pfn = cdp.getProofFor(fact[1]);
99 : 7 : return d_env.getProofNodeManager()->mkScope(pfn, assumps);
100 : 7 : }
101 : : /** identify */
102 : 0 : std::string identify() const override { return "DeqCongProofGenerator"; }
103 : : };
104 : :
105 : 50938 : TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
106 : : : QuantifiersUtil(env),
107 : 50938 : d_qstate(qs),
108 : 50938 : d_qim(nullptr),
109 : 50938 : d_qreg(qr),
110 : 50938 : d_processed(context()),
111 : 50938 : d_typeMap(context()),
112 : 50938 : d_ops(context()),
113 : 50938 : d_opMap(context()),
114 : 50938 : d_inactive_map(context()),
115 : 50938 : d_has_map(context()),
116 [ + + ]: 50938 : d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env)
117 : 203752 : : nullptr)
118 : : {
119 : 50938 : d_true = nodeManager()->mkConst(true);
120 : 50938 : d_false = nodeManager()->mkConst(false);
121 : 50938 : }
122 : :
123 : 99227 : TermDb::~TermDb() {}
124 : :
125 : 50938 : void TermDb::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; }
126 : :
127 : 54043 : void TermDb::registerQuantifier(Node q)
128 : : {
129 [ - + ][ - + ]: 54043 : Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
[ - - ]
130 [ + + ]: 172848 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
131 : : {
132 : 118805 : Node ic = d_qreg.getInstantiationConstant(q, i);
133 : 118805 : setTermInactive(ic);
134 : 118805 : }
135 : 54043 : }
136 : :
137 : 3465 : size_t TermDb::getNumOperators() const { return d_ops.size(); }
138 : :
139 : 13540 : Node TermDb::getOperator(size_t i) const
140 : : {
141 [ - + ][ - + ]: 13540 : Assert(i < d_ops.size());
[ - - ]
142 : 13540 : return d_ops[i];
143 : : }
144 : :
145 : : /** ground terms */
146 : 1862 : size_t TermDb::getNumGroundTerms(TNode f) const
147 : : {
148 : 1862 : NodeDbListMap::const_iterator it = d_opMap.find(f);
149 [ + - ]: 1862 : if (it != d_opMap.end())
150 : : {
151 : 1862 : return it->second->d_list.size();
152 : : }
153 : 0 : return 0;
154 : : }
155 : :
156 : 8947 : Node TermDb::getGroundTerm(TNode f, size_t i) const
157 : : {
158 : 8947 : NodeDbListMap::const_iterator it = d_opMap.find(f);
159 [ + - ]: 8947 : if (it != d_opMap.end())
160 : : {
161 [ - + ][ - + ]: 8947 : Assert(i < it->second->d_list.size());
[ - - ]
162 : 8947 : return it->second->d_list[i];
163 : : }
164 : 0 : DebugUnhandled();
165 : : return Node::null();
166 : : }
167 : :
168 : 966302 : DbList* TermDb::getGroundTermList(TNode f) const
169 : : {
170 : 966302 : NodeDbListMap::const_iterator it = d_opMap.find(f);
171 [ + + ]: 966302 : if (it != d_opMap.end())
172 : : {
173 : 943708 : return it->second.get();
174 : : }
175 : 22594 : return nullptr;
176 : : }
177 : :
178 : 1538 : size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const
179 : : {
180 : 1538 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
181 [ + + ]: 1538 : if (it != d_typeMap.end())
182 : : {
183 : 1475 : return it->second->d_list.size();
184 : : }
185 : 63 : return 0;
186 : : }
187 : :
188 : 58134 : Node TermDb::getTypeGroundTerm(TypeNode tn, size_t i) const
189 : : {
190 : 58134 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
191 [ + - ]: 58134 : if (it != d_typeMap.end())
192 : : {
193 [ - + ][ - + ]: 58134 : Assert(i < it->second->d_list.size());
[ - - ]
194 : 58134 : return it->second->d_list[i];
195 : : }
196 : 0 : DebugUnhandled();
197 : : return Node::null();
198 : : }
199 : :
200 : 8064 : Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
201 : : {
202 : 8064 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
203 [ + + ]: 8064 : if (it != d_typeMap.end())
204 : : {
205 [ - + ][ - + ]: 2760 : Assert(!it->second->d_list.empty());
[ - - ]
206 [ + + ]: 2760 : if (!reqVar)
207 : : {
208 : 1696 : return it->second->d_list[0];
209 : : }
210 [ + + ]: 2337 : for (const Node& v : it->second->d_list)
211 : : {
212 [ + + ]: 2158 : if (v.isVar())
213 : : {
214 : 885 : return v;
215 : : }
216 : : }
217 : : }
218 : 5483 : return getOrMakeTypeFreshVariable(tn);
219 : : }
220 : :
221 : 5483 : Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
222 : : {
223 : 5483 : std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn);
224 [ + + ]: 5483 : if (it == d_type_fv.end())
225 : : {
226 : 1706 : NodeManager* nm = nodeManager();
227 : 1706 : SkolemManager* sm = nm->getSkolemManager();
228 : 1706 : std::vector<Node> cacheVals;
229 : 1706 : cacheVals.push_back(nm->mkConst(SortToTerm(tn)));
230 : 1706 : Node k = sm->mkSkolemFunction(SkolemId::GROUND_TERM, cacheVals);
231 [ + - ]: 3412 : Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
232 : 1706 : << std::endl;
233 [ - + ]: 1706 : if (options().quantifiers.instMaxLevel != -1)
234 : : {
235 : 0 : QuantAttributes::setInstantiationLevelAttr(k, 0);
236 : : }
237 : 1706 : d_type_fv[tn] = k;
238 : 1706 : return k;
239 : 1706 : }
240 : 3777 : return it->second;
241 : : }
242 : :
243 : 154569385 : Node TermDb::getMatchOperator(TNode n)
244 : : {
245 : 154569385 : Kind k = n.getKind();
246 : : // datatype operators may be parametric, always assume they are
247 [ + + ][ + + ]: 154569385 : if (k == Kind::SELECT || k == Kind::STORE || k == Kind::SET_UNION
[ + + ]
248 [ + + ][ + - ]: 154427152 : || k == Kind::SET_INTER || k == Kind::SET_SUBSET || k == Kind::SET_MINUS
[ + + ]
249 [ + + ][ + + ]: 154423754 : || k == Kind::SET_MEMBER || k == Kind::SET_SINGLETON
250 [ + + ][ + + ]: 154364838 : || k == Kind::APPLY_SELECTOR || k == Kind::APPLY_TESTER
251 [ + + ][ + + ]: 153699935 : || k == Kind::SEP_PTO || k == Kind::HO_APPLY || k == Kind::SEQ_NTH
[ + + ]
252 [ + + ][ + + ]: 153652469 : || k == Kind::STRING_LENGTH || k == Kind::BITVECTOR_UBV_TO_INT
253 [ + + ]: 153574665 : || k == Kind::INT_TO_BITVECTOR)
254 : : {
255 : : // since it is parametric, use a particular one as op
256 : 994756 : TypeNode tn = n[0].getType();
257 : 994756 : Node op = n.getOperator();
258 : : std::map<Node, std::map<TypeNode, Node> >::iterator ito =
259 : 994756 : d_par_op_map.find(op);
260 [ + + ]: 994756 : if (ito != d_par_op_map.end())
261 : : {
262 : 970636 : std::map<TypeNode, Node>::iterator it = ito->second.find(tn);
263 [ + + ]: 970636 : if (it != ito->second.end())
264 : : {
265 : 969193 : return it->second;
266 : : }
267 : : }
268 [ + - ][ - + ]: 51126 : Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator()
[ - - ]
269 : 25563 : << ", " << tn << " : " << n << std::endl;
270 : 25563 : d_par_op_map[op][tn] = n;
271 : 25563 : return n;
272 : 994756 : }
273 [ + + ]: 153574629 : else if (inst::TriggerTermInfo::isAtomicTriggerKind(k))
274 : : {
275 : 145937416 : return n.getOperator();
276 : : }
277 : 7637213 : return Node::null();
278 : : }
279 : :
280 : 0 : bool TermDb::isMatchable(TNode n) { return !getMatchOperator(n).isNull(); }
281 : :
282 : 10911479 : void TermDb::eqNotifyMerge(TNode t1, TNode t2)
283 : : {
284 [ + + ]: 10911479 : if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
285 : : {
286 : : // Since the equivalence class of t1 and t2 merged, we now consider these
287 : : // two terms to be relevant in the current context. Note technically this
288 : : // does not mean that these terms are in assertions, e.g. t1 and t2 may be
289 : : // merged via congruence if a=b is an assertion and f(a) and f(b) are
290 : : // preregistered terms. Nevertheless this is a close approximation of the
291 : : // terms we care about. Since we are listening to the master equality
292 : : // engine notifications, this also includes internally introduced terms
293 : : // (if any) introduced by theory solvers.
294 : 10704338 : setHasTerm(t1);
295 : 10704338 : setHasTerm(t2);
296 : : }
297 : 10911479 : }
298 : :
299 : 5048272 : void TermDb::addTerm(Node n)
300 : : {
301 [ + + ]: 5048272 : if (d_processed.find(n) != d_processed.end())
302 : : {
303 : 2909075 : return;
304 : : }
305 : 2139197 : d_processed.insert(n);
306 [ + + ]: 2139197 : if (!TermUtil::hasInstConstAttr(n))
307 : : {
308 [ + - ]: 1980445 : Trace("term-db-debug") << "register term : " << n << std::endl;
309 : 1980445 : DbList* dlt = getOrMkDbListForType(n.getType());
310 : 1980445 : dlt->d_list.push_back(n);
311 : : // if this is an atomic trigger, consider adding it
312 : 1980445 : Node op = getMatchOperator(n);
313 [ + + ]: 1980445 : if (!op.isNull())
314 : : {
315 [ + - ]: 921715 : Trace("term-db") << "register term in db " << n << std::endl;
316 [ + - ]: 921715 : Trace("term-db-debug") << " match operator is : " << op << std::endl;
317 : 921715 : DbList* dlo = getOrMkDbListForOp(op);
318 : 921715 : dlo->d_list.push_back(n);
319 : : // If we are higher-order, we may need to register more terms.
320 : 921715 : addTermInternal(n);
321 : : }
322 : 1980445 : }
323 : : else
324 : : {
325 : 158752 : setTermInactive(n);
326 : : }
327 [ + + ]: 2139197 : if (!n.isClosure())
328 : : {
329 [ + + ]: 5252798 : for (const Node& nc : n)
330 : : {
331 : 3113667 : addTerm(nc);
332 : 3113667 : }
333 : : }
334 : : }
335 : :
336 : 1980445 : DbList* TermDb::getOrMkDbListForType(TypeNode tn)
337 : : {
338 : 1980445 : TypeNodeDbListMap::iterator it = d_typeMap.find(tn);
339 [ + + ]: 1980445 : if (it != d_typeMap.end())
340 : : {
341 : 1913718 : return it->second.get();
342 : : }
343 : 66727 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
344 : 66727 : d_typeMap.insert(tn, dl);
345 : 66727 : return dl.get();
346 : 66727 : }
347 : :
348 : 1024592 : DbList* TermDb::getOrMkDbListForOp(TNode op)
349 : : {
350 : 1024592 : NodeDbListMap::iterator it = d_opMap.find(op);
351 [ + + ]: 1024592 : if (it != d_opMap.end())
352 : : {
353 : 851737 : return it->second.get();
354 : : }
355 : 172855 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
356 : 172855 : d_opMap.insert(op, dl);
357 [ - + ][ - + ]: 172855 : Assert(op.getKind() != Kind::BOUND_VARIABLE);
[ - - ]
358 : 172855 : d_ops.push_back(op);
359 : 172855 : return dl.get();
360 : 172855 : }
361 : :
362 : 1993574 : void TermDb::computeArgReps(TNode n)
363 : : {
364 [ + + ]: 1993574 : if (d_arg_reps.find(n) == d_arg_reps.end())
365 : : {
366 : 1123724 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
367 : 1123724 : std::vector<TNode>& tars = d_arg_reps[n];
368 [ + + ]: 3330111 : for (const TNode& nc : n)
369 : : {
370 [ + - ][ + - ]: 4412774 : TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
[ - - ]
371 : 2206387 : tars.emplace_back(r);
372 : 2206387 : }
373 : : }
374 : 1993574 : }
375 : :
376 : 8422432 : void TermDb::computeUfEqcTerms(TNode f)
377 : : {
378 [ - + ][ - + ]: 8422432 : Assert(f == getOperatorRepresentative(f));
[ - - ]
379 [ + + ]: 8422432 : if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
380 : : {
381 : 8324643 : return;
382 : : }
383 [ + - ]: 97789 : Trace("term-db-debug") << "computeUfEqcTerms for " << f << std::endl;
384 : 97789 : TNodeTrie& tnt = d_func_map_eqc_trie[f];
385 : 97789 : tnt.clear();
386 : : // get the matchable operators in the equivalence class of f
387 : 97789 : std::vector<TNode> ops;
388 : 97789 : getOperatorsFor(f, ops);
389 : 97789 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
390 [ + + ]: 195767 : for (TNode ff : ops)
391 : : {
392 : 97978 : DbList* dbl = getOrMkDbListForOp(ff);
393 [ + + ]: 1173182 : for (const Node& n : dbl->d_list)
394 : : {
395 [ + + ][ + + ]: 1075204 : if (hasTermCurrent(n) && isTermActive(n))
[ + + ][ + + ]
[ - - ]
396 : : {
397 : 895442 : computeArgReps(n);
398 [ + - ][ + - ]: 1790884 : TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
[ - - ]
399 : 895442 : tnt.d_data[r].addTerm(n, d_arg_reps[n]);
400 [ + - ]: 1790884 : Trace("term-db-debug")
401 : 0 : << "Adding term " << n << " to eqc " << r
402 [ - + ][ - - ]: 895442 : << " with arg reps : " << d_arg_reps[n] << std::endl;
403 : 895442 : }
404 : : }
405 : 97978 : }
406 : 97789 : }
407 : :
408 : 31339196 : void TermDb::computeUfTerms(TNode f)
409 : : {
410 [ + + ]: 31339196 : if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
411 : : {
412 : : // already computed
413 : 31226804 : return;
414 : : }
415 [ - + ][ - + ]: 112447 : Assert(f == getOperatorRepresentative(f));
[ - - ]
416 : 112447 : d_op_nonred_count[f] = 0;
417 : : // get the matchable operators in the equivalence class of f
418 : 112447 : std::vector<TNode> ops;
419 : 112447 : getOperatorsFor(f, ops);
420 [ + - ]: 112447 : Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
421 : 112447 : unsigned congruentCount = 0;
422 : 112447 : unsigned nonCongruentCount = 0;
423 : 112447 : unsigned alreadyCongruentCount = 0;
424 : 112447 : unsigned relevantCount = 0;
425 : 112447 : NodeManager* nm = nodeManager();
426 [ + + ]: 225599 : for (TNode ff : ops)
427 : : {
428 : 113207 : NodeDbListMap::iterator it = d_opMap.find(ff);
429 [ + + ]: 113207 : if (it == d_opMap.end())
430 : : {
431 : : // no terms for this operator
432 : 16703 : continue;
433 : : }
434 [ + - ]: 96504 : Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
435 [ + + ]: 1366304 : for (const Node& n : it->second->d_list)
436 : : {
437 : : // to be added to term index, term must be relevant, and exist in EE
438 [ + + ][ - + ]: 1269855 : if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
[ + + ][ + + ]
[ - - ]
439 : : {
440 [ + - ]: 88872 : Trace("term-db-debug") << n << " is not relevant." << std::endl;
441 : 432599 : continue;
442 : : }
443 : :
444 : 1180983 : relevantCount++;
445 [ + + ]: 1180983 : if (!isTermActive(n))
446 : : {
447 [ + - ]: 82851 : Trace("term-db-debug") << n << " is already redundant." << std::endl;
448 : 82851 : alreadyCongruentCount++;
449 : 82851 : continue;
450 : : }
451 : :
452 : 1098132 : computeArgReps(n);
453 : 1098132 : std::vector<TNode>& reps = d_arg_reps[n];
454 [ + - ]: 2196264 : Trace("term-db-debug")
455 : 1098132 : << "Adding term " << n << " with arg reps : " << reps << std::endl;
456 [ - + ][ - + ]: 1098132 : Assert(d_qstate.hasTerm(n));
[ - - ]
457 [ + - ]: 2196264 : Trace("term-db-debug")
458 : 1098132 : << " and value : " << d_qstate.getRepresentative(n) << std::endl;
459 : 2196264 : Node at = d_func_map_trie[f].addOrGetTerm(n, reps);
460 [ - + ][ - + ]: 1098132 : Assert(d_qstate.hasTerm(at));
[ - - ]
461 [ + - ]: 1098132 : Trace("term-db-debug2") << "...add term returned " << at << std::endl;
462 : 1098132 : if (at != n && d_qstate.areEqual(at, n))
463 : : {
464 : 260876 : setTermInactive(n);
465 [ + - ]: 260876 : Trace("term-db-debug") << n << " is redundant." << std::endl;
466 : 260876 : congruentCount++;
467 : 260876 : continue;
468 : : }
469 : 837256 : std::vector<Node> antec;
470 [ + + ]: 837256 : if (checkCongruentDisequal(at, n, antec))
471 : : {
472 [ - + ][ - + ]: 55 : Assert(at.getNumChildren() == n.getNumChildren());
[ - - ]
473 [ + + ]: 179 : for (size_t k = 0, size = at.getNumChildren(); k < size; k++)
474 : : {
475 [ + + ]: 124 : if (at[k] != n[k])
476 : : {
477 : 75 : antec.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]));
478 [ - + ][ - + ]: 75 : Assert(d_qstate.areEqual(at[k], n[k]));
[ - - ]
479 : : }
480 : : }
481 : 220 : Node lem = nm->mkNode(Kind::IMPLIES, {nm->mkAnd(antec), at.eqNode(n)});
482 [ - + ]: 55 : if (TraceIsOn("term-db-lemma"))
483 : : {
484 [ - - ]: 0 : Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
485 : 0 : << n << "!!!!" << std::endl;
486 [ - - ]: 0 : if (!d_qstate.getValuation().needCheck())
487 : : {
488 [ - - ]: 0 : Trace("term-db-lemma")
489 : 0 : << " all theories passed with no lemmas." << std::endl;
490 : : // we should be a full effort check, prior to theory combination
491 : : }
492 [ - - ]: 0 : Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
493 : : }
494 [ + + ]: 55 : d_qim->addPendingLemma(lem,
495 : : InferenceId::QUANTIFIERS_TDB_DEQ_CONG,
496 : : LemmaProperty::NONE,
497 : 55 : d_dcproof.get());
498 : 55 : d_qstate.notifyInConflict();
499 : 55 : return;
500 : 55 : }
501 : : // Also populate relevant domain. Note this only will add if the term is
502 : : // non-congruent, which is why we wait to compute it here.
503 : 837201 : std::vector<std::vector<TNode> >& frds = d_fmapRelDom[f];
504 : 837201 : size_t rsize = reps.size();
505 : : // ensure the relevant domain vector has been allocated
506 : 837201 : frds.resize(rsize);
507 [ + + ]: 2576848 : for (size_t i = 0; i < rsize; i++)
508 : : {
509 : 1739647 : TNode r = reps[i];
510 : 1739647 : std::vector<TNode>& frd = frds[i];
511 [ + + ]: 1739647 : if (std::find(frd.begin(), frd.end(), r) == frd.end())
512 : : {
513 : 721221 : frd.push_back(r);
514 : : }
515 : 1739647 : }
516 : 837201 : nonCongruentCount++;
517 : 837201 : d_op_nonred_count[f]++;
518 [ + + ][ + + ]: 1098187 : }
[ + ]
519 [ - + ]: 96449 : if (TraceIsOn("tdb"))
520 : : {
521 [ - - ]: 0 : Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
522 : 0 : << " / ";
523 [ - - ]: 0 : Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
524 : 0 : << (nonCongruentCount + congruentCount
525 : 0 : + alreadyCongruentCount)
526 : 0 : << " / ";
527 [ - - ]: 0 : Trace("tdb") << relevantCount << " / " << it->second->d_list.size()
528 : 0 : << std::endl;
529 : : }
530 [ + + ][ + ]: 113207 : }
531 [ + + ]: 112447 : }
532 : :
533 : 46914030 : Node TermDb::getOperatorRepresentative(TNode op) const { return op; }
534 : :
535 : 785436 : bool TermDb::checkCongruentDisequal(TNode a,
536 : : TNode b,
537 : : CVC5_UNUSED std::vector<Node>& exp)
538 : : {
539 [ + + ]: 785436 : if (d_qstate.areDisequal(a, b))
540 : : {
541 : 48 : return true;
542 : : }
543 : 785388 : return false;
544 : : }
545 : :
546 : 13106006 : bool TermDb::inRelevantDomain(TNode f, size_t i, TNode r)
547 : : {
548 : : // notice if we are not higher-order, getOperatorRepresentative is a no-op
549 : 13106006 : f = getOperatorRepresentative(f);
550 : 13106006 : computeUfTerms(f);
551 : 13106006 : Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
552 : : || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
553 : : std::map<Node, std::vector<std::vector<TNode> > >::const_iterator it =
554 : 13106006 : d_fmapRelDom.find(f);
555 [ + + ]: 13106006 : if (it != d_fmapRelDom.end())
556 : : {
557 [ - + ][ - + ]: 12808047 : Assert(i < it->second.size());
[ - - ]
558 : 12808047 : const std::vector<TNode>& rd = it->second[i];
559 : 12808047 : return std::find(rd.begin(), rd.end(), r) != rd.end();
560 : : }
561 : 297959 : return false;
562 : : }
563 : :
564 : 8407352 : bool TermDb::isTermActive(Node n)
565 : : {
566 : 8407352 : return d_inactive_map.find(n) == d_inactive_map.end();
567 : : // return !n.getAttribute(NoMatchAttribute());
568 : : }
569 : :
570 : 538433 : void TermDb::setTermInactive(Node n) { d_inactive_map[n] = true; }
571 : :
572 : 9579591 : bool TermDb::hasTermCurrent(const Node& n, bool useMode) const
573 : : {
574 [ - + ]: 9579591 : if (!useMode)
575 : : {
576 : 0 : return d_has_map.find(n) != d_has_map.end();
577 : : }
578 : : // some assertions are not sent to EE
579 [ + + ]: 9579591 : if (options().quantifiers.termDbMode == options::TermDbMode::ALL)
580 : : {
581 : 118365 : return true;
582 : : }
583 [ + - ]: 9461226 : else if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
584 : : {
585 : 9461226 : return d_has_map.find(n) != d_has_map.end();
586 : : }
587 : 0 : DebugUnhandled() << "TermDb::hasTermCurrent: Unknown termDbMode : "
588 : 0 : << options().quantifiers.termDbMode;
589 : : return false;
590 : : }
591 : :
592 : 1470 : bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
593 : : {
594 [ + + ]: 1470 : if (options().quantifiers.instMaxLevel != -1)
595 : : {
596 : : uint64_t level;
597 [ + - ]: 1114 : if (QuantAttributes::getInstantiationLevel(n, level))
598 : : {
599 : : int64_t fml =
600 [ - + ][ + - ]: 1114 : f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
[ - - ]
601 [ - + ]: 1114 : unsigned ml = fml >= 0 ? fml : options().quantifiers.instMaxLevel;
602 : :
603 [ - + ]: 1114 : if (level > ml)
604 : : {
605 [ - - ]: 0 : Trace("inst-add-debug")
606 : 0 : << "Term " << n << " has instantiation level " << level;
607 [ - - ]: 0 : Trace("inst-add-debug")
608 : 0 : << ", which is more than maximum allowed level " << ml
609 : 0 : << " for this quantified formula." << std::endl;
610 : 0 : return false;
611 : : }
612 : : }
613 : : else
614 : : {
615 [ - - ]: 0 : Trace("inst-add-debug")
616 : 0 : << "Term " << n << " does not have an instantiation level."
617 : 0 : << std::endl;
618 : 0 : return false;
619 : : }
620 : : }
621 : : // it cannot have instantiation constants, which originate from
622 : : // counterexample-guided instantiation strategies.
623 : 1470 : return !TermUtil::hasInstConstAttr(n);
624 : : }
625 : :
626 : 356 : Node TermDb::getEligibleTermInEqc(TNode r)
627 : : {
628 [ + - ]: 356 : if (isTermEligibleForInstantiation(r, TNode::null()))
629 : : {
630 : 356 : return r;
631 : : }
632 : : else
633 : : {
634 : 0 : std::map<Node, Node>::iterator it = d_term_elig_eqc.find(r);
635 [ - - ]: 0 : if (it == d_term_elig_eqc.end())
636 : : {
637 : 0 : Node h;
638 : 0 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
639 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
640 [ - - ]: 0 : while (!eqc_i.isFinished())
641 : : {
642 : 0 : TNode n = (*eqc_i);
643 : 0 : ++eqc_i;
644 [ - - ]: 0 : if (isTermEligibleForInstantiation(n, TNode::null()))
645 : : {
646 : 0 : h = n;
647 : 0 : break;
648 : : }
649 [ - - ]: 0 : }
650 : 0 : d_term_elig_eqc[r] = h;
651 : 0 : return h;
652 : 0 : }
653 : : else
654 : : {
655 : 0 : return it->second;
656 : : }
657 : : }
658 : : }
659 : :
660 : 63487 : bool TermDb::finishResetInternal(CVC5_UNUSED Theory::Effort e)
661 : : {
662 : : // do nothing
663 : 63487 : return true;
664 : : }
665 : :
666 : 824713 : void TermDb::addTermInternal(CVC5_UNUSED Node n)
667 : : {
668 : : // do nothing
669 : 824713 : }
670 : :
671 : 196380 : void TermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
672 : : {
673 : 196380 : ops.push_back(f);
674 : 196380 : }
675 : :
676 : 39504389 : void TermDb::setHasTerm(Node n)
677 : : {
678 [ + - ]: 39504389 : Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
679 : 39504389 : std::vector<TNode> visit;
680 : 39504389 : TNode cur;
681 : 39504389 : visit.push_back(n);
682 : : do
683 : : {
684 : 78763866 : cur = visit.back();
685 : 78763866 : visit.pop_back();
686 [ + + ]: 78763866 : if (d_has_map.find(cur) == d_has_map.end())
687 : : {
688 : 23969552 : d_has_map.insert(cur);
689 : 23969552 : visit.insert(visit.end(), cur.begin(), cur.end());
690 : : }
691 [ + + ]: 78763866 : } while (!visit.empty());
692 : 39504389 : }
693 : :
694 : 40005 : void TermDb::presolve() {}
695 : :
696 : 68843 : bool TermDb::reset(Theory::Effort effort)
697 : : {
698 : 68843 : d_op_nonred_count.clear();
699 : 68843 : d_arg_reps.clear();
700 : 68843 : d_func_map_trie.clear();
701 : 68843 : d_func_map_eqc_trie.clear();
702 : 68843 : d_fmapRelDom.clear();
703 : :
704 [ - + ][ - + ]: 68843 : Assert(d_qstate.getEqualityEngine()->consistent());
[ - - ]
705 : :
706 : : // compute has map
707 [ + + ]: 68843 : if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
708 : : {
709 : 68591 : d_term_elig_eqc.clear();
710 : 68591 : const LogicInfo& logicInfo = d_qstate.getLogicInfo();
711 [ + + ]: 1028865 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
712 : : {
713 [ + + ]: 960274 : if (!logicInfo.isTheoryEnabled(theoryId))
714 : : {
715 : 307502 : continue;
716 : : }
717 : : // Note that we have already marked all terms that have participated in
718 : : // equality engine merges as relevant. We go back and ensure all
719 : : // remaining terms that appear in assertions are marked relevant here
720 : : // in case there are terms appearing in assertions but not in the master
721 : : // equality engine.
722 : 652772 : for (context::CDList<Assertion>::const_iterator
723 : 652772 : it = d_qstate.factsBegin(theoryId),
724 : 652772 : it_end = d_qstate.factsEnd(theoryId);
725 [ + + ]: 18748485 : it != it_end;
726 : 18095713 : ++it)
727 : : {
728 : 18095713 : setHasTerm((*it).d_assertion);
729 : : }
730 : : }
731 : : }
732 : : // finish reset
733 : 68843 : return finishResetInternal(effort);
734 : : }
735 : :
736 : 51347 : TNodeTrie* TermDb::getTermArgTrie(Node f)
737 : : {
738 : 51347 : f = getOperatorRepresentative(f);
739 : 51347 : computeUfTerms(f);
740 : 51347 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
741 [ + + ]: 51347 : if (itut != d_func_map_trie.end())
742 : : {
743 : 34388 : return &itut->second;
744 : : }
745 : : else
746 : : {
747 : 16959 : return nullptr;
748 : : }
749 : : }
750 : :
751 : 8422432 : TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
752 : : {
753 : 8422432 : f = getOperatorRepresentative(f);
754 : 8422432 : computeUfEqcTerms(f);
755 : 8422432 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
756 [ - + ]: 8422432 : if (itut == d_func_map_eqc_trie.end())
757 : : {
758 : 0 : return nullptr;
759 : : }
760 : : else
761 : : {
762 [ + + ]: 8422432 : if (eqc.isNull())
763 : : {
764 : 2191034 : return &itut->second;
765 : : }
766 : : else
767 : : {
768 : : std::map<TNode, TNodeTrie>::iterator itute =
769 : 6231398 : itut->second.d_data.find(eqc);
770 [ + + ]: 6231398 : if (itute != itut->second.d_data.end())
771 : : {
772 : 3416122 : return &itute->second;
773 : : }
774 : : else
775 : : {
776 : 2815276 : return nullptr;
777 : : }
778 : : }
779 : : }
780 : : }
781 : :
782 : 0 : TNode TermDb::getCongruentTerm(Node f, Node n)
783 : : {
784 : 0 : f = getOperatorRepresentative(f);
785 : 0 : computeUfTerms(f);
786 : 0 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
787 [ - - ]: 0 : if (itut != d_func_map_trie.end())
788 : : {
789 : 0 : computeArgReps(n);
790 : 0 : return itut->second.existsTerm(d_arg_reps[n]);
791 : : }
792 : 0 : return TNode::null();
793 : : }
794 : :
795 : 18181843 : TNode TermDb::getCongruentTerm(Node f, const std::vector<TNode>& args)
796 : : {
797 : 18181843 : f = getOperatorRepresentative(f);
798 : 18181843 : computeUfTerms(f);
799 : 18181843 : return d_func_map_trie[f].existsTerm(args);
800 : : }
801 : :
802 : : } // namespace quantifiers
803 : : } // namespace theory
804 : : } // namespace cvc5::internal
|
