1 /********************* */
2 /*! \file term_database.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Implementation of term databse class
15 #include "theory/quantifiers/term_database.h"
17 #include "options/base_options.h"
18 #include "options/quantifiers_options.h"
19 #include "options/smt_options.h"
20 #include "options/theory_options.h"
21 #include "options/uf_options.h"
22 #include "theory/quantifiers/ematching/trigger_term_info.h"
23 #include "theory/quantifiers/quantifiers_attributes.h"
24 #include "theory/quantifiers/term_util.h"
25 #include "theory/quantifiers_engine.h"
26 #include "theory/theory_engine.h"
29 using namespace CVC4::kind
;
30 using namespace CVC4::context
;
31 using namespace CVC4::theory::inst
;
35 namespace quantifiers
{
37 TermDb::TermDb(QuantifiersState
& qs
,
38 QuantifiersInferenceManager
& qim
,
39 QuantifiersEngine
* qe
)
43 d_inactive_map(qs
.getSatContext())
45 d_consistent_ee
= true;
46 d_true
= NodeManager::currentNM()->mkConst(true);
47 d_false
= NodeManager::currentNM()->mkConst(false);
54 void TermDb::registerQuantifier( Node q
) {
55 Assert(q
[0].getNumChildren()
56 == d_quantEngine
->getTermUtil()->getNumInstantiationConstants(q
));
57 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
58 Node ic
= d_quantEngine
->getTermUtil()->getInstantiationConstant( q
, i
);
59 setTermInactive( ic
);
63 unsigned TermDb::getNumOperators() { return d_ops
.size(); }
64 Node
TermDb::getOperator(unsigned i
)
66 Assert(i
< d_ops
.size());
71 unsigned TermDb::getNumGroundTerms(Node f
) const
73 std::map
<Node
, std::vector
<Node
> >::const_iterator it
= d_op_map
.find(f
);
74 if( it
!=d_op_map
.end() ){
75 return it
->second
.size();
81 Node
TermDb::getGroundTerm(Node f
, unsigned i
) const
83 std::map
<Node
, std::vector
<Node
> >::const_iterator it
= d_op_map
.find(f
);
84 if (it
!= d_op_map
.end())
86 Assert(i
< it
->second
.size());
96 unsigned TermDb::getNumTypeGroundTerms(TypeNode tn
) const
98 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
100 if( it
!=d_type_map
.end() ){
101 return it
->second
.size();
107 Node
TermDb::getTypeGroundTerm(TypeNode tn
, unsigned i
) const
109 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
111 if (it
!= d_type_map
.end())
113 Assert(i
< it
->second
.size());
114 return it
->second
[i
];
123 Node
TermDb::getOrMakeTypeGroundTerm(TypeNode tn
, bool reqVar
)
125 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
127 if (it
!= d_type_map
.end())
129 Assert(!it
->second
.empty());
132 return it
->second
[0];
134 for (const Node
& v
: it
->second
)
142 return getOrMakeTypeFreshVariable(tn
);
145 Node
TermDb::getOrMakeTypeFreshVariable(TypeNode tn
)
147 std::unordered_map
<TypeNode
, Node
, TypeNodeHashFunction
>::iterator it
=
149 if (it
== d_type_fv
.end())
151 std::stringstream ss
;
152 ss
<< language::SetLanguage(options::outputLanguage());
154 Node k
= NodeManager::currentNM()->mkSkolem(
155 ss
.str(), tn
, "is a termDb fresh variable");
156 Trace("mkVar") << "TermDb:: Make variable " << k
<< " : " << tn
158 if (options::instMaxLevel() != -1)
160 QuantAttributes::setInstantiationLevelAttr(k
, 0);
171 Node
TermDb::getMatchOperator( Node n
) {
172 Kind k
= n
.getKind();
173 //datatype operators may be parametric, always assume they are
174 if (k
== SELECT
|| k
== STORE
|| k
== UNION
|| k
== INTERSECTION
175 || k
== SUBSET
|| k
== SETMINUS
|| k
== MEMBER
|| k
== SINGLETON
176 || k
== APPLY_SELECTOR_TOTAL
|| k
== APPLY_SELECTOR
|| k
== APPLY_TESTER
177 || k
== SEP_PTO
|| k
== HO_APPLY
|| k
== SEQ_NTH
)
179 //since it is parametric, use a particular one as op
180 TypeNode tn
= n
[0].getType();
181 Node op
= n
.getOperator();
182 std::map
< Node
, std::map
< TypeNode
, Node
> >::iterator ito
= d_par_op_map
.find( op
);
183 if( ito
!=d_par_op_map
.end() ){
184 std::map
< TypeNode
, Node
>::iterator it
= ito
->second
.find( tn
);
185 if( it
!=ito
->second
.end() ){
189 Trace("par-op") << "Parametric operator : " << k
<< ", " << n
.getOperator() << ", " << tn
<< " : " << n
<< std::endl
;
190 d_par_op_map
[op
][tn
] = n
;
193 else if (inst::TriggerTermInfo::isAtomicTriggerKind(k
))
195 return n
.getOperator();
201 void TermDb::addTerm(Node n
,
202 std::set
<Node
>& added
,
204 bool withinInstClosure
)
206 //don't add terms in quantifier bodies
207 if( withinQuant
&& !options::registerQuantBodyTerms() ){
211 if (d_processed
.find(n
) == d_processed
.end())
213 d_processed
.insert(n
);
214 if (!TermUtil::hasInstConstAttr(n
))
216 Trace("term-db-debug") << "register term : " << n
<< std::endl
;
217 d_type_map
[n
.getType()].push_back(n
);
218 // if this is an atomic trigger, consider adding it
219 if (inst::TriggerTermInfo::isAtomicTrigger(n
))
221 Trace("term-db") << "register term in db " << n
<< std::endl
;
223 Node op
= getMatchOperator(n
);
224 Trace("term-db-debug") << " match operator is : " << op
<< std::endl
;
225 if (d_op_map
.find(op
) == d_op_map
.end())
229 d_op_map
[op
].push_back(n
);
231 // If we are higher-order, we may need to register more terms.
234 addTermHo(n
, added
, withinQuant
, withinInstClosure
);
244 if (withinInstClosure
245 && d_iclosure_processed
.find(n
) == d_iclosure_processed
.end())
247 d_iclosure_processed
.insert(n
);
250 if (rec
&& !n
.isClosure())
252 for (const Node
& nc
: n
)
254 addTerm(nc
, added
, withinQuant
, withinInstClosure
);
259 void TermDb::computeArgReps( TNode n
) {
260 if (d_arg_reps
.find(n
) == d_arg_reps
.end())
262 eq::EqualityEngine
* ee
= d_qstate
.getEqualityEngine();
263 for (const TNode
& nc
: n
)
265 TNode r
= ee
->hasTerm(nc
) ? ee
->getRepresentative(nc
) : nc
;
266 d_arg_reps
[n
].push_back( r
);
271 void TermDb::computeUfEqcTerms( TNode f
) {
272 Assert(f
== getOperatorRepresentative(f
));
273 if (d_func_map_eqc_trie
.find(f
) != d_func_map_eqc_trie
.end())
277 d_func_map_eqc_trie
[f
].clear();
278 // get the matchable operators in the equivalence class of f
279 std::vector
<TNode
> ops
;
283 ops
.insert(ops
.end(), d_ho_op_slaves
[f
].begin(), d_ho_op_slaves
[f
].end());
285 eq::EqualityEngine
* ee
= d_qstate
.getEqualityEngine();
288 for (const Node
& n
: d_op_map
[ff
])
290 if (hasTermCurrent(n
) && isTermActive(n
))
293 TNode r
= ee
->hasTerm(n
) ? ee
->getRepresentative(n
) : TNode(n
);
294 d_func_map_eqc_trie
[f
].d_data
[r
].addTerm(n
, d_arg_reps
[n
]);
300 void TermDb::computeUfTerms( TNode f
) {
301 if (d_op_nonred_count
.find(f
) != d_op_nonred_count
.end())
306 Assert(f
== getOperatorRepresentative(f
));
307 d_op_nonred_count
[f
] = 0;
308 // get the matchable operators in the equivalence class of f
309 std::vector
<TNode
> ops
;
313 ops
.insert(ops
.end(), d_ho_op_slaves
[f
].begin(), d_ho_op_slaves
[f
].end());
315 Trace("term-db-debug") << "computeUfTerms for " << f
<< std::endl
;
316 unsigned congruentCount
= 0;
317 unsigned nonCongruentCount
= 0;
318 unsigned alreadyCongruentCount
= 0;
319 unsigned relevantCount
= 0;
320 NodeManager
* nm
= NodeManager::currentNM();
323 std::map
<Node
, std::vector
<Node
> >::iterator it
= d_op_map
.find(ff
);
324 if (it
== d_op_map
.end())
326 // no terms for this operator
329 Trace("term-db-debug") << "Adding terms for operator " << ff
<< std::endl
;
330 for (const Node
& n
: it
->second
)
332 // to be added to term index, term must be relevant, and exist in EE
333 if (!hasTermCurrent(n
) || !d_qstate
.hasTerm(n
))
335 Trace("term-db-debug") << n
<< " is not relevant." << std::endl
;
340 if (!isTermActive(n
))
342 Trace("term-db-debug") << n
<< " is already redundant." << std::endl
;
343 alreadyCongruentCount
++;
348 Trace("term-db-debug") << "Adding term " << n
<< " with arg reps : ";
349 for (unsigned i
= 0, size
= d_arg_reps
[n
].size(); i
< size
; i
++)
351 Trace("term-db-debug") << d_arg_reps
[n
][i
] << " ";
352 if (std::find(d_func_map_rel_dom
[f
][i
].begin(),
353 d_func_map_rel_dom
[f
][i
].end(),
355 == d_func_map_rel_dom
[f
][i
].end())
357 d_func_map_rel_dom
[f
][i
].push_back(d_arg_reps
[n
][i
]);
360 Trace("term-db-debug") << std::endl
;
361 Assert(d_qstate
.hasTerm(n
));
362 Trace("term-db-debug")
363 << " and value : " << d_qstate
.getRepresentative(n
) << std::endl
;
364 Node at
= d_func_map_trie
[f
].addOrGetTerm(n
, d_arg_reps
[n
]);
365 Assert(d_qstate
.hasTerm(at
));
366 Trace("term-db-debug2") << "...add term returned " << at
<< std::endl
;
367 if (at
!= n
&& d_qstate
.areEqual(at
, n
))
370 Trace("term-db-debug") << n
<< " is redundant." << std::endl
;
374 if (d_qstate
.areDisequal(at
, n
))
376 std::vector
<Node
> lits
;
377 lits
.push_back(nm
->mkNode(EQUAL
, at
, n
));
381 // operators might be disequal
384 Node atf
= getMatchOperator(at
);
385 Node nf
= getMatchOperator(n
);
388 if (at
.getKind() == APPLY_UF
&& n
.getKind() == APPLY_UF
)
390 lits
.push_back(atf
.eqNode(nf
).negate());
402 Assert(at
.getNumChildren() == n
.getNumChildren());
403 for (unsigned k
= 0, size
= at
.getNumChildren(); k
< size
; k
++)
407 lits
.push_back(nm
->mkNode(EQUAL
, at
[k
], n
[k
]).negate());
410 Node lem
= lits
.size() == 1 ? lits
[0] : nm
->mkNode(OR
, lits
);
411 if (Trace
.isOn("term-db-lemma"))
413 Trace("term-db-lemma") << "Disequal congruent terms : " << at
<< " "
414 << n
<< "!!!!" << std::endl
;
415 if (!d_qstate
.getValuation().needCheck())
417 Trace("term-db-lemma") << " all theories passed with no lemmas."
419 // we should be a full effort check, prior to theory combination
421 Trace("term-db-lemma") << " add lemma : " << lem
<< std::endl
;
423 d_quantEngine
->addLemma(lem
);
424 d_qstate
.notifyInConflict();
425 d_consistent_ee
= false;
430 d_op_nonred_count
[f
]++;
432 if (Trace
.isOn("tdb"))
434 Trace("tdb") << "Term db size [" << f
<< "] : " << nonCongruentCount
436 Trace("tdb") << (nonCongruentCount
+ congruentCount
) << " / "
437 << (nonCongruentCount
+ congruentCount
438 + alreadyCongruentCount
)
440 Trace("tdb") << relevantCount
<< " / " << it
->second
.size() << std::endl
;
445 void TermDb::addTermHo(Node n
,
446 std::set
<Node
>& added
,
448 bool withinInstClosure
)
450 Assert(options::ufHo());
451 if (n
.getType().isFunction())
453 // nothing special to do with functions
456 NodeManager
* nm
= NodeManager::currentNM();
458 std::vector
<Node
> args
;
459 while (curr
.getKind() == HO_APPLY
)
461 args
.insert(args
.begin(), curr
[1]);
466 std::map
<Node
, Node
>::iterator itp
= d_ho_fun_op_purify
.find(curr
);
468 if (itp
== d_ho_fun_op_purify
.end())
470 psk
= nm
->mkSkolem("pfun",
472 "purify for function operator term indexing");
473 d_ho_fun_op_purify
[curr
] = psk
;
474 // we do not add it to d_ops since it is an internal operator
480 std::vector
<Node
> children
;
481 children
.push_back(psk
);
482 children
.insert(children
.end(), args
.begin(), args
.end());
483 Node p_n
= nm
->mkNode(APPLY_UF
, children
);
484 Trace("term-db") << "register term in db (via purify) " << p_n
486 // also add this one internally
487 d_op_map
[psk
].push_back(p_n
);
488 // maintain backwards mapping
489 d_ho_purify_to_term
[p_n
] = n
;
492 if (!args
.empty() && curr
.isVar())
494 // also add standard application version
495 args
.insert(args
.begin(), curr
);
496 Node uf_n
= nm
->mkNode(APPLY_UF
, args
);
497 addTerm(uf_n
, added
, withinQuant
, withinInstClosure
);
501 Node
TermDb::getOperatorRepresentative( TNode op
) const {
502 std::map
< TNode
, TNode
>::const_iterator it
= d_ho_op_rep
.find( op
);
503 if( it
!=d_ho_op_rep
.end() ){
510 bool TermDb::inRelevantDomain( TNode f
, unsigned i
, TNode r
) {
511 if( options::ufHo() ){
512 f
= getOperatorRepresentative( f
);
515 Assert(!d_qstate
.getEqualityEngine()->hasTerm(r
)
516 || d_qstate
.getEqualityEngine()->getRepresentative(r
) == r
);
517 std::map
< Node
, std::map
< unsigned, std::vector
< Node
> > >::iterator it
= d_func_map_rel_dom
.find( f
);
518 if( it
!= d_func_map_rel_dom
.end() ){
519 std::map
< unsigned, std::vector
< Node
> >::iterator it2
= it
->second
.find( i
);
520 if( it2
!=it
->second
.end() ){
521 return std::find( it2
->second
.begin(), it2
->second
.end(), r
)!=it2
->second
.end();
530 Node
TermDb::evaluateTerm2(TNode n
,
531 std::map
<TNode
, Node
>& visited
,
532 std::vector
<Node
>& exp
,
533 bool useEntailmentTests
,
537 std::map
< TNode
, Node
>::iterator itv
= visited
.find( n
);
538 if( itv
!= visited
.end() ){
541 size_t prevSize
= exp
.size();
542 Trace("term-db-eval") << "evaluate term : " << n
<< std::endl
;
544 if( n
.getKind()==FORALL
|| n
.getKind()==BOUND_VARIABLE
){
547 else if (d_qstate
.hasTerm(n
))
549 Trace("term-db-eval") << "...exists in ee, return rep" << std::endl
;
550 ret
= d_qstate
.getRepresentative(n
);
555 exp
.push_back(n
.eqNode(ret
));
560 else if (n
.hasOperator())
562 std::vector
<TNode
> args
;
563 bool ret_set
= false;
564 Kind k
= n
.getKind();
565 std::vector
<Node
> tempExp
;
566 for (unsigned i
= 0, nchild
= n
.getNumChildren(); i
< nchild
; i
++)
568 TNode c
= evaluateTerm2(n
[i
],
580 else if (c
== d_true
|| c
== d_false
)
583 if ((k
== AND
&& c
== d_false
) || (k
== OR
&& c
== d_true
))
590 else if (k
== ITE
&& i
== 0)
592 ret
= evaluateTerm2(n
[c
== d_true
? 1 : 2],
605 exp
.insert(exp
.end(), tempExp
.begin(), tempExp
.end());
607 Trace("term-db-eval") << " child " << i
<< " : " << c
<< std::endl
;
612 // if we short circuited
616 exp
.insert(exp
.end(), tempExp
.begin(), tempExp
.end());
621 // get the (indexed) operator of n, if it exists
622 TNode f
= getMatchOperator(n
);
623 // if it is an indexed term, return the congruent term
626 // if f is congruent to a term indexed by this class
627 TNode nn
= getCongruentTerm(f
, args
);
628 Trace("term-db-eval") << " got congruent term " << nn
629 << " from DB for " << n
<< std::endl
;
634 Assert(nn
.getNumChildren() == n
.getNumChildren());
635 for (unsigned i
= 0, nchild
= nn
.getNumChildren(); i
< nchild
; i
++)
639 exp
.push_back(nn
[i
].eqNode(n
[i
]));
643 ret
= d_qstate
.getRepresentative(nn
);
644 Trace("term-db-eval") << "return rep" << std::endl
;
647 Assert(!ret
.isNull());
652 exp
.push_back(nn
.eqNode(ret
));
658 Trace("term-db-eval") << "return rewrite" << std::endl
;
659 // a theory symbol or a new UF term
660 if (n
.getMetaKind() == metakind::PARAMETERIZED
)
662 args
.insert(args
.begin(), n
.getOperator());
664 ret
= NodeManager::currentNM()->mkNode(n
.getKind(), args
);
665 ret
= Rewriter::rewrite(ret
);
666 if (ret
.getKind() == EQUAL
)
668 if (d_qstate
.areDisequal(ret
[0], ret
[1]))
673 if (useEntailmentTests
)
675 if (ret
.getKind() == EQUAL
|| ret
.getKind() == GEQ
)
677 TheoryEngine
* te
= d_quantEngine
->getTheoryEngine();
678 for (unsigned j
= 0; j
< 2; j
++)
680 std::pair
<bool, Node
> et
= te
->entailmentCheck(
681 options::TheoryOfMode::THEORY_OF_TYPE_BASED
,
682 j
== 0 ? ret
: ret
.negate());
685 ret
= j
== 0 ? d_true
: d_false
;
688 exp
.push_back(et
.second
);
698 // must have the term
699 if (reqHasTerm
&& !ret
.isNull())
701 Kind k
= ret
.getKind();
702 if (k
!= OR
&& k
!= AND
&& k
!= EQUAL
&& k
!= ITE
&& k
!= NOT
705 if (!d_qstate
.hasTerm(ret
))
711 Trace("term-db-eval") << "evaluated term : " << n
<< ", got : " << ret
712 << ", reqHasTerm = " << reqHasTerm
<< std::endl
;
713 // clear the explanation if failed
714 if (computeExp
&& ret
.isNull())
716 exp
.resize(prevSize
);
722 TNode
TermDb::getEntailedTerm2(TNode n
,
723 std::map
<TNode
, TNode
>& subs
,
727 Trace("term-db-entail") << "get entailed term : " << n
<< std::endl
;
728 if (d_qstate
.hasTerm(n
))
730 Trace("term-db-entail") << "...exists in ee, return rep " << std::endl
;
732 }else if( n
.getKind()==BOUND_VARIABLE
){
734 std::map
< TNode
, TNode
>::iterator it
= subs
.find( n
);
735 if( it
!=subs
.end() ){
736 Trace("term-db-entail") << "...substitution is : " << it
->second
<< std::endl
;
738 Assert(d_qstate
.hasTerm(it
->second
));
739 Assert(d_qstate
.getRepresentative(it
->second
) == it
->second
);
742 return getEntailedTerm2(it
->second
, subs
, subsRep
, hasSubs
);
745 }else if( n
.getKind()==ITE
){
746 for( unsigned i
=0; i
<2; i
++ ){
747 if (isEntailed2(n
[0], subs
, subsRep
, hasSubs
, i
== 0))
749 return getEntailedTerm2(n
[i
== 0 ? 1 : 2], subs
, subsRep
, hasSubs
);
753 if( n
.hasOperator() ){
754 TNode f
= getMatchOperator( n
);
756 std::vector
< TNode
> args
;
757 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
758 TNode c
= getEntailedTerm2(n
[i
], subs
, subsRep
, hasSubs
);
760 return TNode::null();
762 c
= d_qstate
.getRepresentative(c
);
763 Trace("term-db-entail") << " child " << i
<< " : " << c
<< std::endl
;
766 TNode nn
= getCongruentTerm(f
, args
);
767 Trace("term-db-entail") << " got congruent term " << nn
<< " for " << n
<< std::endl
;
772 return TNode::null();
775 Node
TermDb::evaluateTerm(TNode n
,
776 bool useEntailmentTests
,
779 std::map
< TNode
, Node
> visited
;
780 std::vector
<Node
> exp
;
781 return evaluateTerm2(n
, visited
, exp
, useEntailmentTests
, false, reqHasTerm
);
784 Node
TermDb::evaluateTerm(TNode n
,
785 std::vector
<Node
>& exp
,
786 bool useEntailmentTests
,
789 std::map
<TNode
, Node
> visited
;
790 return evaluateTerm2(n
, visited
, exp
, useEntailmentTests
, true, reqHasTerm
);
793 TNode
TermDb::getEntailedTerm(TNode n
,
794 std::map
<TNode
, TNode
>& subs
,
797 return getEntailedTerm2(n
, subs
, subsRep
, true);
800 TNode
TermDb::getEntailedTerm(TNode n
)
802 std::map
< TNode
, TNode
> subs
;
803 return getEntailedTerm2(n
, subs
, false, false);
806 bool TermDb::isEntailed2(
807 TNode n
, std::map
<TNode
, TNode
>& subs
, bool subsRep
, bool hasSubs
, bool pol
)
809 Trace("term-db-entail") << "Check entailed : " << n
<< ", pol = " << pol
<< std::endl
;
810 Assert(n
.getType().isBoolean());
811 if( n
.getKind()==EQUAL
&& !n
[0].getType().isBoolean() ){
812 TNode n1
= getEntailedTerm2(n
[0], subs
, subsRep
, hasSubs
);
814 TNode n2
= getEntailedTerm2(n
[1], subs
, subsRep
, hasSubs
);
819 Assert(d_qstate
.hasTerm(n1
));
820 Assert(d_qstate
.hasTerm(n2
));
822 return d_qstate
.areEqual(n1
, n2
);
824 return d_qstate
.areDisequal(n1
, n2
);
829 }else if( n
.getKind()==NOT
){
830 return isEntailed2(n
[0], subs
, subsRep
, hasSubs
, !pol
);
831 }else if( n
.getKind()==OR
|| n
.getKind()==AND
){
832 bool simPol
= ( pol
&& n
.getKind()==OR
) || ( !pol
&& n
.getKind()==AND
);
833 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
834 if (isEntailed2(n
[i
], subs
, subsRep
, hasSubs
, pol
))
846 //Boolean equality here
847 }else if( n
.getKind()==EQUAL
|| n
.getKind()==ITE
){
848 for( unsigned i
=0; i
<2; i
++ ){
849 if (isEntailed2(n
[0], subs
, subsRep
, hasSubs
, i
== 0))
851 unsigned ch
= ( n
.getKind()==EQUAL
|| i
==0 ) ? 1 : 2;
852 bool reqPol
= ( n
.getKind()==ITE
|| i
==0 ) ? pol
: !pol
;
853 return isEntailed2(n
[ch
], subs
, subsRep
, hasSubs
, reqPol
);
856 }else if( n
.getKind()==APPLY_UF
){
857 TNode n1
= getEntailedTerm2(n
, subs
, subsRep
, hasSubs
);
859 Assert(d_qstate
.hasTerm(n1
));
862 }else if( n1
==d_false
){
865 return d_qstate
.getRepresentative(n1
) == (pol
? d_true
: d_false
);
868 }else if( n
.getKind()==FORALL
&& !pol
){
869 return isEntailed2(n
[1], subs
, subsRep
, hasSubs
, pol
);
874 bool TermDb::isEntailed(TNode n
, bool pol
)
876 Assert(d_consistent_ee
);
877 std::map
< TNode
, TNode
> subs
;
878 return isEntailed2(n
, subs
, false, false, pol
);
881 bool TermDb::isEntailed(TNode n
,
882 std::map
<TNode
, TNode
>& subs
,
886 Assert(d_consistent_ee
);
887 return isEntailed2(n
, subs
, subsRep
, true, pol
);
890 bool TermDb::isTermActive( Node n
) {
891 return d_inactive_map
.find( n
)==d_inactive_map
.end();
892 //return !n.getAttribute(NoMatchAttribute());
895 void TermDb::setTermInactive( Node n
) {
896 d_inactive_map
[n
] = true;
897 //Trace("term-db-debug2") << "set no match attribute" << std::endl;
898 //NoMatchAttribute nma;
899 //n.setAttribute(nma,true);
902 bool TermDb::hasTermCurrent( Node n
, bool useMode
) {
904 return d_has_map
.find( n
)!=d_has_map
.end();
906 //some assertions are not sent to EE
907 if (options::termDbMode() == options::TermDbMode::ALL
)
911 else if (options::termDbMode() == options::TermDbMode::RELEVANT
)
913 return d_has_map
.find( n
)!=d_has_map
.end();
915 Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
919 bool TermDb::isTermEligibleForInstantiation(TNode n
, TNode f
)
921 if( options::lteRestrictInstClosure() ){
922 //has to be both in inst closure and in ground assertions
923 if( !isInstClosure( n
) ){
924 Trace("inst-add-debug") << "Term " << n
<< " is not an inst-closure term." << std::endl
;
927 // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
928 if( !hasTermCurrent( n
, false ) ){
929 Trace("inst-add-debug") << "Term " << n
<< " is not in a ground assertion." << std::endl
;
933 if( options::instMaxLevel()!=-1 ){
934 if( n
.hasAttribute(InstLevelAttribute()) ){
935 int fml
= f
.isNull() ? -1 : d_quantEngine
->getQuantAttributes()->getQuantInstLevel( f
);
936 unsigned ml
= fml
>=0 ? fml
: options::instMaxLevel();
938 if( n
.getAttribute(InstLevelAttribute())>ml
){
939 Trace("inst-add-debug") << "Term " << n
<< " has instantiation level " << n
.getAttribute(InstLevelAttribute());
940 Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml
<< " for this quantified formula." << std::endl
;
944 if( options::instLevelInputOnly() ){
945 Trace("inst-add-debug") << "Term " << n
<< " does not have an instantiation level." << std::endl
;
950 // it cannot have instantiation constants, which originate from
951 // counterexample-guided instantiation strategies.
952 return !TermUtil::hasInstConstAttr(n
);
955 Node
TermDb::getEligibleTermInEqc( TNode r
) {
956 if( isTermEligibleForInstantiation( r
, TNode::null() ) ){
959 std::map
< Node
, Node
>::iterator it
= d_term_elig_eqc
.find( r
);
960 if( it
==d_term_elig_eqc
.end() ){
962 eq::EqualityEngine
* ee
= d_qstate
.getEqualityEngine();
963 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
, ee
);
964 while (!eqc_i
.isFinished())
968 if (isTermEligibleForInstantiation(n
, TNode::null()))
974 d_term_elig_eqc
[r
] = h
;
982 bool TermDb::isInstClosure( Node r
) {
983 return d_iclosure_processed
.find( r
)!=d_iclosure_processed
.end();
986 void TermDb::setHasTerm( Node n
) {
987 Trace("term-db-debug2") << "hasTerm : " << n
<< std::endl
;
988 if( d_has_map
.find( n
)==d_has_map
.end() ){
990 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
996 void TermDb::presolve() {
997 if( options::incrementalSolving() ){
998 // reset the caches that are SAT context-independent but user
1003 d_processed
.clear();
1004 d_iclosure_processed
.clear();
1008 bool TermDb::reset( Theory::Effort effort
){
1009 d_op_nonred_count
.clear();
1011 d_func_map_trie
.clear();
1012 d_func_map_eqc_trie
.clear();
1013 d_func_map_rel_dom
.clear();
1014 d_consistent_ee
= true;
1016 eq::EqualityEngine
* ee
= d_qstate
.getEqualityEngine();
1018 Assert(ee
->consistent());
1019 // if higher-order, add equalities for the purification terms now
1020 if (options::ufHo())
1023 << "TermDb::reset : assert higher-order purify equalities..."
1025 for (std::pair
<const Node
, Node
>& pp
: d_ho_purify_to_term
)
1027 if (ee
->hasTerm(pp
.second
)
1028 && (!ee
->hasTerm(pp
.first
) || !ee
->areEqual(pp
.second
, pp
.first
)))
1031 std::map
<Node
, Node
>::iterator itpe
= d_ho_purify_to_eq
.find(pp
.first
);
1032 if (itpe
== d_ho_purify_to_eq
.end())
1034 eq
= Rewriter::rewrite(pp
.first
.eqNode(pp
.second
));
1035 d_ho_purify_to_eq
[pp
.first
] = eq
;
1041 Trace("quant-ho") << "- assert purify equality : " << eq
<< std::endl
;
1042 ee
->assertEquality(eq
, true, eq
);
1043 if (!ee
->consistent())
1045 // In some rare cases, purification functions (in the domain of
1046 // d_ho_purify_to_term) may escape the term database. For example,
1047 // matching algorithms may construct instantiations involving these
1048 // functions. As a result, asserting these equalities internally may
1049 // cause a conflict. In this case, we insist that the purification
1050 // equality is sent out as a lemma here.
1051 Trace("term-db-lemma")
1052 << "Purify equality lemma: " << eq
<< std::endl
;
1053 d_quantEngine
->addLemma(eq
);
1054 d_qstate
.notifyInConflict();
1055 d_consistent_ee
= false;
1063 if (options::termDbMode() == options::TermDbMode::RELEVANT
1064 || options::lteRestrictInstClosure())
1067 d_term_elig_eqc
.clear();
1068 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1069 while( !eqcs_i
.isFinished() ){
1070 TNode r
= (*eqcs_i
);
1071 bool addedFirst
= false;
1073 //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
1074 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
, ee
);
1075 while( !eqc_i
.isFinished() ){
1077 if( first
.isNull() ){
1082 setHasTerm( first
);
1090 TheoryEngine
* te
= d_quantEngine
->getTheoryEngine();
1091 const LogicInfo
& logicInfo
= te
->getLogicInfo();
1092 for (TheoryId theoryId
= THEORY_FIRST
; theoryId
< THEORY_LAST
; ++theoryId
)
1094 if (!logicInfo
.isTheoryEnabled(theoryId
))
1098 Theory
* theory
= te
->theoryOf(theoryId
);
1099 Assert(theory
!= nullptr);
1100 for (context::CDList
<Assertion
>::const_iterator
1101 it
= theory
->facts_begin(),
1102 it_end
= theory
->facts_end();
1106 if ((*it
).d_assertion
.getKind() != INST_CLOSURE
)
1108 setHasTerm((*it
).d_assertion
);
1113 //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
1114 for (const Node
& n
: d_iclosure_processed
)
1116 if (!ee
->hasTerm(n
))
1122 if( options::ufHo() && options::hoMergeTermDb() ){
1123 Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl
;
1124 // build operator representative map
1125 d_ho_op_rep
.clear();
1126 d_ho_op_slaves
.clear();
1127 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1128 while( !eqcs_i
.isFinished() ){
1129 TNode r
= (*eqcs_i
);
1130 if( r
.getType().isFunction() ){
1131 Trace("quant-ho") << " process function eqc " << r
<< std::endl
;
1133 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
, ee
);
1134 while( !eqc_i
.isFinished() ){
1143 // use its purified variable, if it exists
1144 std::map
<Node
, Node
>::iterator itp
= d_ho_fun_op_purify
.find(n
);
1145 if (itp
!= d_ho_fun_op_purify
.end())
1147 n_use
= itp
->second
;
1150 Trace("quant-ho") << " - process " << n_use
<< ", from " << n
1152 if (!n_use
.isNull() && d_op_map
.find(n_use
) != d_op_map
.end())
1157 d_ho_op_rep
[n_use
] = n_use
;
1161 Trace("quant-ho") << " have : " << n_use
<< " == " << first
1162 << ", type = " << n_use
.getType() << std::endl
;
1163 d_ho_op_rep
[n_use
] = first
;
1164 d_ho_op_slaves
[first
].push_back(n_use
);
1172 Trace("quant-ho") << "...finished compute equal functions." << std::endl
;
1176 //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
1177 for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
1178 computeUfTerms( it->first );
1179 if( !d_consistent_ee ){
1187 TNodeTrie
* TermDb::getTermArgTrie(Node f
)
1189 if( options::ufHo() ){
1190 f
= getOperatorRepresentative( f
);
1192 computeUfTerms( f
);
1193 std::map
<Node
, TNodeTrie
>::iterator itut
= d_func_map_trie
.find(f
);
1194 if( itut
!=d_func_map_trie
.end() ){
1195 return &itut
->second
;
1201 TNodeTrie
* TermDb::getTermArgTrie(Node eqc
, Node f
)
1203 if( options::ufHo() ){
1204 f
= getOperatorRepresentative( f
);
1206 computeUfEqcTerms( f
);
1207 std::map
<Node
, TNodeTrie
>::iterator itut
= d_func_map_eqc_trie
.find(f
);
1208 if( itut
==d_func_map_eqc_trie
.end() ){
1212 return &itut
->second
;
1214 std::map
<TNode
, TNodeTrie
>::iterator itute
=
1215 itut
->second
.d_data
.find(eqc
);
1216 if( itute
!=itut
->second
.d_data
.end() ){
1217 return &itute
->second
;
1225 TNode
TermDb::getCongruentTerm( Node f
, Node n
) {
1226 if( options::ufHo() ){
1227 f
= getOperatorRepresentative( f
);
1229 computeUfTerms( f
);
1230 std::map
<Node
, TNodeTrie
>::iterator itut
= d_func_map_trie
.find(f
);
1231 if( itut
!=d_func_map_trie
.end() ){
1232 computeArgReps( n
);
1233 return itut
->second
.existsTerm( d_arg_reps
[n
] );
1235 return TNode::null();
1239 TNode
TermDb::getCongruentTerm( Node f
, std::vector
< TNode
>& args
) {
1240 if( options::ufHo() ){
1241 f
= getOperatorRepresentative( f
);
1243 computeUfTerms( f
);
1244 return d_func_map_trie
[f
].existsTerm( args
);
1247 Node
TermDb::getHoTypeMatchPredicate(TypeNode tn
)
1249 std::map
<TypeNode
, Node
>::iterator ithp
= d_ho_type_match_pred
.find(tn
);
1250 if (ithp
!= d_ho_type_match_pred
.end())
1252 return ithp
->second
;
1254 NodeManager
* nm
= NodeManager::currentNM();
1255 TypeNode ptn
= nm
->mkFunctionType(tn
, nm
->booleanType());
1256 Node k
= nm
->mkSkolem("U", ptn
, "predicate to force higher-order types");
1257 d_ho_type_match_pred
[tn
] = k
;
1261 }/* CVC4::theory::quantifiers namespace */
1262 }/* CVC4::theory namespace */
1263 }/* CVC4 namespace */