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 : 20118 : DeqCongProofGenerator(Env& env) : EnvObj(env) {}
53 : 40208 : 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 : 9 : std::shared_ptr<ProofNode> getProofFor(Node fact) override
60 : : {
61 [ - + ][ - + ]: 9 : Assert(fact.getKind() == Kind::IMPLIES);
[ - - ]
62 [ - + ][ - + ]: 9 : Assert(fact[1].getKind() == Kind::EQUAL);
[ - - ]
63 : 18 : Node a = fact[1][0];
64 : 18 : Node b = fact[1][1];
65 : 18 : std::vector<Node> assumps;
66 [ + + ]: 9 : if (fact[0].getKind() == Kind::AND)
67 : : {
68 : 4 : assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
69 : : }
70 : : else
71 : : {
72 : 5 : assumps.push_back(fact[0]);
73 : : }
74 : 27 : CDProof cdp(d_env);
75 [ - + ]: 9 : 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 [ - + ][ - + ]: 9 : Assert(a.getNumChildren() == b.getNumChildren());
[ - - ]
83 : 18 : std::vector<Node> cargs;
84 : 9 : ProofRule cr = expr::getCongRule(a, cargs);
85 : 9 : size_t nchild = a.getNumChildren();
86 : 18 : std::vector<Node> premises;
87 [ + + ]: 31 : for (size_t i = 0; i < nchild; i++)
88 : : {
89 : 66 : Node eq = a[i].eqNode(b[i]);
90 : 22 : premises.push_back(eq);
91 [ + + ]: 22 : if (a[i] == b[i])
92 : : {
93 : 18 : cdp.addStep(eq, ProofRule::REFL, {}, {a[i]});
94 : : }
95 : : else
96 : : {
97 [ - + ][ - + ]: 13 : Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end());
[ - - ]
98 : : }
99 : : }
100 : 9 : cdp.addStep(fact[1], cr, premises, cargs);
101 : 9 : std::shared_ptr<ProofNode> pfn = cdp.getProofFor(fact[1]);
102 : 9 : return d_env.getProofNodeManager()->mkScope(pfn, assumps);
103 : : }
104 : : /** identify */
105 : 0 : std::string identify() const override { return "DeqCongProofGenerator"; }
106 : : };
107 : :
108 : 50980 : TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
109 : : : QuantifiersUtil(env),
110 : : d_qstate(qs),
111 : : d_qim(nullptr),
112 : : d_qreg(qr),
113 : : d_processed(context()),
114 : : d_typeMap(context()),
115 : : d_ops(context()),
116 : : d_opMap(context()),
117 : : d_inactive_map(context()),
118 : 20118 : d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env)
119 [ + + ]: 71098 : : nullptr)
120 : : {
121 : 50980 : d_true = nodeManager()->mkConst(true);
122 : 50980 : d_false = nodeManager()->mkConst(false);
123 : 50980 : }
124 : :
125 : 100290 : TermDb::~TermDb(){
126 : :
127 : 100290 : }
128 : :
129 : 50980 : void TermDb::finishInit(QuantifiersInferenceManager* qim)
130 : : {
131 : 50980 : d_qim = qim;
132 : 50980 : }
133 : :
134 : 59596 : void TermDb::registerQuantifier( Node q ) {
135 [ - + ][ - + ]: 59596 : Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
[ - - ]
136 [ + + ]: 191908 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
137 : : {
138 : 132312 : Node ic = d_qreg.getInstantiationConstant(q, i);
139 : 132312 : setTermInactive( ic );
140 : : }
141 : 59596 : }
142 : :
143 : 3466 : size_t TermDb::getNumOperators() const { return d_ops.size(); }
144 : :
145 : 12141 : Node TermDb::getOperator(size_t i) const
146 : : {
147 [ - + ][ - + ]: 12141 : Assert(i < d_ops.size());
[ - - ]
148 : 12141 : return d_ops[i];
149 : : }
150 : :
151 : : /** ground terms */
152 : 2122 : size_t TermDb::getNumGroundTerms(TNode f) const
153 : : {
154 : 2122 : NodeDbListMap::const_iterator it = d_opMap.find(f);
155 [ + - ]: 2122 : if (it != d_opMap.end())
156 : : {
157 : 2122 : return it->second->d_list.size();
158 : : }
159 : 0 : return 0;
160 : : }
161 : :
162 : 10358 : Node TermDb::getGroundTerm(TNode f, size_t i) const
163 : : {
164 : 10358 : NodeDbListMap::const_iterator it = d_opMap.find(f);
165 [ + - ]: 10358 : if (it != d_opMap.end())
166 : : {
167 [ - + ][ - + ]: 10358 : Assert(i < it->second->d_list.size());
[ - - ]
168 : 10358 : return it->second->d_list[i];
169 : : }
170 : 0 : Assert(false);
171 : : return Node::null();
172 : : }
173 : :
174 : 955488 : DbList* TermDb::getGroundTermList(TNode f) const
175 : : {
176 : 955488 : NodeDbListMap::const_iterator it = d_opMap.find(f);
177 [ + + ]: 955488 : if (it != d_opMap.end())
178 : : {
179 : 930341 : return it->second.get();
180 : : }
181 : 25147 : return nullptr;
182 : : }
183 : :
184 : 1705 : size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const
185 : : {
186 : 1705 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
187 [ + + ]: 1705 : if (it != d_typeMap.end())
188 : : {
189 : 1633 : return it->second->d_list.size();
190 : : }
191 : 72 : return 0;
192 : : }
193 : :
194 : 68592 : Node TermDb::getTypeGroundTerm(TypeNode tn, size_t i) const
195 : : {
196 : 68592 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
197 [ + - ]: 68592 : if (it != d_typeMap.end())
198 : : {
199 [ - + ][ - + ]: 68592 : Assert(i < it->second->d_list.size());
[ - - ]
200 : 68592 : return it->second->d_list[i];
201 : : }
202 : 0 : Assert(false);
203 : : return Node::null();
204 : : }
205 : :
206 : 7522 : Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
207 : : {
208 : 7522 : TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
209 [ + + ]: 7522 : if (it != d_typeMap.end())
210 : : {
211 [ - + ][ - + ]: 2551 : Assert(!it->second->d_list.empty());
[ - - ]
212 [ + + ]: 2551 : if (!reqVar)
213 : : {
214 : 1911 : return it->second->d_list[0];
215 : : }
216 [ + + ]: 1223 : for (const Node& v : it->second->d_list)
217 : : {
218 [ + + ]: 1104 : if (v.isVar())
219 : : {
220 : 521 : return v;
221 : : }
222 : : }
223 : : }
224 : 5090 : return getOrMakeTypeFreshVariable(tn);
225 : : }
226 : :
227 : 5090 : Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
228 : : {
229 : 5090 : std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn);
230 [ + + ]: 5090 : if (it == d_type_fv.end())
231 : : {
232 : 739 : NodeManager* nm = nodeManager();
233 : 739 : SkolemManager* sm = nm->getSkolemManager();
234 : 1478 : std::vector<Node> cacheVals;
235 : 739 : cacheVals.push_back(nm->mkConst(SortToTerm(tn)));
236 : 1478 : Node k = sm->mkSkolemFunction(SkolemId::GROUND_TERM, cacheVals);
237 [ + - ]: 1478 : Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
238 : 739 : << std::endl;
239 [ - + ]: 739 : if (options().quantifiers.instMaxLevel != -1)
240 : : {
241 : 0 : QuantAttributes::setInstantiationLevelAttr(k, 0);
242 : : }
243 : 739 : d_type_fv[tn] = k;
244 : 739 : return k;
245 : : }
246 : 4351 : return it->second;
247 : : }
248 : :
249 : 37525600 : Node TermDb::getMatchOperator(TNode n)
250 : : {
251 : 37525600 : Kind k = n.getKind();
252 : : //datatype operators may be parametric, always assume they are
253 [ + + ][ + + ]: 37525600 : if (k == Kind::SELECT || k == Kind::STORE || k == Kind::SET_UNION
[ + + ]
254 [ + + ][ + - ]: 37373000 : || k == Kind::SET_INTER || k == Kind::SET_SUBSET || k == Kind::SET_MINUS
[ + + ]
255 [ + + ][ + + ]: 37369300 : || k == Kind::SET_MEMBER || k == Kind::SET_SINGLETON
256 [ + + ][ + + ]: 37305600 : || k == Kind::APPLY_SELECTOR || k == Kind::APPLY_TESTER
257 [ + + ][ + + ]: 36619500 : || k == Kind::SEP_PTO || k == Kind::HO_APPLY || k == Kind::SEQ_NTH
[ + + ]
258 [ + + ][ + + ]: 36583700 : || k == Kind::STRING_LENGTH || k == Kind::BITVECTOR_TO_NAT
259 [ + + ]: 36506100 : || k == Kind::INT_TO_BITVECTOR)
260 : : {
261 : : //since it is parametric, use a particular one as op
262 : 2039200 : TypeNode tn = n[0].getType();
263 : 2039200 : Node op = n.getOperator();
264 : 1019600 : std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
265 [ + + ]: 1019600 : if( ito!=d_par_op_map.end() ){
266 : 994533 : std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
267 [ + + ]: 994533 : if( it!=ito->second.end() ){
268 : 993048 : return it->second;
269 : : }
270 : : }
271 [ + - ][ - + ]: 26552 : Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
[ - - ]
272 : 26552 : d_par_op_map[op][tn] = n;
273 : 26552 : return n;
274 : : }
275 [ + + ]: 36506000 : else if (inst::TriggerTermInfo::isAtomicTriggerKind(k))
276 : : {
277 : 29496500 : return n.getOperator();
278 : : }
279 : 7009520 : return Node::null();
280 : : }
281 : :
282 : 0 : bool TermDb::isMatchable(TNode n) { return !getMatchOperator(n).isNull(); }
283 : :
284 : 5382900 : void TermDb::addTerm(Node n)
285 : : {
286 [ + + ]: 5382900 : if (d_processed.find(n) != d_processed.end())
287 : : {
288 : 3205840 : return;
289 : : }
290 : 2177070 : d_processed.insert(n);
291 [ + + ]: 2177070 : if (!TermUtil::hasInstConstAttr(n))
292 : : {
293 [ + - ]: 2027130 : Trace("term-db-debug") << "register term : " << n << std::endl;
294 : 2027130 : DbList* dlt = getOrMkDbListForType(n.getType());
295 : 2027130 : dlt->d_list.push_back(n);
296 : : // if this is an atomic trigger, consider adding it
297 : 4054260 : Node op = getMatchOperator(n);
298 [ + + ]: 2027130 : if (!op.isNull())
299 : : {
300 [ + - ]: 975516 : Trace("term-db") << "register term in db " << n << std::endl;
301 [ + - ]: 975516 : Trace("term-db-debug") << " match operator is : " << op << std::endl;
302 : 975516 : DbList* dlo = getOrMkDbListForOp(op);
303 : 975516 : dlo->d_list.push_back(n);
304 : : // If we are higher-order, we may need to register more terms.
305 : 975516 : addTermInternal(n);
306 : : }
307 : : }
308 : : else
309 : : {
310 : 149938 : setTermInactive(n);
311 : : }
312 [ + + ]: 2177070 : if (!n.isClosure())
313 : : {
314 [ + + ]: 5609240 : for (const Node& nc : n)
315 : : {
316 : 3432250 : addTerm(nc);
317 : : }
318 : : }
319 : : }
320 : :
321 : 2027130 : DbList* TermDb::getOrMkDbListForType(TypeNode tn)
322 : : {
323 : 2027130 : TypeNodeDbListMap::iterator it = d_typeMap.find(tn);
324 [ + + ]: 2027130 : if (it != d_typeMap.end())
325 : : {
326 : 1957760 : return it->second.get();
327 : : }
328 : 138740 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
329 : 69370 : d_typeMap.insert(tn, dl);
330 : 69370 : return dl.get();
331 : : }
332 : :
333 : 1086710 : DbList* TermDb::getOrMkDbListForOp(TNode op)
334 : : {
335 : 1086710 : NodeDbListMap::iterator it = d_opMap.find(op);
336 [ + + ]: 1086710 : if (it != d_opMap.end())
337 : : {
338 : 904469 : return it->second.get();
339 : : }
340 : 364484 : std::shared_ptr<DbList> dl = std::make_shared<DbList>(context());
341 : 182242 : d_opMap.insert(op, dl);
342 [ - + ][ - + ]: 182242 : Assert(op.getKind() != Kind::BOUND_VARIABLE);
[ - - ]
343 : 182242 : d_ops.push_back(op);
344 : 182242 : return dl.get();
345 : : }
346 : :
347 : 2025640 : void TermDb::computeArgReps( TNode n ) {
348 [ + + ]: 2025640 : if (d_arg_reps.find(n) == d_arg_reps.end())
349 : : {
350 : 1143900 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
351 : 1143900 : std::vector<TNode>& tars = d_arg_reps[n];
352 [ + + ]: 3425820 : for (const TNode& nc : n)
353 : : {
354 [ + - ][ + - ]: 6845770 : TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
[ - - ]
355 : 2281920 : tars.emplace_back(r);
356 : : }
357 : : }
358 : 2025640 : }
359 : :
360 : 7383100 : void TermDb::computeUfEqcTerms( TNode f ) {
361 [ - + ][ - + ]: 7383100 : Assert(f == getOperatorRepresentative(f));
[ - - ]
362 [ + + ]: 7383100 : if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
363 : : {
364 : 7276470 : return;
365 : : }
366 : 106634 : TNodeTrie& tnt = d_func_map_eqc_trie[f];
367 : 106634 : tnt.clear();
368 : : // get the matchable operators in the equivalence class of f
369 : 213268 : std::vector<TNode> ops;
370 : 106634 : getOperatorsFor(f, ops);
371 : 106634 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
372 [ + + ]: 213434 : for (TNode ff : ops)
373 : : {
374 : 106800 : DbList* dbl = getOrMkDbListForOp(ff);
375 [ + + ]: 1189300 : for (const Node& n : dbl->d_list)
376 : : {
377 [ + + ][ + + ]: 1082500 : if (hasTermCurrent(n) && isTermActive(n))
[ + + ][ + + ]
[ - - ]
378 : : {
379 : 903599 : computeArgReps(n);
380 [ + - ][ + - ]: 1807200 : TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
[ - - ]
381 : 903599 : tnt.d_data[r].addTerm(n, d_arg_reps[n]);
382 : : }
383 : : }
384 : : }
385 : : }
386 : :
387 : 18923800 : void TermDb::computeUfTerms( TNode f ) {
388 [ + + ]: 18923800 : if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
389 : : {
390 : : // already computed
391 : 18802200 : return;
392 : : }
393 [ - + ][ - + ]: 121689 : Assert(f == getOperatorRepresentative(f));
[ - - ]
394 : 121689 : d_op_nonred_count[f] = 0;
395 : : // get the matchable operators in the equivalence class of f
396 : 121689 : std::vector<TNode> ops;
397 : 121689 : getOperatorsFor(f, ops);
398 [ + - ]: 121689 : Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
399 : 121689 : unsigned congruentCount = 0;
400 : 121689 : unsigned nonCongruentCount = 0;
401 : 121689 : unsigned alreadyCongruentCount = 0;
402 : 121689 : unsigned relevantCount = 0;
403 : 121689 : NodeManager* nm = nodeManager();
404 [ + + ]: 244103 : for (TNode ff : ops)
405 : : {
406 : 122474 : NodeDbListMap::iterator it = d_opMap.find(ff);
407 [ + + ]: 122474 : if (it == d_opMap.end())
408 : : {
409 : : // no terms for this operator
410 : 18562 : continue;
411 : : }
412 [ + - ]: 103912 : Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
413 [ + + ]: 1397340 : for (const Node& n : it->second->d_list)
414 : : {
415 : : // to be added to term index, term must be relevant, and exist in EE
416 [ + + ][ - + ]: 1293490 : if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
[ + + ][ + + ]
[ - - ]
417 : : {
418 [ + - ]: 98343 : Trace("term-db-debug") << n << " is not relevant." << std::endl;
419 : 425168 : continue;
420 : : }
421 : :
422 : 1195140 : relevantCount++;
423 [ + + ]: 1195140 : if (!isTermActive(n))
424 : : {
425 [ + - ]: 73109 : Trace("term-db-debug") << n << " is already redundant." << std::endl;
426 : 73109 : alreadyCongruentCount++;
427 : 73109 : continue;
428 : : }
429 : :
430 : 1122040 : computeArgReps(n);
431 : 1122040 : std::vector<TNode>& reps = d_arg_reps[n];
432 [ + - ]: 1122040 : Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
433 : 1122040 : std::vector<std::vector<TNode> >& frds = d_fmapRelDom[f];
434 : 1122040 : size_t rsize = reps.size();
435 : : // ensure the relevant domain vector has been allocated
436 : 1122040 : frds.resize(rsize);
437 [ + + ]: 3364750 : for (size_t i = 0; i < rsize; i++)
438 : : {
439 : 4485420 : TNode r = reps[i];
440 [ + - ]: 2242710 : Trace("term-db-debug") << r << " ";
441 : 2242710 : std::vector<TNode>& frd = frds[i];
442 [ + + ]: 2242710 : if (std::find(frd.begin(), frd.end(), r) == frd.end())
443 : : {
444 : 768518 : frd.push_back(r);
445 : : }
446 : : }
447 [ + - ]: 1122040 : Trace("term-db-debug") << std::endl;
448 [ - + ][ - + ]: 1122040 : Assert(d_qstate.hasTerm(n));
[ - - ]
449 [ + - ]: 2244070 : Trace("term-db-debug")
450 : 1122040 : << " and value : " << d_qstate.getRepresentative(n) << std::endl;
451 : 2244070 : Node at = d_func_map_trie[f].addOrGetTerm(n, reps);
452 [ - + ][ - + ]: 1122040 : Assert(d_qstate.hasTerm(at));
[ - - ]
453 [ + - ]: 1122040 : Trace("term-db-debug2") << "...add term returned " << at << std::endl;
454 : 1122040 : if (at != n && d_qstate.areEqual(at, n))
455 : : {
456 : 253716 : setTermInactive(n);
457 [ + - ]: 253716 : Trace("term-db-debug") << n << " is redundant." << std::endl;
458 : 253716 : congruentCount++;
459 : 253716 : continue;
460 : : }
461 : 868320 : std::vector<Node> antec;
462 [ + + ]: 868320 : if (checkCongruentDisequal(at, n, antec))
463 : : {
464 [ - + ][ - + ]: 60 : Assert(at.getNumChildren() == n.getNumChildren());
[ - - ]
465 [ + + ]: 193 : for (size_t k = 0, size = at.getNumChildren(); k < size; k++)
466 : : {
467 [ + + ]: 133 : if (at[k] != n[k])
468 : : {
469 : 81 : antec.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]));
470 [ - + ][ - + ]: 81 : Assert(d_qstate.areEqual(at[k], n[k]));
[ - - ]
471 : : }
472 : : }
473 : 120 : Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(antec), at.eqNode(n));
474 [ - + ]: 60 : if (TraceIsOn("term-db-lemma"))
475 : : {
476 [ - - ]: 0 : Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
477 : 0 : << n << "!!!!" << std::endl;
478 [ - - ]: 0 : if (!d_qstate.getValuation().needCheck())
479 : : {
480 [ - - ]: 0 : Trace("term-db-lemma")
481 : 0 : << " all theories passed with no lemmas." << std::endl;
482 : : // we should be a full effort check, prior to theory combination
483 : : }
484 [ - - ]: 0 : Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
485 : : }
486 [ + + ]: 60 : d_qim->addPendingLemma(lem,
487 : : InferenceId::QUANTIFIERS_TDB_DEQ_CONG,
488 : : LemmaProperty::NONE,
489 : 60 : d_dcproof.get());
490 : 60 : d_qstate.notifyInConflict();
491 : 60 : return;
492 : : }
493 : 868260 : nonCongruentCount++;
494 : 868260 : d_op_nonred_count[f]++;
495 : : }
496 [ - + ]: 103852 : if (TraceIsOn("tdb"))
497 : : {
498 [ - - ]: 0 : Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
499 : 0 : << " / ";
500 [ - - ]: 0 : Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
501 : 0 : << (nonCongruentCount + congruentCount
502 : 0 : + alreadyCongruentCount)
503 : 0 : << " / ";
504 [ - - ]: 0 : Trace("tdb") << relevantCount << " / " << it->second->d_list.size()
505 : 0 : << std::endl;
506 : : }
507 : : }
508 : : }
509 : :
510 : 32476700 : Node TermDb::getOperatorRepresentative(TNode op) const { return op; }
511 : :
512 : 825491 : bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
513 : : {
514 [ + + ]: 825491 : if (d_qstate.areDisequal(a, b))
515 : : {
516 : 52 : return true;
517 : : }
518 : 825439 : return false;
519 : : }
520 : :
521 : 12741000 : bool TermDb::inRelevantDomain(TNode f, size_t i, TNode r)
522 : : {
523 : : // notice if we are not higher-order, getOperatorRepresentative is a no-op
524 : 12741000 : f = getOperatorRepresentative(f);
525 : 12741000 : computeUfTerms(f);
526 : 12741000 : Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
527 : : || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
528 : : std::map<Node, std::vector<std::vector<TNode> > >::const_iterator it =
529 : 12741000 : d_fmapRelDom.find(f);
530 [ + + ]: 12741000 : if (it != d_fmapRelDom.end())
531 : : {
532 [ - + ][ - + ]: 12402700 : Assert(i < it->second.size());
[ - - ]
533 : 12402700 : const std::vector<TNode>& rd = it->second[i];
534 : 12402700 : return std::find(rd.begin(), rd.end(), r) != rd.end();
535 : : }
536 : 338343 : return false;
537 : : }
538 : :
539 : 8257400 : bool TermDb::isTermActive(Node n)
540 : : {
541 : 8257400 : return d_inactive_map.find( n )==d_inactive_map.end();
542 : : //return !n.getAttribute(NoMatchAttribute());
543 : : }
544 : :
545 : 535966 : void TermDb::setTermInactive(Node n) { d_inactive_map[n] = true; }
546 : :
547 : 9643840 : bool TermDb::hasTermCurrent(const Node& n, bool useMode) const
548 : : {
549 [ - + ]: 9643840 : if( !useMode ){
550 : 0 : return d_has_map.find( n )!=d_has_map.end();
551 : : }
552 : : //some assertions are not sent to EE
553 [ + + ]: 9643840 : if (options().quantifiers.termDbMode == options::TermDbMode::ALL)
554 : : {
555 : 138648 : return true;
556 : : }
557 [ + - ]: 9505190 : else if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
558 : : {
559 : 9505190 : return d_has_map.find( n )!=d_has_map.end();
560 : : }
561 : 0 : Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : "
562 : 0 : << options().quantifiers.termDbMode;
563 : : return false;
564 : : }
565 : :
566 : 1716 : bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
567 : : {
568 [ + + ]: 1716 : if (options().quantifiers.instMaxLevel != -1)
569 : : {
570 : : uint64_t level;
571 [ + - ]: 1304 : if (QuantAttributes::getInstantiationLevel(n, level))
572 : : {
573 : : int64_t fml =
574 [ - + ][ + - ]: 1304 : f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
[ - - ]
575 [ - + ]: 1304 : unsigned ml = fml >= 0 ? fml : options().quantifiers.instMaxLevel;
576 : :
577 [ - + ]: 1304 : if (level > ml)
578 : : {
579 [ - - ]: 0 : Trace("inst-add-debug")
580 : 0 : << "Term " << n << " has instantiation level " << level;
581 [ - - ]: 0 : Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
582 : 0 : return false;
583 : : }
584 : : }
585 : : else
586 : : {
587 [ - - ]: 0 : Trace("inst-add-debug")
588 : 0 : << "Term " << n << " does not have an instantiation level."
589 : 0 : << std::endl;
590 : 0 : return false;
591 : : }
592 : : }
593 : : // it cannot have instantiation constants, which originate from
594 : : // counterexample-guided instantiation strategies.
595 : 1716 : return !TermUtil::hasInstConstAttr(n);
596 : : }
597 : :
598 : 412 : Node TermDb::getEligibleTermInEqc( TNode r ) {
599 [ + - ]: 412 : if( isTermEligibleForInstantiation( r, TNode::null() ) ){
600 : 412 : return r;
601 : : }else{
602 : 0 : std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
603 [ - - ]: 0 : if( it==d_term_elig_eqc.end() ){
604 : 0 : Node h;
605 : 0 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
606 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
607 [ - - ]: 0 : while (!eqc_i.isFinished())
608 : : {
609 : 0 : TNode n = (*eqc_i);
610 : 0 : ++eqc_i;
611 [ - - ]: 0 : if (isTermEligibleForInstantiation(n, TNode::null()))
612 : : {
613 : 0 : h = n;
614 : 0 : break;
615 : : }
616 : : }
617 : 0 : d_term_elig_eqc[r] = h;
618 : 0 : return h;
619 : : }else{
620 : 0 : return it->second;
621 : : }
622 : : }
623 : : }
624 : :
625 : 57851 : bool TermDb::finishResetInternal(Theory::Effort e)
626 : : {
627 : : // do nothing
628 : 57851 : return true;
629 : : }
630 : :
631 : 895338 : void TermDb::addTermInternal(Node n)
632 : : {
633 : : // do nothing
634 : 895338 : }
635 : :
636 : 216255 : void TermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
637 : : {
638 : 216255 : ops.push_back(f);
639 : 216255 : }
640 : :
641 : 89983000 : void TermDb::setHasTerm( Node n ) {
642 [ + - ]: 89983000 : Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
643 [ + + ]: 89983000 : if( d_has_map.find( n )==d_has_map.end() ){
644 : 36953300 : d_has_map[n] = true;
645 [ + + ]: 96825600 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
646 : 59872300 : setHasTerm( n[i] );
647 : : }
648 : : }
649 : 89983000 : }
650 : :
651 : 39187 : void TermDb::presolve() {}
652 : :
653 : 61727 : bool TermDb::reset( Theory::Effort effort ){
654 : 61727 : d_op_nonred_count.clear();
655 : 61727 : d_arg_reps.clear();
656 : 61727 : d_func_map_trie.clear();
657 : 61727 : d_func_map_eqc_trie.clear();
658 : 61727 : d_fmapRelDom.clear();
659 : :
660 : 61727 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
661 : :
662 [ - + ][ - + ]: 61727 : Assert(ee->consistent());
[ - - ]
663 : :
664 : : //compute has map
665 [ + + ]: 61727 : if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
666 : : {
667 : 61430 : d_has_map.clear();
668 : 61430 : d_term_elig_eqc.clear();
669 : 61430 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
670 [ + + ]: 3796330 : while( !eqcs_i.isFinished() ){
671 : 7469800 : TNode r = (*eqcs_i);
672 : 3734900 : bool addedFirst = false;
673 : 7469800 : Node first;
674 : : //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
675 : 3734900 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
676 [ + + ]: 20120400 : while( !eqc_i.isFinished() ){
677 : 32771000 : TNode n = (*eqc_i);
678 [ + + ]: 16385500 : if( first.isNull() ){
679 : 3734900 : first = n;
680 : : }else{
681 [ + + ]: 12650600 : if( !addedFirst ){
682 : 1127160 : addedFirst = true;
683 : 1127160 : setHasTerm( first );
684 : : }
685 : 12650600 : setHasTerm( n );
686 : : }
687 : 16385500 : ++eqc_i;
688 : : }
689 : 3734900 : ++eqcs_i;
690 : : }
691 : 61430 : const LogicInfo& logicInfo = d_qstate.getLogicInfo();
692 [ + + ]: 921450 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
693 : : {
694 [ + + ]: 860020 : if (!logicInfo.isTheoryEnabled(theoryId))
695 : : {
696 : 264694 : continue;
697 : : }
698 : 16333000 : for (context::CDList<Assertion>::const_iterator
699 : 595326 : it = d_qstate.factsBegin(theoryId),
700 : 595326 : it_end = d_qstate.factsEnd(theoryId);
701 [ + + ]: 16928300 : it != it_end;
702 : 16333000 : ++it)
703 : : {
704 : 16333000 : setHasTerm((*it).d_assertion);
705 : : }
706 : : }
707 : : }
708 : : // finish reset
709 : 61727 : return finishResetInternal(effort);
710 : : }
711 : :
712 : 56474 : TNodeTrie* TermDb::getTermArgTrie(Node f)
713 : : {
714 : 56474 : f = getOperatorRepresentative(f);
715 : 56474 : computeUfTerms( f );
716 : 56474 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
717 [ + + ]: 56474 : if( itut!=d_func_map_trie.end() ){
718 : 36894 : return &itut->second;
719 : : }else{
720 : 19580 : return NULL;
721 : : }
722 : : }
723 : :
724 : 7383100 : TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
725 : : {
726 : 7383100 : f = getOperatorRepresentative(f);
727 : 7383100 : computeUfEqcTerms( f );
728 : 7383100 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
729 [ - + ]: 7383100 : if( itut==d_func_map_eqc_trie.end() ){
730 : 0 : return NULL;
731 : : }else{
732 [ + + ]: 7383100 : if( eqc.isNull() ){
733 : 2350310 : return &itut->second;
734 : : }else{
735 : : std::map<TNode, TNodeTrie>::iterator itute =
736 : 5032790 : itut->second.d_data.find(eqc);
737 [ + + ]: 5032790 : if( itute!=itut->second.d_data.end() ){
738 : 2347990 : return &itute->second;
739 : : }else{
740 : 2684800 : return NULL;
741 : : }
742 : : }
743 : : }
744 : : }
745 : :
746 : 0 : TNode TermDb::getCongruentTerm( Node f, Node n ) {
747 : 0 : f = getOperatorRepresentative(f);
748 : 0 : computeUfTerms( f );
749 : 0 : std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
750 [ - - ]: 0 : if( itut!=d_func_map_trie.end() ){
751 : 0 : computeArgReps( n );
752 : 0 : return itut->second.existsTerm( d_arg_reps[n] );
753 : : }
754 : 0 : return TNode::null();
755 : : }
756 : :
757 : 6126290 : TNode TermDb::getCongruentTerm(Node f, const std::vector<TNode>& args)
758 : : {
759 : 6126290 : f = getOperatorRepresentative(f);
760 : 6126290 : computeUfTerms( f );
761 : 6126290 : return d_func_map_trie[f].existsTerm( args );
762 : : }
763 : :
764 : : } // namespace quantifiers
765 : : } // namespace theory
766 : : } // namespace cvc5::internal
|
