Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of term database class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/term_database.h"
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "expr/sort_to_term.h"
20 : : #include "options/base_options.h"
21 : : #include "options/printer_options.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "options/smt_options.h"
24 : : #include "options/theory_options.h"
25 : : #include "options/uf_options.h"
26 : : #include "proof/proof.h"
27 : : #include "proof/proof_generator.h"
28 : : #include "proof/proof_node_algorithm.h"
29 : : #include "proof/proof_node_manager.h"
30 : : #include "theory/quantifiers/ematching/trigger_term_info.h"
31 : : #include "theory/quantifiers/quantifiers_attributes.h"
32 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
33 : : #include "theory/quantifiers/quantifiers_registry.h"
34 : : #include "theory/quantifiers/quantifiers_state.h"
35 : : #include "theory/quantifiers/term_util.h"
36 : : #include "theory/rewriter.h"
37 : : #include "theory/uf/equality_engine.h"
38 : :
39 : : using namespace cvc5::internal::kind;
40 : : using namespace cvc5::context;
41 : :
42 : : namespace cvc5::internal {
43 : : namespace theory {
44 : : namespace quantifiers {
45 : :
46 : : /**
47 : : * A proof generator for proving simple congruence lemmas discovered by TermDb.
48 : : */
49 : : class DeqCongProofGenerator : protected EnvObj, public ProofGenerator
50 : : {
51 : : public:
52 : 18897 : DeqCongProofGenerator(Env& env) : EnvObj(env) {}
53 : 37766 : virtual ~DeqCongProofGenerator() {}
54 : : /**
55 : : * The lemma is of the form:
56 : : * (=> (and (= ti si) .. (= tj sj)) (= (f t1 ... tn) (f s1 ... sn)))
57 : : * which can be proven by a congruence step.
58 : : */
59 : 7 : std::shared_ptr<ProofNode> getProofFor(Node fact) override
60 : : {
61 [ - + ][ - + ]: 7 : Assert(fact.getKind() == Kind::IMPLIES);
[ - - ]
62 [ - + ][ - + ]: 7 : Assert(fact[1].getKind() == Kind::EQUAL);
[ - - ]
63 : 7 : Node a = fact[1][0];
64 : 7 : Node b = fact[1][1];
65 : 7 : std::vector<Node> assumps;
66 [ + + ]: 7 : if (fact[0].getKind() == Kind::AND)
67 : : {
68 : 3 : assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
69 : : }
70 : : else
71 : : {
72 : 4 : assumps.push_back(fact[0]);
73 : : }
74 : 14 : CDProof cdp(d_env);
75 [ - + ]: 7 : if (a.getOperator() != b.getOperator())
76 : : {
77 : : // TODO: wishue #158, likely corresponds to a higher-order term
78 : : // indexing conflict.
79 : 0 : cdp.addTrustedStep(fact, TrustId::QUANTIFIERS_PREPROCESS, {}, {});
80 : 0 : return cdp.getProofFor(fact);
81 : : }
82 [ - + ][ - + ]: 7 : Assert(a.getNumChildren() == b.getNumChildren());
[ - - ]
83 : 7 : std::vector<Node> cargs;
84 : 7 : ProofRule cr = expr::getCongRule(a, cargs);
85 : 7 : size_t nchild = a.getNumChildren();
86 : 7 : std::vector<Node> premises;
87 [ + + ]: 24 : for (size_t i = 0; i < nchild; i++)
88 : : {
89 : 34 : Node eq = a[i].eqNode(b[i]);
90 : 17 : premises.push_back(eq);
91 [ + + ]: 17 : if (a[i] == b[i])
92 : : {
93 : 14 : cdp.addStep(eq, ProofRule::REFL, {}, {a[i]});
94 : : }
95 : : else
96 : : {
97 [ - + ][ - + ]: 10 : Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end());
[ - - ]
98 : : }
99 : 17 : }
100 : 7 : cdp.addStep(fact[1], cr, premises, cargs);
101 : 7 : std::shared_ptr<ProofNode> pfn = cdp.getProofFor(fact[1]);
102 : 7 : return d_env.getProofNodeManager()->mkScope(pfn, assumps);
103 : 7 : }
104 : : /** identify */
105 : 0 : std::string identify() const override { return "DeqCongProofGenerator"; }
106 : : };
107 : :
108 : 49953 : TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
109 : : : QuantifiersUtil(env),
110 : 49953 : d_qstate(qs),
111 : 49953 : d_qim(nullptr),
112 : 49953 : d_qreg(qr),
113 : 49953 : d_processed(context()),
114 : 49953 : d_typeMap(context()),
115 : 49953 : d_ops(context()),
116 : 49953 : d_opMap(context()),
117 : 49953 : d_inactive_map(context()),
118 : 49953 : d_has_map(context()),
119 [ + + ]: 49953 : d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env)
120 : 199812 : : nullptr)
121 : : {
122 : 49953 : d_true = nodeManager()->mkConst(true);
123 : 49953 : d_false = nodeManager()->mkConst(false);
124 : 49953 : }
125 : :
126 : 98017 : TermDb::~TermDb(){
127 : :
128 : 98017 : }
129 : :
130 : 49953 : void TermDb::finishInit(QuantifiersInferenceManager* qim)
131 : : {
132 : 49953 : d_qim = qim;
133 : 49953 : }
134 : :
135 : 53394 : void TermDb::registerQuantifier( Node q ) {
136 [ - + ][ - + ]: 53394 : Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
[ - - ]
137 [ + + ]: 171504 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
138 : : {
139 : 118110 : Node ic = d_qreg.getInstantiationConstant(q, i);
140 : 118110 : setTermInactive( ic );
141 : 118110 : }
142 : 53394 : }
143 : :
144 : 3162 : size_t TermDb::getNumOperators() const { return d_ops.size(); }
145 : :
146 : 12098 : Node TermDb::getOperator(size_t i) const
147 : : {
148 [ - + ][ - + ]: 12098 : Assert(i < d_ops.size());
[ - - ]
149 : 12098 : return d_ops[i];
150 : : }
151 : :
152 : : /** ground terms */
153 : 1834 : size_t TermDb::getNumGroundTerms(TNode f) const
154 : : {
155 : 1834 : NodeDbListMap::const_iterator it = d_opMap.find(f);
156 [ + - ]: 1834 : if (it != d_opMap.end())
157 : : {
158 : 1834 : return it->second->d_list.size();
159 : : }
160 : 0 : return 0;
161 : : }
162 : :
163 : 8884 : Node TermDb::getGroundTerm(TNode f, size_t i) const
164 : : {
165 : 8884 : NodeDbListMap::const_iterator it = d_opMap.find(f);
166 [ + - ]: 8884 : if (it != d_opMap.end())
167 : : {
168 [ - + ][ - + ]: 8884 : Assert(i < it->second->d_list.size());
[ - - ]
169 : 8884 : return it->second->d_list[i];
170 : : }
171 : 0 : DebugUnhandled();
172 : : return Node::null();
173 : : }
174 : :
175 : 1009124 : DbList* TermDb::getGroundTermList(TNode f) const
176 : : {
177 : 1009124 : NodeDbListMap::const_iterator it = d_opMap.find(f);
178 [ + + ]: 1009124 : if (it != d_opMap.end())
179 : : {
180 : 986819 : return it->second.get();
181 : : }
182 : 22305 : return nullptr;
183 : : }
184 : :
185 : 1468 : size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const
186 : : {
187 : 1468 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
188 [ + + ]: 1468 : if (it != d_typeMap.end())
189 : : {
190 : 1405 : return it->second->d_list.size();
191 : : }
192 : 63 : return 0;
193 : : }
194 : :
195 : 57784 : Node TermDb::getTypeGroundTerm(TypeNode tn, size_t i) const
196 : : {
197 : 57784 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
198 [ + - ]: 57784 : if (it != d_typeMap.end())
199 : : {
200 [ - + ][ - + ]: 57784 : Assert(i < it->second->d_list.size());
[ - - ]
201 : 57784 : return it->second->d_list[i];
202 : : }
203 : 0 : DebugUnhandled();
204 : : return Node::null();
205 : : }
206 : :
207 : 7908 : Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
208 : : {
209 : 7908 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
210 [ + + ]: 7908 : if (it != d_typeMap.end())
211 : : {
212 [ - + ][ - + ]: 2678 : Assert(!it->second->d_list.empty());
[ - - ]
213 [ + + ]: 2678 : if (!reqVar)
214 : : {
215 : 1654 : return it->second->d_list[0];
216 : : }
217 [ + + ]: 2297 : for (const Node& v : it->second->d_list)
218 : : {
219 [ + + ]: 2118 : if (v.isVar())
220 : : {
221 : 845 : return v;
222 : : }
223 : : }
224 : : }
225 : 5409 : return getOrMakeTypeFreshVariable(tn);
226 : : }
227 : :
228 : 5409 : Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
229 : : {
230 : 5409 : std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn);
231 [ + + ]: 5409 : if (it == d_type_fv.end())
232 : : {
233 : 1632 : NodeManager* nm = nodeManager();
234 : 1632 : SkolemManager* sm = nm->getSkolemManager();
235 : 1632 : std::vector<Node> cacheVals;
236 : 1632 : cacheVals.push_back(nm->mkConst(SortToTerm(tn)));
237 : 1632 : Node k = sm->mkSkolemFunction(SkolemId::GROUND_TERM, cacheVals);
238 [ + - ]: 3264 : Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
239 : 1632 : << std::endl;
240 [ - + ]: 1632 : if (options().quantifiers.instMaxLevel != -1)
241 : : {
242 : 0 : QuantAttributes::setInstantiationLevelAttr(k, 0);
243 : : }
244 : 1632 : d_type_fv[tn] = k;
245 : 1632 : return k;
246 : 1632 : }
247 : 3777 : return it->second;
248 : : }
249 : :
250 : 233067514 : Node TermDb::getMatchOperator(TNode n)
251 : : {
252 : 233067514 : Kind k = n.getKind();
253 : : //datatype operators may be parametric, always assume they are
254 [ + + ][ + + ]: 233067514 : if (k == Kind::SELECT || k == Kind::STORE || k == Kind::SET_UNION
[ + + ]
255 [ + + ][ + - ]: 232930334 : || k == Kind::SET_INTER || k == Kind::SET_SUBSET || k == Kind::SET_MINUS
[ + + ]
256 [ + + ][ + + ]: 232926936 : || k == Kind::SET_MEMBER || k == Kind::SET_SINGLETON
257 [ + + ][ + + ]: 232868002 : || k == Kind::APPLY_SELECTOR || k == Kind::APPLY_TESTER
258 [ + + ][ + + ]: 232201706 : || k == Kind::SEP_PTO || k == Kind::HO_APPLY || k == Kind::SEQ_NTH
[ + + ]
259 [ + + ][ + + ]: 232157845 : || k == Kind::STRING_LENGTH || k == Kind::BITVECTOR_UBV_TO_INT
260 [ + + ]: 232080755 : || k == Kind::INT_TO_BITVECTOR)
261 : : {
262 : : //since it is parametric, use a particular one as op
263 : 986795 : TypeNode tn = n[0].getType();
264 : 986795 : Node op = n.getOperator();
265 : 986795 : std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
266 [ + + ]: 986795 : if( ito!=d_par_op_map.end() ){
267 : 962786 : std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
268 [ + + ]: 962786 : if( it!=ito->second.end() ){
269 : 961350 : return it->second;
270 : : }
271 : : }
272 [ + - ][ - + ]: 25445 : Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
[ - - ]
273 : 25445 : d_par_op_map[op][tn] = n;
274 : 25445 : return n;
275 : 986795 : }
276 [ + + ]: 232080719 : else if (inst::TriggerTermInfo::isAtomicTriggerKind(k))
277 : : {
278 : 224045503 : return n.getOperator();
279 : : }
280 : 8035216 : return Node::null();
281 : : }
282 : :
283 : 0 : bool TermDb::isMatchable(TNode n) { return !getMatchOperator(n).isNull(); }
284 : :
285 : 10344229 : void TermDb::eqNotifyMerge(TNode t1, TNode t2)
286 : : {
287 [ + + ]: 10344229 : if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
288 : : {
289 : : // Since the equivalence class of t1 and t2 merged, we now consider these
290 : : // two terms to be relevant in the current context. Note technically this
291 : : // does not mean that these terms are in assertions, e.g. t1 and t2 may be
292 : : // merged via congruence if a=b is an assertion and f(a) and f(b) are
293 : : // preregistered terms. Nevertheless this is a close approximation of the
294 : : // terms we care about. Since we are listening to the master equality
295 : : // engine notifications, this also includes internally introduced terms
296 : : // (if any) introduced by theory solvers.
297 : 10129988 : setHasTerm(t1);
298 : 10129988 : setHasTerm(t2);
299 : : }
300 : 10344229 : }
301 : :
302 : 5226140 : void TermDb::addTerm(Node n)
303 : : {
304 [ + + ]: 5226140 : if (d_processed.find(n) != d_processed.end())
305 : : {
306 : 3117924 : return;
307 : : }
308 : 2108216 : d_processed.insert(n);
309 [ + + ]: 2108216 : if (!TermUtil::hasInstConstAttr(n))
310 : : {
311 [ + - ]: 1952637 : Trace("term-db-debug") << "register term : " << n << std::endl;
312 : 1952637 : DbList* dlt = getOrMkDbListForType(n.getType());
313 : 1952637 : dlt->d_list.push_back(n);
314 : : // if this is an atomic trigger, consider adding it
315 : 1952637 : Node op = getMatchOperator(n);
316 [ + + ]: 1952637 : if (!op.isNull())
317 : : {
318 [ + - ]: 914850 : Trace("term-db") << "register term in db " << n << std::endl;
319 [ + - ]: 914850 : Trace("term-db-debug") << " match operator is : " << op << std::endl;
320 : 914850 : DbList* dlo = getOrMkDbListForOp(op);
321 : 914850 : dlo->d_list.push_back(n);
322 : : // If we are higher-order, we may need to register more terms.
323 : 914850 : addTermInternal(n);
324 : : }
325 : 1952637 : }
326 : : else
327 : : {
328 : 155579 : setTermInactive(n);
329 : : }
330 [ + + ]: 2108216 : if (!n.isClosure())
331 : : {
332 [ + + ]: 5433311 : for (const Node& nc : n)
333 : : {
334 : 3325161 : addTerm(nc);
335 : 3325161 : }
336 : : }
337 : : }
338 : :
339 : 1952637 : DbList* TermDb::getOrMkDbListForType(TypeNode tn)
340 : : {
341 : 1952637 : TypeNodeDbListMap::iterator it = d_typeMap.find(tn);
342 [ + + ]: 1952637 : if (it != d_typeMap.end())
343 : : {
344 : 1887464 : return it->second.get();
345 : : }
346 : 65173 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
347 : 65173 : d_typeMap.insert(tn, dl);
348 : 65173 : return dl.get();
349 : 65173 : }
350 : :
351 : 1017728 : DbList* TermDb::getOrMkDbListForOp(TNode op)
352 : : {
353 : 1017728 : NodeDbListMap::iterator it = d_opMap.find(op);
354 [ + + ]: 1017728 : if (it != d_opMap.end())
355 : : {
356 : 845599 : return it->second.get();
357 : : }
358 : 172129 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
359 : 172129 : d_opMap.insert(op, dl);
360 [ - + ][ - + ]: 172129 : Assert(op.getKind() != Kind::BOUND_VARIABLE);
[ - - ]
361 : 172129 : d_ops.push_back(op);
362 : 172129 : return dl.get();
363 : 172129 : }
364 : :
365 : 2064545 : void TermDb::computeArgReps( TNode n ) {
366 [ + + ]: 2064545 : if (d_arg_reps.find(n) == d_arg_reps.end())
367 : : {
368 : 1156188 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
369 : 1156188 : std::vector<TNode>& tars = d_arg_reps[n];
370 [ + + ]: 3425660 : for (const TNode& nc : n)
371 : : {
372 [ + - ][ + - ]: 4538944 : TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
[ - - ]
373 : 2269472 : tars.emplace_back(r);
374 : 2269472 : }
375 : : }
376 : 2064545 : }
377 : :
378 : 8947667 : void TermDb::computeUfEqcTerms( TNode f ) {
379 [ - + ][ - + ]: 8947667 : Assert(f == getOperatorRepresentative(f));
[ - - ]
380 [ + + ]: 8947667 : if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
381 : : {
382 : 8850311 : return;
383 : : }
384 [ + - ]: 97356 : Trace("term-db-debug") << "computeUfEqcTerms for " << f << std::endl;
385 : 97356 : TNodeTrie& tnt = d_func_map_eqc_trie[f];
386 : 97356 : tnt.clear();
387 : : // get the matchable operators in the equivalence class of f
388 : 97356 : std::vector<TNode> ops;
389 : 97356 : getOperatorsFor(f, ops);
390 : 97356 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
391 [ + + ]: 194901 : for (TNode ff : ops)
392 : : {
393 : 97545 : DbList* dbl = getOrMkDbListForOp(ff);
394 [ + + ]: 1214667 : for (const Node& n : dbl->d_list)
395 : : {
396 [ + + ][ + + ]: 1117122 : if (hasTermCurrent(n) && isTermActive(n))
[ + + ][ + + ]
[ - - ]
397 : : {
398 : 936853 : computeArgReps(n);
399 [ + - ][ + - ]: 1873706 : TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
[ - - ]
400 : 936853 : tnt.d_data[r].addTerm(n, d_arg_reps[n]);
401 [ + - ]: 1873706 : Trace("term-db-debug")
402 : 0 : << "Adding term " << n << " to eqc " << r
403 [ - + ][ - - ]: 936853 : << " with arg reps : " << d_arg_reps[n] << std::endl;
404 : 936853 : }
405 : : }
406 : 97545 : }
407 : 97356 : }
408 : :
409 : 40586697 : void TermDb::computeUfTerms( TNode f ) {
410 [ + + ]: 40586697 : if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
411 : : {
412 : : // already computed
413 : 40475819 : return;
414 : : }
415 [ - + ][ - + ]: 110933 : Assert(f == getOperatorRepresentative(f));
[ - - ]
416 : 110933 : d_op_nonred_count[f] = 0;
417 : : // get the matchable operators in the equivalence class of f
418 : 110933 : std::vector<TNode> ops;
419 : 110933 : getOperatorsFor(f, ops);
420 [ + - ]: 110933 : Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
421 : 110933 : unsigned congruentCount = 0;
422 : 110933 : unsigned nonCongruentCount = 0;
423 : 110933 : unsigned alreadyCongruentCount = 0;
424 : 110933 : unsigned relevantCount = 0;
425 : 110933 : NodeManager* nm = nodeManager();
426 [ + + ]: 222564 : for (TNode ff : ops)
427 : : {
428 : 111686 : NodeDbListMap::iterator it = d_opMap.find(ff);
429 [ + + ]: 111686 : if (it == d_opMap.end())
430 : : {
431 : : // no terms for this operator
432 : 16451 : continue;
433 : : }
434 [ + - ]: 95235 : Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
435 [ + + ]: 1396401 : 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 [ + + ][ - + ]: 1301221 : if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
[ + + ][ + + ]
[ - - ]
439 : : {
440 [ + - ]: 88926 : Trace("term-db-debug") << n << " is not relevant." << std::endl;
441 : 443855 : continue;
442 : : }
443 : :
444 : 1212295 : relevantCount++;
445 [ + + ]: 1212295 : if (!isTermActive(n))
446 : : {
447 [ + - ]: 84603 : Trace("term-db-debug") << n << " is already redundant." << std::endl;
448 : 84603 : alreadyCongruentCount++;
449 : 84603 : continue;
450 : : }
451 : :
452 : 1127692 : computeArgReps(n);
453 : 1127692 : std::vector<TNode>& reps = d_arg_reps[n];
454 [ + - ]: 2255384 : Trace("term-db-debug")
455 : 1127692 : << "Adding term " << n << " with arg reps : " << reps << std::endl;
456 [ - + ][ - + ]: 1127692 : Assert(d_qstate.hasTerm(n));
[ - - ]
457 [ + - ]: 2255384 : Trace("term-db-debug")
458 : 1127692 : << " and value : " << d_qstate.getRepresentative(n) << std::endl;
459 : 2255384 : Node at = d_func_map_trie[f].addOrGetTerm(n, reps);
460 [ - + ][ - + ]: 1127692 : Assert(d_qstate.hasTerm(at));
[ - - ]
461 [ + - ]: 1127692 : Trace("term-db-debug2") << "...add term returned " << at << std::endl;
462 : 1127692 : if (at != n && d_qstate.areEqual(at, n))
463 : : {
464 : 270326 : setTermInactive(n);
465 [ + - ]: 270326 : Trace("term-db-debug") << n << " is redundant." << std::endl;
466 : 270326 : congruentCount++;
467 : 270326 : continue;
468 : : }
469 : 857366 : std::vector<Node> antec;
470 [ + + ]: 857366 : 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 : 110 : 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 : 857311 : std::vector<std::vector<TNode> >& frds = d_fmapRelDom[f];
504 : 857311 : size_t rsize = reps.size();
505 : : // ensure the relevant domain vector has been allocated
506 : 857311 : frds.resize(rsize);
507 [ + + ]: 2643171 : for (size_t i = 0; i < rsize; i++)
508 : : {
509 : 1785860 : TNode r = reps[i];
510 : 1785860 : std::vector<TNode>& frd = frds[i];
511 [ + + ]: 1785860 : if (std::find(frd.begin(), frd.end(), r) == frd.end())
512 : : {
513 : 726426 : frd.push_back(r);
514 : : }
515 : 1785860 : }
516 : 857311 : nonCongruentCount++;
517 : 857311 : d_op_nonred_count[f]++;
518 [ + + ][ + + ]: 1127747 : }
[ + ]
519 [ - + ]: 95180 : 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 [ + + ][ + ]: 111686 : }
531 [ + + ]: 110933 : }
532 : :
533 : 57419431 : Node TermDb::getOperatorRepresentative(TNode op) const { return op; }
534 : :
535 : 815967 : bool TermDb::checkCongruentDisequal(TNode a,
536 : : TNode b,
537 : : CVC5_UNUSED std::vector<Node>& exp)
538 : : {
539 [ + + ]: 815967 : if (d_qstate.areDisequal(a, b))
540 : : {
541 : 48 : return true;
542 : : }
543 : 815919 : return false;
544 : : }
545 : :
546 : 14179603 : 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 : 14179603 : f = getOperatorRepresentative(f);
550 : 14179603 : computeUfTerms(f);
551 : 14179603 : 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 : 14179603 : d_fmapRelDom.find(f);
555 [ + + ]: 14179603 : if (it != d_fmapRelDom.end())
556 : : {
557 [ - + ][ - + ]: 13881648 : Assert(i < it->second.size());
[ - - ]
558 : 13881648 : const std::vector<TNode>& rd = it->second[i];
559 : 13881648 : return std::find(rd.begin(), rd.end(), r) != rd.end();
560 : : }
561 : 297955 : return false;
562 : : }
563 : :
564 : 8734715 : bool TermDb::isTermActive(Node n)
565 : : {
566 : 8734715 : return d_inactive_map.find( n )==d_inactive_map.end();
567 : : //return !n.getAttribute(NoMatchAttribute());
568 : : }
569 : :
570 : 544015 : void TermDb::setTermInactive(Node n) { d_inactive_map[n] = true; }
571 : :
572 : 9551206 : bool TermDb::hasTermCurrent(const Node& n, bool useMode) const
573 : : {
574 [ - + ]: 9551206 : if( !useMode ){
575 : 0 : return d_has_map.find( n )!=d_has_map.end();
576 : : }
577 : : //some assertions are not sent to EE
578 [ + + ]: 9551206 : if (options().quantifiers.termDbMode == options::TermDbMode::ALL)
579 : : {
580 : 125308 : return true;
581 : : }
582 [ + - ]: 9425898 : else if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
583 : : {
584 : 9425898 : return d_has_map.find( n )!=d_has_map.end();
585 : : }
586 : 0 : DebugUnhandled() << "TermDb::hasTermCurrent: Unknown termDbMode : "
587 : 0 : << options().quantifiers.termDbMode;
588 : : return false;
589 : : }
590 : :
591 : 1470 : bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
592 : : {
593 [ + + ]: 1470 : if (options().quantifiers.instMaxLevel != -1)
594 : : {
595 : : uint64_t level;
596 [ + - ]: 1114 : if (QuantAttributes::getInstantiationLevel(n, level))
597 : : {
598 : : int64_t fml =
599 [ - + ][ + - ]: 1114 : f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
[ - - ]
600 [ - + ]: 1114 : unsigned ml = fml >= 0 ? fml : options().quantifiers.instMaxLevel;
601 : :
602 [ - + ]: 1114 : if (level > ml)
603 : : {
604 [ - - ]: 0 : Trace("inst-add-debug")
605 : 0 : << "Term " << n << " has instantiation level " << level;
606 [ - - ]: 0 : Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
607 : 0 : return false;
608 : : }
609 : : }
610 : : else
611 : : {
612 [ - - ]: 0 : Trace("inst-add-debug")
613 : 0 : << "Term " << n << " does not have an instantiation level."
614 : 0 : << std::endl;
615 : 0 : return false;
616 : : }
617 : : }
618 : : // it cannot have instantiation constants, which originate from
619 : : // counterexample-guided instantiation strategies.
620 : 1470 : return !TermUtil::hasInstConstAttr(n);
621 : : }
622 : :
623 : 356 : Node TermDb::getEligibleTermInEqc( TNode r ) {
624 [ + - ]: 356 : if( isTermEligibleForInstantiation( r, TNode::null() ) ){
625 : 356 : return r;
626 : : }else{
627 : 0 : std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
628 [ - - ]: 0 : if( it==d_term_elig_eqc.end() ){
629 : 0 : Node h;
630 : 0 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
631 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
632 [ - - ]: 0 : while (!eqc_i.isFinished())
633 : : {
634 : 0 : TNode n = (*eqc_i);
635 : 0 : ++eqc_i;
636 [ - - ]: 0 : if (isTermEligibleForInstantiation(n, TNode::null()))
637 : : {
638 : 0 : h = n;
639 : 0 : break;
640 : : }
641 [ - - ]: 0 : }
642 : 0 : d_term_elig_eqc[r] = h;
643 : 0 : return h;
644 : 0 : }else{
645 : 0 : return it->second;
646 : : }
647 : : }
648 : : }
649 : :
650 : 62867 : bool TermDb::finishResetInternal(CVC5_UNUSED Theory::Effort e)
651 : : {
652 : : // do nothing
653 : 62867 : return true;
654 : : }
655 : :
656 : 823962 : void TermDb::addTermInternal(CVC5_UNUSED Node n)
657 : : {
658 : : // do nothing
659 : 823962 : }
660 : :
661 : 197172 : void TermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
662 : : {
663 : 197172 : ops.push_back(f);
664 : 197172 : }
665 : :
666 : 38211293 : void TermDb::setHasTerm(Node n)
667 : : {
668 [ + - ]: 38211293 : Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
669 : 38211293 : std::vector<TNode> visit;
670 : 38211293 : TNode cur;
671 : 38211293 : visit.push_back(n);
672 : : do
673 : : {
674 : 76562234 : cur = visit.back();
675 : 76562234 : visit.pop_back();
676 [ + + ]: 76562234 : if (d_has_map.find(cur) == d_has_map.end())
677 : : {
678 : 23247935 : d_has_map.insert(cur);
679 : 23247935 : visit.insert(visit.end(), cur.begin(), cur.end());
680 : : }
681 [ + + ]: 76562234 : } while (!visit.empty());
682 : 38211293 : }
683 : :
684 : 39041 : void TermDb::presolve() {}
685 : :
686 : 66817 : bool TermDb::reset( Theory::Effort effort ){
687 : 66817 : d_op_nonred_count.clear();
688 : 66817 : d_arg_reps.clear();
689 : 66817 : d_func_map_trie.clear();
690 : 66817 : d_func_map_eqc_trie.clear();
691 : 66817 : d_fmapRelDom.clear();
692 : :
693 [ - + ][ - + ]: 66817 : Assert(d_qstate.getEqualityEngine()->consistent());
[ - - ]
694 : :
695 : : //compute has map
696 [ + + ]: 66817 : if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
697 : : {
698 : 66561 : d_term_elig_eqc.clear();
699 : 66561 : const LogicInfo& logicInfo = d_qstate.getLogicInfo();
700 [ + + ]: 998415 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
701 : : {
702 [ + + ]: 931854 : if (!logicInfo.isTheoryEnabled(theoryId))
703 : : {
704 : 303305 : continue;
705 : : }
706 : : // Note that we have already marked all terms that have participated in
707 : : // equality engine merges as relevant. We go back and ensure all
708 : : // remaining terms that appear in assertions are marked relevant here
709 : : // in case there are terms appearing in assertions but not in the master
710 : : // equality engine.
711 : 628549 : for (context::CDList<Assertion>::const_iterator
712 : 628549 : it = d_qstate.factsBegin(theoryId),
713 : 628549 : it_end = d_qstate.factsEnd(theoryId);
714 [ + + ]: 18579866 : it != it_end;
715 : 17951317 : ++it)
716 : : {
717 : 17951317 : setHasTerm((*it).d_assertion);
718 : : }
719 : : }
720 : : }
721 : : // finish reset
722 : 66817 : return finishResetInternal(effort);
723 : : }
724 : :
725 : 50883 : TNodeTrie* TermDb::getTermArgTrie(Node f)
726 : : {
727 : 50883 : f = getOperatorRepresentative(f);
728 : 50883 : computeUfTerms( f );
729 : 50883 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
730 [ + + ]: 50883 : if( itut!=d_func_map_trie.end() ){
731 : 34056 : return &itut->second;
732 : : }else{
733 : 16827 : return NULL;
734 : : }
735 : : }
736 : :
737 : 8947667 : TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
738 : : {
739 : 8947667 : f = getOperatorRepresentative(f);
740 : 8947667 : computeUfEqcTerms( f );
741 : 8947667 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
742 [ - + ]: 8947667 : if( itut==d_func_map_eqc_trie.end() ){
743 : 0 : return NULL;
744 : : }else{
745 [ + + ]: 8947667 : if( eqc.isNull() ){
746 : 2228748 : return &itut->second;
747 : : }else{
748 : : std::map<TNode, TNodeTrie>::iterator itute =
749 : 6718919 : itut->second.d_data.find(eqc);
750 [ + + ]: 6718919 : if( itute!=itut->second.d_data.end() ){
751 : 3774609 : return &itute->second;
752 : : }else{
753 : 2944310 : return NULL;
754 : : }
755 : : }
756 : : }
757 : : }
758 : :
759 : 0 : TNode TermDb::getCongruentTerm( Node f, Node n ) {
760 : 0 : f = getOperatorRepresentative(f);
761 : 0 : computeUfTerms( f );
762 : 0 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
763 [ - - ]: 0 : if( itut!=d_func_map_trie.end() ){
764 : 0 : computeArgReps( n );
765 : 0 : return itut->second.existsTerm( d_arg_reps[n] );
766 : : }
767 : 0 : return TNode::null();
768 : : }
769 : :
770 : 26356211 : TNode TermDb::getCongruentTerm(Node f, const std::vector<TNode>& args)
771 : : {
772 : 26356211 : f = getOperatorRepresentative(f);
773 : 26356211 : computeUfTerms( f );
774 : 26356211 : return d_func_map_trie[f].existsTerm( args );
775 : : }
776 : :
777 : : } // namespace quantifiers
778 : : } // namespace theory
779 : : } // namespace cvc5::internal
|
