1 /********************* */
2 /*! \file term_database.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Implementation of term databse class
13 **/
14
15 #include "theory/quantifiers/term_database.h"
16
17 #include "options/base_options.h"
18 #include "options/quantifiers_options.h"
19 #include "options/uf_options.h"
20 #include "theory/quantifiers/quantifiers_attributes.h"
21 #include "theory/quantifiers/term_util.h"
22 #include "theory/quantifiers/ematching/trigger.h"
23 #include "theory/quantifiers_engine.h"
24 #include "theory/theory_engine.h"
25
26 using namespace std;
27 using namespace CVC4::kind;
28 using namespace CVC4::context;
29 using namespace CVC4::theory::inst;
30
31 namespace CVC4 {
32 namespace theory {
33 namespace quantifiers {
34
TermDb(context::Context * c,context::UserContext * u,QuantifiersEngine * qe)35 TermDb::TermDb(context::Context* c, context::UserContext* u,
36 QuantifiersEngine* qe)
37 : d_quantEngine(qe),
38 d_inactive_map(c) {
39 d_consistent_ee = true;
40 d_true = NodeManager::currentNM()->mkConst(true);
41 d_false = NodeManager::currentNM()->mkConst(false);
42 }
43
~TermDb()44 TermDb::~TermDb(){
45
46 }
47
registerQuantifier(Node q)48 void TermDb::registerQuantifier( Node q ) {
49 Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) );
50 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
51 Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
52 setTermInactive( ic );
53 }
54 }
55
getNumOperators()56 unsigned TermDb::getNumOperators() { return d_ops.size(); }
getOperator(unsigned i)57 Node TermDb::getOperator(unsigned i)
58 {
59 Assert(i < d_ops.size());
60 return d_ops[i];
61 }
62
63 /** ground terms */
getNumGroundTerms(Node f) const64 unsigned TermDb::getNumGroundTerms(Node f) const
65 {
66 std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
67 if( it!=d_op_map.end() ){
68 return it->second.size();
69 }else{
70 return 0;
71 }
72 }
73
getGroundTerm(Node f,unsigned i) const74 Node TermDb::getGroundTerm(Node f, unsigned i) const
75 {
76 std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
77 if (it != d_op_map.end())
78 {
79 Assert(i < it->second.size());
80 return it->second[i];
81 }
82 else
83 {
84 Assert(false);
85 return Node::null();
86 }
87 }
88
getNumTypeGroundTerms(TypeNode tn) const89 unsigned TermDb::getNumTypeGroundTerms(TypeNode tn) const
90 {
91 std::map<TypeNode, std::vector<Node> >::const_iterator it =
92 d_type_map.find(tn);
93 if( it!=d_type_map.end() ){
94 return it->second.size();
95 }else{
96 return 0;
97 }
98 }
99
getTypeGroundTerm(TypeNode tn,unsigned i) const100 Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
101 {
102 std::map<TypeNode, std::vector<Node> >::const_iterator it =
103 d_type_map.find(tn);
104 if (it != d_type_map.end())
105 {
106 Assert(i < it->second.size());
107 return it->second[i];
108 }
109 else
110 {
111 Assert(false);
112 return Node::null();
113 }
114 }
115
getOrMakeTypeGroundTerm(TypeNode tn)116 Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
117 {
118 std::map<TypeNode, std::vector<Node> >::const_iterator it =
119 d_type_map.find(tn);
120 if (it != d_type_map.end())
121 {
122 Assert(!it->second.empty());
123 return it->second[0];
124 }
125 else
126 {
127 return getOrMakeTypeFreshVariable(tn);
128 }
129 }
130
getOrMakeTypeFreshVariable(TypeNode tn)131 Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
132 {
133 std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
134 d_type_fv.find(tn);
135 if (it == d_type_fv.end())
136 {
137 std::stringstream ss;
138 ss << language::SetLanguage(options::outputLanguage());
139 ss << "e_" << tn;
140 Node k = NodeManager::currentNM()->mkSkolem(
141 ss.str(), tn, "is a termDb fresh variable");
142 Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
143 << std::endl;
144 if (options::instMaxLevel() != -1)
145 {
146 QuantAttributes::setInstantiationLevelAttr(k, 0);
147 }
148 d_type_fv[tn] = k;
149 return k;
150 }
151 else
152 {
153 return it->second;
154 }
155 }
156
getMatchOperator(Node n)157 Node TermDb::getMatchOperator( Node n ) {
158 Kind k = n.getKind();
159 //datatype operators may be parametric, always assume they are
160 if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
161 k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){
162 //since it is parametric, use a particular one as op
163 TypeNode tn = n[0].getType();
164 Node op = n.getOperator();
165 std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
166 if( ito!=d_par_op_map.end() ){
167 std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
168 if( it!=ito->second.end() ){
169 return it->second;
170 }
171 }
172 Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
173 d_par_op_map[op][tn] = n;
174 return n;
175 }else if( inst::Trigger::isAtomicTriggerKind( k ) ){
176 return n.getOperator();
177 }else{
178 return Node::null();
179 }
180 }
181
addTerm(Node n,std::set<Node> & added,bool withinQuant,bool withinInstClosure)182 void TermDb::addTerm(Node n,
183 std::set<Node>& added,
184 bool withinQuant,
185 bool withinInstClosure)
186 {
187 //don't add terms in quantifier bodies
188 if( withinQuant && !options::registerQuantBodyTerms() ){
189 return;
190 }
191 bool rec = false;
192 if (d_processed.find(n) == d_processed.end())
193 {
194 d_processed.insert(n);
195 if (!TermUtil::hasInstConstAttr(n))
196 {
197 Trace("term-db-debug") << "register term : " << n << std::endl;
198 d_type_map[n.getType()].push_back(n);
199 // if this is an atomic trigger, consider adding it
200 if (inst::Trigger::isAtomicTrigger(n))
201 {
202 Trace("term-db") << "register term in db " << n << std::endl;
203
204 Node op = getMatchOperator(n);
205 Trace("term-db-debug") << " match operator is : " << op << std::endl;
206 if (d_op_map.find(op) == d_op_map.end())
207 {
208 d_ops.push_back(op);
209 }
210 d_op_map[op].push_back(n);
211 added.insert(n);
212 // If we are higher-order, we may need to register more terms.
213 if (options::ufHo())
214 {
215 addTermHo(n, added, withinQuant, withinInstClosure);
216 }
217 }
218 }
219 else
220 {
221 setTermInactive(n);
222 }
223 rec = true;
224 }
225 if (withinInstClosure
226 && d_iclosure_processed.find(n) == d_iclosure_processed.end())
227 {
228 d_iclosure_processed.insert(n);
229 rec = true;
230 }
231 if (rec && n.getKind() != FORALL)
232 {
233 for (const Node& nc : n)
234 {
235 addTerm(nc, added, withinQuant, withinInstClosure);
236 }
237 }
238 }
239
computeArgReps(TNode n)240 void TermDb::computeArgReps( TNode n ) {
241 if (d_arg_reps.find(n) == d_arg_reps.end())
242 {
243 eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
244 for (const TNode& nc : n)
245 {
246 TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
247 d_arg_reps[n].push_back( r );
248 }
249 }
250 }
251
computeUfEqcTerms(TNode f)252 void TermDb::computeUfEqcTerms( TNode f ) {
253 Assert( f==getOperatorRepresentative( f ) );
254 if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
255 {
256 return;
257 }
258 d_func_map_eqc_trie[f].clear();
259 // get the matchable operators in the equivalence class of f
260 std::vector<TNode> ops;
261 ops.push_back(f);
262 if (options::ufHo())
263 {
264 ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
265 }
266 eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
267 for (const Node& ff : ops)
268 {
269 for (const TNode& n : d_op_map[ff])
270 {
271 if (hasTermCurrent(n) && isTermActive(n))
272 {
273 computeArgReps(n);
274 TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n;
275 d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
276 }
277 }
278 }
279 }
280
computeUfTerms(TNode f)281 void TermDb::computeUfTerms( TNode f ) {
282 if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
283 {
284 // already computed
285 return;
286 }
287 Assert( f==getOperatorRepresentative( f ) );
288 d_op_nonred_count[f] = 0;
289 // get the matchable operators in the equivalence class of f
290 std::vector<TNode> ops;
291 ops.push_back(f);
292 if (options::ufHo())
293 {
294 ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
295 }
296 Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
297 unsigned congruentCount = 0;
298 unsigned nonCongruentCount = 0;
299 unsigned alreadyCongruentCount = 0;
300 unsigned relevantCount = 0;
301 eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
302 NodeManager* nm = NodeManager::currentNM();
303 for (const Node& ff : ops)
304 {
305 std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
306 if (it == d_op_map.end())
307 {
308 // no terms for this operator
309 continue;
310 }
311 Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
312 for (const Node& n : it->second)
313 {
314 // to be added to term index, term must be relevant, and exist in EE
315 if (!hasTermCurrent(n) || !ee->hasTerm(n))
316 {
317 Trace("term-db-debug") << n << " is not relevant." << std::endl;
318 continue;
319 }
320
321 relevantCount++;
322 if (!isTermActive(n))
323 {
324 Trace("term-db-debug") << n << " is already redundant." << std::endl;
325 alreadyCongruentCount++;
326 continue;
327 }
328
329 computeArgReps(n);
330 Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
331 for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++)
332 {
333 Trace("term-db-debug") << d_arg_reps[n][i] << " ";
334 if (std::find(d_func_map_rel_dom[f][i].begin(),
335 d_func_map_rel_dom[f][i].end(),
336 d_arg_reps[n][i])
337 == d_func_map_rel_dom[f][i].end())
338 {
339 d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]);
340 }
341 }
342 Trace("term-db-debug") << std::endl;
343 Assert(ee->hasTerm(n));
344 Trace("term-db-debug") << " and value : " << ee->getRepresentative(n)
345 << std::endl;
346 Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
347 Assert(ee->hasTerm(at));
348 Trace("term-db-debug2") << "...add term returned " << at << std::endl;
349 if (at != n && ee->areEqual(at, n))
350 {
351 setTermInactive(n);
352 Trace("term-db-debug") << n << " is redundant." << std::endl;
353 congruentCount++;
354 continue;
355 }
356 if (ee->areDisequal(at, n, false))
357 {
358 std::vector<Node> lits;
359 lits.push_back(nm->mkNode(EQUAL, at, n));
360 bool success = true;
361 if (options::ufHo())
362 {
363 // operators might be disequal
364 if (ops.size() > 1)
365 {
366 Node atf = getMatchOperator(at);
367 Node nf = getMatchOperator(n);
368 if (atf != nf)
369 {
370 if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF)
371 {
372 lits.push_back(atf.eqNode(nf).negate());
373 }
374 else
375 {
376 success = false;
377 Assert(false);
378 }
379 }
380 }
381 }
382 if (success)
383 {
384 Assert(at.getNumChildren() == n.getNumChildren());
385 for (unsigned k = 0, size = at.getNumChildren(); k < size; k++)
386 {
387 if (at[k] != n[k])
388 {
389 lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate());
390 }
391 }
392 Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits);
393 if (Trace.isOn("term-db-lemma"))
394 {
395 Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
396 << n << "!!!!" << std::endl;
397 if (!d_quantEngine->getTheoryEngine()->needCheck())
398 {
399 Trace("term-db-lemma") << " all theories passed with no lemmas."
400 << std::endl;
401 // we should be a full effort check, prior to theory combination
402 }
403 Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
404 }
405 d_quantEngine->addLemma(lem);
406 d_quantEngine->setConflict();
407 d_consistent_ee = false;
408 return;
409 }
410 }
411 nonCongruentCount++;
412 d_op_nonred_count[f]++;
413 }
414 if (Trace.isOn("tdb"))
415 {
416 Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
417 << " / ";
418 Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
419 << (nonCongruentCount + congruentCount
420 + alreadyCongruentCount)
421 << " / ";
422 Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
423 }
424 }
425 }
426
addTermHo(Node n,std::set<Node> & added,bool withinQuant,bool withinInstClosure)427 void TermDb::addTermHo(Node n,
428 std::set<Node>& added,
429 bool withinQuant,
430 bool withinInstClosure)
431 {
432 Assert(options::ufHo());
433 if (n.getType().isFunction())
434 {
435 // nothing special to do with functions
436 return;
437 }
438 NodeManager* nm = NodeManager::currentNM();
439 Node curr = n;
440 std::vector<Node> args;
441 while (curr.getKind() == HO_APPLY)
442 {
443 args.insert(args.begin(), curr[1]);
444 curr = curr[0];
445 if (!curr.isVar())
446 {
447 // purify the term
448 std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(curr);
449 Node psk;
450 if (itp == d_ho_fun_op_purify.end())
451 {
452 psk = nm->mkSkolem("pfun",
453 curr.getType(),
454 "purify for function operator term indexing");
455 d_ho_fun_op_purify[curr] = psk;
456 // we do not add it to d_ops since it is an internal operator
457 }
458 else
459 {
460 psk = itp->second;
461 }
462 std::vector<Node> children;
463 children.push_back(psk);
464 children.insert(children.end(), args.begin(), args.end());
465 Node p_n = nm->mkNode(APPLY_UF, children);
466 Trace("term-db") << "register term in db (via purify) " << p_n
467 << std::endl;
468 // also add this one internally
469 d_op_map[psk].push_back(p_n);
470 // maintain backwards mapping
471 d_ho_purify_to_term[p_n] = n;
472 }
473 }
474 if (!args.empty() && curr.isVar())
475 {
476 // also add standard application version
477 args.insert(args.begin(), curr);
478 Node uf_n = nm->mkNode(APPLY_UF, args);
479 addTerm(uf_n, added, withinQuant, withinInstClosure);
480 }
481 }
482
getOperatorRepresentative(TNode op) const483 Node TermDb::getOperatorRepresentative( TNode op ) const {
484 std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
485 if( it!=d_ho_op_rep.end() ){
486 return it->second;
487 }else{
488 return op;
489 }
490 }
491
inRelevantDomain(TNode f,unsigned i,TNode r)492 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
493 if( options::ufHo() ){
494 f = getOperatorRepresentative( f );
495 }
496 computeUfTerms( f );
497 Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) ||
498 d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
499 std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
500 if( it != d_func_map_rel_dom.end() ){
501 std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
502 if( it2!=it->second.end() ){
503 return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
504 }else{
505 return false;
506 }
507 }else{
508 return false;
509 }
510 }
511
512 //return a term n' equivalent to n
513 // maximal subterms of n' are representatives in the equality engine qy
evaluateTerm2(TNode n,std::map<TNode,Node> & visited,EqualityQuery * qy,bool useEntailmentTests)514 Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) {
515 std::map< TNode, Node >::iterator itv = visited.find( n );
516 if( itv != visited.end() ){
517 return itv->second;
518 }
519 Trace("term-db-eval") << "evaluate term : " << n << std::endl;
520 Node ret = n;
521 if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
522 //do nothing
523 }else if( !qy->hasTerm( n ) ){
524 //term is not known to be equal to a representative in equality engine, evaluate it
525 if( n.hasOperator() ){
526 TNode f = getMatchOperator( n );
527 std::vector< TNode > args;
528 bool ret_set = false;
529 for( unsigned i=0; i<n.getNumChildren(); i++ ){
530 TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests );
531 if( c.isNull() ){
532 ret = Node::null();
533 ret_set = true;
534 break;
535 }else if( c==d_true || c==d_false ){
536 //short-circuiting
537 if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
538 ret = c;
539 ret_set = true;
540 break;
541 }else if( n.getKind()==kind::ITE && i==0 ){
542 ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests );
543 ret_set = true;
544 break;
545 }
546 }
547 Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
548 args.push_back( c );
549 }
550 if( !ret_set ){
551 //if it is an indexed term, return the congruent term
552 if( !f.isNull() ){
553 TNode nn = qy->getCongruentTerm( f, args );
554 Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
555 if( !nn.isNull() ){
556 ret = qy->getRepresentative( nn );
557 Trace("term-db-eval") << "return rep" << std::endl;
558 ret_set = true;
559 Assert( !ret.isNull() );
560 }
561 }
562 if( !ret_set ){
563 Trace("term-db-eval") << "return rewrite" << std::endl;
564 //a theory symbol or a new UF term
565 if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
566 args.insert( args.begin(), n.getOperator() );
567 }
568 ret = NodeManager::currentNM()->mkNode( n.getKind(), args );
569 ret = Rewriter::rewrite( ret );
570 if( ret.getKind()==kind::EQUAL ){
571 if( qy->areDisequal( ret[0], ret[1] ) ){
572 ret = d_false;
573 }
574 }
575 if( useEntailmentTests ){
576 if( ret.getKind()==kind::EQUAL || ret.getKind()==kind::GEQ ){
577 for( unsigned j=0; j<2; j++ ){
578 std::pair<bool, Node> et = d_quantEngine->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, j==0 ? ret : ret.negate() );
579 if( et.first ){
580 ret = j==0 ? d_true : d_false;
581 break;
582 }
583 }
584 }
585 }
586 }
587 }
588 }
589 }else{
590 Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
591 ret = qy->getRepresentative( n );
592 }
593 Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
594 visited[n] = ret;
595 return ret;
596 }
597
598
getEntailedTerm2(TNode n,std::map<TNode,TNode> & subs,bool subsRep,bool hasSubs,EqualityQuery * qy)599 TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
600 Assert( !qy->extendsEngine() );
601 Trace("term-db-entail") << "get entailed term : " << n << std::endl;
602 if( qy->getEngine()->hasTerm( n ) ){
603 Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
604 return n;
605 }else if( n.getKind()==BOUND_VARIABLE ){
606 if( hasSubs ){
607 std::map< TNode, TNode >::iterator it = subs.find( n );
608 if( it!=subs.end() ){
609 Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
610 if( subsRep ){
611 Assert( qy->getEngine()->hasTerm( it->second ) );
612 Assert( qy->getEngine()->getRepresentative( it->second )==it->second );
613 return it->second;
614 }else{
615 return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
616 }
617 }
618 }
619 }else if( n.getKind()==ITE ){
620 for( unsigned i=0; i<2; i++ ){
621 if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
622 return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
623 }
624 }
625 }else{
626 if( n.hasOperator() ){
627 TNode f = getMatchOperator( n );
628 if( !f.isNull() ){
629 std::vector< TNode > args;
630 for( unsigned i=0; i<n.getNumChildren(); i++ ){
631 TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
632 if( c.isNull() ){
633 return TNode::null();
634 }
635 c = qy->getEngine()->getRepresentative( c );
636 Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
637 args.push_back( c );
638 }
639 TNode nn = qy->getCongruentTerm( f, args );
640 Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl;
641 return nn;
642 }
643 }
644 }
645 return TNode::null();
646 }
647
evaluateTerm(TNode n,EqualityQuery * qy,bool useEntailmentTests)648 Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) {
649 if( qy==NULL ){
650 qy = d_quantEngine->getEqualityQuery();
651 }
652 std::map< TNode, Node > visited;
653 return evaluateTerm2( n, visited, qy, useEntailmentTests );
654 }
655
getEntailedTerm(TNode n,std::map<TNode,TNode> & subs,bool subsRep,EqualityQuery * qy)656 TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
657 if( qy==NULL ){
658 qy = d_quantEngine->getEqualityQuery();
659 }
660 return getEntailedTerm2( n, subs, subsRep, true, qy );
661 }
662
getEntailedTerm(TNode n,EqualityQuery * qy)663 TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
664 if( qy==NULL ){
665 qy = d_quantEngine->getEqualityQuery();
666 }
667 std::map< TNode, TNode > subs;
668 return getEntailedTerm2( n, subs, false, false, qy );
669 }
670
isEntailed2(TNode n,std::map<TNode,TNode> & subs,bool subsRep,bool hasSubs,bool pol,EqualityQuery * qy)671 bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
672 Assert( !qy->extendsEngine() );
673 Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
674 Assert( n.getType().isBoolean() );
675 if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
676 TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
677 if( !n1.isNull() ){
678 TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
679 if( !n2.isNull() ){
680 if( n1==n2 ){
681 return pol;
682 }else{
683 Assert( qy->getEngine()->hasTerm( n1 ) );
684 Assert( qy->getEngine()->hasTerm( n2 ) );
685 if( pol ){
686 return qy->getEngine()->areEqual( n1, n2 );
687 }else{
688 return qy->getEngine()->areDisequal( n1, n2, false );
689 }
690 }
691 }
692 }
693 }else if( n.getKind()==NOT ){
694 return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
695 }else if( n.getKind()==OR || n.getKind()==AND ){
696 bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
697 for( unsigned i=0; i<n.getNumChildren(); i++ ){
698 if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
699 if( simPol ){
700 return true;
701 }
702 }else{
703 if( !simPol ){
704 return false;
705 }
706 }
707 }
708 return !simPol;
709 //Boolean equality here
710 }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
711 for( unsigned i=0; i<2; i++ ){
712 if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
713 unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
714 bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
715 return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
716 }
717 }
718 }else if( n.getKind()==APPLY_UF ){
719 TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
720 if( !n1.isNull() ){
721 Assert( qy->hasTerm( n1 ) );
722 if( n1==d_true ){
723 return pol;
724 }else if( n1==d_false ){
725 return !pol;
726 }else{
727 return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
728 }
729 }
730 }else if( n.getKind()==FORALL && !pol ){
731 return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
732 }
733 return false;
734 }
735
isEntailed(TNode n,bool pol,EqualityQuery * qy)736 bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
737 if( qy==NULL ){
738 Assert( d_consistent_ee );
739 qy = d_quantEngine->getEqualityQuery();
740 }
741 std::map< TNode, TNode > subs;
742 return isEntailed2( n, subs, false, false, pol, qy );
743 }
744
isEntailed(TNode n,std::map<TNode,TNode> & subs,bool subsRep,bool pol,EqualityQuery * qy)745 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
746 if( qy==NULL ){
747 Assert( d_consistent_ee );
748 qy = d_quantEngine->getEqualityQuery();
749 }
750 return isEntailed2( n, subs, subsRep, true, pol, qy );
751 }
752
isTermActive(Node n)753 bool TermDb::isTermActive( Node n ) {
754 return d_inactive_map.find( n )==d_inactive_map.end();
755 //return !n.getAttribute(NoMatchAttribute());
756 }
757
setTermInactive(Node n)758 void TermDb::setTermInactive( Node n ) {
759 d_inactive_map[n] = true;
760 //Trace("term-db-debug2") << "set no match attribute" << std::endl;
761 //NoMatchAttribute nma;
762 //n.setAttribute(nma,true);
763 }
764
hasTermCurrent(Node n,bool useMode)765 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
766 if( !useMode ){
767 return d_has_map.find( n )!=d_has_map.end();
768 }else{
769 //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
770 if( options::termDbMode()==TERM_DB_ALL ){
771 return true;
772 }else if( options::termDbMode()==TERM_DB_RELEVANT ){
773 return d_has_map.find( n )!=d_has_map.end();
774 }else{
775 Assert( false );
776 return false;
777 }
778 }
779 }
780
isTermEligibleForInstantiation(TNode n,TNode f,bool print)781 bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
782 if( options::lteRestrictInstClosure() ){
783 //has to be both in inst closure and in ground assertions
784 if( !isInstClosure( n ) ){
785 Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
786 return false;
787 }
788 // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
789 if( !hasTermCurrent( n, false ) ){
790 Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
791 return false;
792 }
793 }
794 if( options::instMaxLevel()!=-1 ){
795 if( n.hasAttribute(InstLevelAttribute()) ){
796 int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
797 unsigned ml = fml>=0 ? fml : options::instMaxLevel();
798
799 if( n.getAttribute(InstLevelAttribute())>ml ){
800 Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
801 Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
802 return false;
803 }
804 }else{
805 if( options::instLevelInputOnly() ){
806 Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
807 return false;
808 }
809 }
810 }
811 return true;
812 }
813
getEligibleTermInEqc(TNode r)814 Node TermDb::getEligibleTermInEqc( TNode r ) {
815 if( isTermEligibleForInstantiation( r, TNode::null() ) ){
816 return r;
817 }else{
818 std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
819 if( it==d_term_elig_eqc.end() ){
820 Node h;
821 eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
822 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
823 while( h.isNull() && !eqc_i.isFinished() ){
824 TNode n = (*eqc_i);
825 ++eqc_i;
826 if( hasTermCurrent( n ) ){
827 h = n;
828 }
829 }
830 d_term_elig_eqc[r] = h;
831 return h;
832 }else{
833 return it->second;
834 }
835 }
836 }
837
isInstClosure(Node r)838 bool TermDb::isInstClosure( Node r ) {
839 return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
840 }
841
setHasTerm(Node n)842 void TermDb::setHasTerm( Node n ) {
843 Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
844 //if( inst::Trigger::isAtomicTrigger( n ) ){
845 if( d_has_map.find( n )==d_has_map.end() ){
846 d_has_map[n] = true;
847 for( unsigned i=0; i<n.getNumChildren(); i++ ){
848 setHasTerm( n[i] );
849 }
850 }
851 }
852
presolve()853 void TermDb::presolve() {
854 if( options::incrementalSolving() ){
855 // reset the caches that are SAT context-independent but user
856 // context-dependent
857 d_ops.clear();
858 d_op_map.clear();
859 d_type_map.clear();
860 d_processed.clear();
861 d_iclosure_processed.clear();
862 }
863 }
864
reset(Theory::Effort effort)865 bool TermDb::reset( Theory::Effort effort ){
866 d_op_nonred_count.clear();
867 d_arg_reps.clear();
868 d_func_map_trie.clear();
869 d_func_map_eqc_trie.clear();
870 d_func_map_rel_dom.clear();
871 d_consistent_ee = true;
872
873 eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
874
875 Assert(ee->consistent());
876 // if higher-order, add equalities for the purification terms now
877 if (options::ufHo())
878 {
879 Trace("quant-ho")
880 << "TermDb::reset : assert higher-order purify equalities..."
881 << std::endl;
882 for (std::pair<const Node, Node>& pp : d_ho_purify_to_term)
883 {
884 if (ee->hasTerm(pp.second)
885 && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
886 {
887 Node eq;
888 std::map<Node, Node>::iterator itpe = d_ho_purify_to_eq.find(pp.first);
889 if (itpe == d_ho_purify_to_eq.end())
890 {
891 eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
892 d_ho_purify_to_eq[pp.first] = eq;
893 }
894 else
895 {
896 eq = itpe->second;
897 }
898 Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
899 ee->assertEquality(eq, true, eq);
900 Assert(ee->consistent());
901 }
902 }
903 }
904
905 //compute has map
906 if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
907 d_has_map.clear();
908 d_term_elig_eqc.clear();
909 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
910 while( !eqcs_i.isFinished() ){
911 TNode r = (*eqcs_i);
912 bool addedFirst = false;
913 Node first;
914 //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
915 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
916 while( !eqc_i.isFinished() ){
917 TNode n = (*eqc_i);
918 if( first.isNull() ){
919 first = n;
920 }else{
921 if( !addedFirst ){
922 addedFirst = true;
923 setHasTerm( first );
924 }
925 setHasTerm( n );
926 }
927 ++eqc_i;
928 }
929 ++eqcs_i;
930 }
931 for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
932 Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
933 if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
934 context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
935 for (unsigned i = 0; it != it_end; ++ it, ++i) {
936 if( (*it).assertion.getKind()!=INST_CLOSURE ){
937 setHasTerm( (*it).assertion );
938 }
939 }
940 }
941 }
942 }
943 //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
944 for (const Node& n : d_iclosure_processed)
945 {
946 if( !ee->hasTerm( n ) ){
947 ee->addTerm( n );
948 }
949 }
950
951 if( options::ufHo() && options::hoMergeTermDb() ){
952 Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
953 // build operator representative map
954 d_ho_op_rep.clear();
955 d_ho_op_slaves.clear();
956 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
957 while( !eqcs_i.isFinished() ){
958 TNode r = (*eqcs_i);
959 if( r.getType().isFunction() ){
960 Trace("quant-ho") << " process function eqc " << r << std::endl;
961 Node first;
962 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
963 while( !eqc_i.isFinished() ){
964 TNode n = (*eqc_i);
965 Node n_use;
966 if (n.isVar())
967 {
968 n_use = n;
969 }
970 else
971 {
972 // use its purified variable, if it exists
973 std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(n);
974 if (itp != d_ho_fun_op_purify.end())
975 {
976 n_use = itp->second;
977 }
978 }
979 Trace("quant-ho") << " - process " << n_use << ", from " << n
980 << std::endl;
981 if (!n_use.isNull() && d_op_map.find(n_use) != d_op_map.end())
982 {
983 if (first.isNull())
984 {
985 first = n_use;
986 d_ho_op_rep[n_use] = n_use;
987 }
988 else
989 {
990 Trace("quant-ho") << " have : " << n_use << " == " << first
991 << ", type = " << n_use.getType() << std::endl;
992 d_ho_op_rep[n_use] = first;
993 d_ho_op_slaves[first].push_back(n_use);
994 }
995 }
996 ++eqc_i;
997 }
998 }
999 ++eqcs_i;
1000 }
1001 Trace("quant-ho") << "...finished compute equal functions." << std::endl;
1002 }
1003
1004 /*
1005 //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
1006 for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
1007 computeUfTerms( it->first );
1008 if( !d_consistent_ee ){
1009 return false;
1010 }
1011 }
1012 */
1013 return true;
1014 }
1015
getTermArgTrie(Node f)1016 TNodeTrie* TermDb::getTermArgTrie(Node f)
1017 {
1018 if( options::ufHo() ){
1019 f = getOperatorRepresentative( f );
1020 }
1021 computeUfTerms( f );
1022 std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1023 if( itut!=d_func_map_trie.end() ){
1024 return &itut->second;
1025 }else{
1026 return NULL;
1027 }
1028 }
1029
getTermArgTrie(Node eqc,Node f)1030 TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
1031 {
1032 if( options::ufHo() ){
1033 f = getOperatorRepresentative( f );
1034 }
1035 computeUfEqcTerms( f );
1036 std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
1037 if( itut==d_func_map_eqc_trie.end() ){
1038 return NULL;
1039 }else{
1040 if( eqc.isNull() ){
1041 return &itut->second;
1042 }else{
1043 std::map<TNode, TNodeTrie>::iterator itute =
1044 itut->second.d_data.find(eqc);
1045 if( itute!=itut->second.d_data.end() ){
1046 return &itute->second;
1047 }else{
1048 return NULL;
1049 }
1050 }
1051 }
1052 }
1053
getCongruentTerm(Node f,Node n)1054 TNode TermDb::getCongruentTerm( Node f, Node n ) {
1055 if( options::ufHo() ){
1056 f = getOperatorRepresentative( f );
1057 }
1058 computeUfTerms( f );
1059 std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1060 if( itut!=d_func_map_trie.end() ){
1061 computeArgReps( n );
1062 return itut->second.existsTerm( d_arg_reps[n] );
1063 }else{
1064 return TNode::null();
1065 }
1066 }
1067
getCongruentTerm(Node f,std::vector<TNode> & args)1068 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
1069 if( options::ufHo() ){
1070 f = getOperatorRepresentative( f );
1071 }
1072 computeUfTerms( f );
1073 return d_func_map_trie[f].existsTerm( args );
1074 }
1075
1076 }/* CVC4::theory::quantifiers namespace */
1077 }/* CVC4::theory namespace */
1078 }/* CVC4 namespace */
1079