1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Dejan Jovanovic, Clark Barrett
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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 Base for theory interface.
14 ** Base for theory interface.
17 #include "theory/theory.h"
24 #include "base/cvc4_assert.h"
25 #include "smt/smt_statistics_registry.h"
26 #include "theory/substitutions.h"
27 #include "theory/quantifiers_engine.h"
35 /** Default value for the uninterpreted sorts is the UF theory */
36 TheoryId
Theory::s_uninterpretedSortOwner
= THEORY_UF
;
38 std::ostream
& operator<<(std::ostream
& os
, Theory::Effort level
){
40 case Theory::EFFORT_STANDARD
:
41 os
<< "EFFORT_STANDARD"; break;
42 case Theory::EFFORT_FULL
:
43 os
<< "EFFORT_FULL"; break;
44 case Theory::EFFORT_COMBINATION
:
45 os
<< "EFFORT_COMBINATION"; break;
46 case Theory::EFFORT_LAST_CALL
:
47 os
<< "EFFORT_LAST_CALL"; break;
52 }/* ostream& operator<<(ostream&, Theory::Effort) */
55 Theory::Theory(TheoryId id
, context::Context
* satContext
,
56 context::UserContext
* userContext
, OutputChannel
& out
,
57 Valuation valuation
, const LogicInfo
& logicInfo
,
58 std::string name
) throw()
60 , d_instanceName(name
)
61 , d_satContext(satContext
)
62 , d_userContext(userContext
)
63 , d_logicInfo(logicInfo
)
65 , d_factsHead(satContext
, 0)
66 , d_sharedTermsIndex(satContext
, 0)
70 , d_checkTime(getFullInstanceName() + "::checkTime")
71 , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
72 , d_sharedTerms(satContext
)
74 , d_valuation(valuation
)
75 , d_proofsEnabled(false)
77 smtStatisticsRegistry()->registerStat(&d_checkTime
);
78 smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime
);
82 smtStatisticsRegistry()->unregisterStat(&d_checkTime
);
83 smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime
);
86 TheoryId
Theory::theoryOf(TheoryOfMode mode
, TNode node
) {
87 TheoryId tid
= THEORY_BUILTIN
;
89 case THEORY_OF_TYPE_BASED
:
90 // Constants, variables, 0-ary constructors
91 if (node
.isVar() || node
.isConst()) {
92 tid
= Theory::theoryOf(node
.getType());
93 } else if (node
.getKind() == kind::EQUAL
) {
94 // Equality is owned by the theory that owns the domain
95 tid
= Theory::theoryOf(node
[0].getType());
97 // Regular nodes are owned by the kind
98 tid
= kindToTheoryId(node
.getKind());
101 case THEORY_OF_TERM_BASED
:
104 if (Theory::theoryOf(node
.getType()) != theory::THEORY_BOOL
) {
105 // We treat the variables as uninterpreted
106 tid
= s_uninterpretedSortOwner
;
108 // Except for the Boolean ones, which we just ignore anyhow
109 tid
= theory::THEORY_BOOL
;
111 } else if (node
.isConst()) {
112 // Constants go to the theory of the type
113 tid
= Theory::theoryOf(node
.getType());
114 } else if (node
.getKind() == kind::EQUAL
) { // Equality
115 // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
116 if (node
[0].getKind() == kind::ITE
) {
117 tid
= Theory::theoryOf(node
[0].getType());
118 } else if (node
[1].getKind() == kind::ITE
) {
119 tid
= Theory::theoryOf(node
[1].getType());
123 TypeNode ltype
= l
.getType();
124 TypeNode rtype
= r
.getType();
125 if( ltype
!= rtype
){
126 tid
= Theory::theoryOf(l
.getType());
128 // If both sides belong to the same theory the choice is easy
129 TheoryId T1
= Theory::theoryOf(l
);
130 TheoryId T2
= Theory::theoryOf(r
);
134 TheoryId T3
= Theory::theoryOf(ltype
);
136 // * x*y = f(z) -> UF
138 // * f(x) = read(a, y) -> either UF or ARRAY
139 // at least one of the theories has to be parametric, i.e. theory of the type is different
140 // from the theory of the term
143 } else if (T2
== T3
) {
146 // If both are parametric, we take the smaller one (arbitrary)
147 tid
= T1
< T2
? T1
: T2
;
153 // Regular nodes are owned by the kind
154 tid
= kindToTheoryId(node
.getKind());
160 Trace("theory::internal") << "theoryOf(" << mode
<< ", " << node
<< ") -> " << tid
<< std::endl
;
164 void Theory::addSharedTermInternal(TNode n
) {
165 Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n
<< ")" << endl
;
166 Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n
<< ")" << endl
;
167 d_sharedTerms
.push_back(n
);
171 void Theory::computeCareGraph() {
172 Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl
;
173 for (unsigned i
= 0; i
< d_sharedTerms
.size(); ++ i
) {
174 TNode a
= d_sharedTerms
[i
];
175 TypeNode aType
= a
.getType();
176 for (unsigned j
= i
+ 1; j
< d_sharedTerms
.size(); ++ j
) {
177 TNode b
= d_sharedTerms
[j
];
178 if (b
.getType() != aType
) {
179 // We don't care about the terms of different types
182 switch (d_valuation
.getEqualityStatus(a
, b
)) {
183 case EQUALITY_TRUE_AND_PROPAGATED
:
184 case EQUALITY_FALSE_AND_PROPAGATED
:
185 // If we know about it, we should have propagated it, so we can skip
196 void Theory::printFacts(std::ostream
& os
) const {
197 unsigned i
, n
= d_facts
.size();
198 for(i
= 0; i
< n
; i
++){
199 const Assertion
& a_i
= d_facts
[i
];
200 Node assertion
= a_i
;
201 os
<< d_id
<< '[' << i
<< ']' << " " << assertion
<< endl
;
205 void Theory::debugPrintFacts() const{
206 DebugChannel
.getStream() << "Theory::debugPrintFacts()" << endl
;
207 printFacts(DebugChannel
.getStream());
210 std::hash_set
<TNode
, TNodeHashFunction
> Theory::currentlySharedTerms() const{
211 std::hash_set
<TNode
, TNodeHashFunction
> currentlyShared
;
212 for (shared_terms_iterator i
= shared_terms_begin(),
213 i_end
= shared_terms_end(); i
!= i_end
; ++i
) {
214 currentlyShared
.insert (*i
);
216 return currentlyShared
;
220 void Theory::collectTerms(TNode n
, set
<Node
>& termSet
) const
222 if (termSet
.find(n
) != termSet
.end()) {
225 Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n
<< endl
;
227 if (n
.getKind() == kind::NOT
|| n
.getKind() == kind::EQUAL
|| !isLeaf(n
)) {
228 for(TNode::iterator child_it
= n
.begin(); child_it
!= n
.end(); ++child_it
) {
229 collectTerms(*child_it
, termSet
);
235 void Theory::computeRelevantTerms(set
<Node
>& termSet
, bool includeShared
) const
237 // Collect all terms appearing in assertions
238 context::CDList
<Assertion
>::const_iterator assert_it
= facts_begin(), assert_it_end
= facts_end();
239 for (; assert_it
!= assert_it_end
; ++assert_it
) {
240 collectTerms(*assert_it
, termSet
);
243 if (!includeShared
) return;
245 // Add terms that are shared terms
246 context::CDList
<TNode
>::const_iterator shared_it
= shared_terms_begin(), shared_it_end
= shared_terms_end();
247 for (; shared_it
!= shared_it_end
; ++shared_it
) {
248 collectTerms(*shared_it
, termSet
);
253 Theory::PPAssertStatus
Theory::ppAssert(TNode in
,
254 SubstitutionMap
& outSubstitutions
)
256 if (in
.getKind() == kind::EQUAL
) {
257 // (and (= x t) phi) can be replaced by phi[x/t] if
258 // 1) x is a variable
259 // 2) x is not in the term t
260 // 3) x : T and t : S, then S <: T
261 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0]) &&
262 (in
[1].getType()).isSubtypeOf(in
[0].getType()) ){
263 outSubstitutions
.addSubstitution(in
[0], in
[1]);
264 return PP_ASSERT_STATUS_SOLVED
;
266 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1]) &&
267 (in
[0].getType()).isSubtypeOf(in
[1].getType())){
268 outSubstitutions
.addSubstitution(in
[1], in
[0]);
269 return PP_ASSERT_STATUS_SOLVED
;
271 if (in
[0].isConst() && in
[1].isConst()) {
272 if (in
[0] != in
[1]) {
273 return PP_ASSERT_STATUS_CONFLICT
;
278 return PP_ASSERT_STATUS_UNSOLVED
;
281 std::pair
<bool, Node
> Theory::entailmentCheck(
283 const EntailmentCheckParameters
* params
,
284 EntailmentCheckSideEffects
* out
) {
285 return make_pair(false, Node::null());
288 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid
)
292 std::string
Theory::getFullInstanceName() const {
293 std::stringstream ss
;
294 ss
<< "theory<" << d_id
<< ">" << d_instanceName
;
298 EntailmentCheckParameters::~EntailmentCheckParameters(){}
300 TheoryId
EntailmentCheckParameters::getTheoryId() const {
304 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid
)
308 TheoryId
EntailmentCheckSideEffects::getTheoryId() const {
312 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
316 ExtTheory::ExtTheory( Theory
* p
) : d_parent( p
),
317 d_ext_func_terms( p
->getSatContext() ), d_ci_inactive( p
->getUserContext() ),
318 d_lemmas( p
->getUserContext() ), d_pp_lemmas( p
->getUserContext() ), d_has_extf( p
->getSatContext() ){
319 d_true
= NodeManager::currentNM()->mkConst( true );
322 //gets all leaf terms in n
323 void ExtTheory::collectVars( Node n
, std::vector
< Node
>& vars
, std::map
< Node
, bool >& visited
) {
325 if( visited
.find( n
)==visited
.end() ){
327 //treat terms not belonging to this theory as leaf
328 if( n
.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){
329 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
330 collectVars( n
[i
], vars
, visited
);
340 void ExtTheory::getSubstitutedTerms( int effort
, std::vector
< Node
>& terms
, std::vector
< Node
>& sterms
, std::vector
< std::vector
< Node
> >& exp
) {
341 Trace("extt-debug") << "Currently " << d_ext_func_terms
.size() << " extended functions." << std::endl
;
342 Trace("extt-debug") << "..." << terms
.size() << " to reduce." << std::endl
;
343 if( !terms
.empty() ){
344 //all variables we need to find a substitution for
345 std::vector
< Node
> vars
;
346 std::vector
< Node
> sub
;
347 std::map
< Node
, std::vector
< Node
> > expc
;
348 for( unsigned i
=0; i
<terms
.size(); i
++ ){
349 //do substitution, rewrite
351 std::map
< Node
, ExtfInfo
>::iterator iti
= d_extf_info
.find( n
);
352 Assert( iti
!=d_extf_info
.end() );
353 for( unsigned i
=0; i
<iti
->second
.d_vars
.size(); i
++ ){
354 if( std::find( vars
.begin(), vars
.end(), iti
->second
.d_vars
[i
] )==vars
.end() ){
355 vars
.push_back( iti
->second
.d_vars
[i
] );
359 //get the current substitution for all variables
360 if( d_parent
->getCurrentSubstitution( effort
, vars
, sub
, expc
) ){
361 Assert( vars
.size()==sub
.size() );
362 for( unsigned i
=0; i
<terms
.size(); i
++ ){
365 Node ns
= n
.substitute( vars
.begin(), vars
.end(), sub
.begin(), sub
.end() );
366 std::vector
< Node
> expn
;
368 //build explanation: explanation vars = sub for each vars in FV( n )
369 std::map
< Node
, ExtfInfo
>::iterator iti
= d_extf_info
.find( n
);
370 Assert( iti
!=d_extf_info
.end() );
371 for( unsigned j
=0; j
<iti
->second
.d_vars
.size(); j
++ ){
372 Node v
= iti
->second
.d_vars
[j
];
373 std::map
< Node
, std::vector
< Node
> >::iterator itx
= expc
.find( v
);
374 if( itx
!=expc
.end() ){
375 for( unsigned k
=0; k
<itx
->second
.size(); k
++ ){
376 if( std::find( expn
.begin(), expn
.end(), itx
->second
[k
] )==expn
.end() ){
377 expn
.push_back( itx
->second
[k
] );
383 Trace("extt-debug") << " have " << n
<< " == " << ns
<< ", exp size=" << expn
.size() << "." << std::endl
;
385 sterms
.push_back( ns
);
386 exp
.push_back( expn
);
389 for( unsigned i
=0; i
<terms
.size(); i
++ ){
390 sterms
.push_back( terms
[i
] );
396 bool ExtTheory::doInferencesInternal( int effort
, std::vector
< Node
>& terms
, std::vector
< Node
>& nred
, bool batch
, bool isRed
) {
398 bool addedLemma
= false;
400 for( unsigned i
=0; i
<terms
.size(); i
++ ){
403 //TODO: reduction with substitution?
404 int ret
= d_parent
->getReduction( effort
, n
, nr
);
408 if( !nr
.isNull() && n
!=nr
){
409 Node lem
= NodeManager::currentNM()->mkNode( n
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, n
, nr
);
410 if( sendLemma( lem
, true ) ){
411 Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem
<< std::endl
;
415 markReduced( terms
[i
], ret
<0 );
419 std::vector
< Node
> sterms
;
420 std::vector
< std::vector
< Node
> > exp
;
421 getSubstitutedTerms( effort
, terms
, sterms
, exp
);
422 for( unsigned i
=0; i
<terms
.size(); i
++ ){
423 bool processed
= false;
424 if( sterms
[i
]!=terms
[i
] ){
425 Node sr
= Rewriter::rewrite( sterms
[i
] );
428 markReduced( terms
[i
] );
429 Node eq
= terms
[i
].eqNode( sr
);
430 Node expn
= exp
[i
].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND
, exp
[i
] ) : ( exp
[i
].size()==1 ? exp
[i
][0] : d_true
);
431 Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
<< " by " << expn
<< std::endl
;
432 Node lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, expn
, eq
);
433 Trace("extt-debug") << "...send lemma " << lem
<< std::endl
;
434 if( sendLemma( lem
) ){
435 Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem
<< std::endl
;
441 nred
.push_back( terms
[i
] );
447 std::vector
< Node
> nnred
;
449 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
450 if( (*it
).second
&& !isContextIndependentInactive( (*it
).first
) ){
451 std::vector
< Node
> nterms
;
452 nterms
.push_back( (*it
).first
);
453 if( doInferencesInternal( effort
, nterms
, nnred
, true, isRed
) ){
459 for( unsigned i
=0; i
<terms
.size(); i
++ ){
460 std::vector
< Node
> nterms
;
461 nterms
.push_back( terms
[i
] );
462 if( doInferencesInternal( effort
, nterms
, nnred
, true, isRed
) ){
471 bool ExtTheory::sendLemma( Node lem
, bool preprocess
) {
473 if( d_pp_lemmas
.find( lem
)==d_pp_lemmas
.end() ){
474 d_pp_lemmas
.insert( lem
);
475 d_parent
->getOutputChannel().lemma( lem
, false, true );
479 if( d_lemmas
.find( lem
)==d_lemmas
.end() ){
480 d_lemmas
.insert( lem
);
481 d_parent
->getOutputChannel().lemma( lem
);
488 bool ExtTheory::doInferences( int effort
, std::vector
< Node
>& terms
, std::vector
< Node
>& nred
, bool batch
) {
489 if( !terms
.empty() ){
490 return doInferencesInternal( effort
, terms
, nred
, batch
, false );
496 bool ExtTheory::doInferences( int effort
, std::vector
< Node
>& nred
, bool batch
) {
497 std::vector
< Node
> terms
;
499 return doInferencesInternal( effort
, terms
, nred
, batch
, false );
502 bool ExtTheory::doReductions( int effort
, std::vector
< Node
>& terms
, std::vector
< Node
>& nred
, bool batch
) {
503 if( !terms
.empty() ){
504 return doInferencesInternal( effort
, terms
, nred
, batch
, true );
510 bool ExtTheory::doReductions( int effort
, std::vector
< Node
>& nred
, bool batch
) {
511 std::vector
< Node
> terms
;
513 return doInferencesInternal( effort
, terms
, nred
, batch
, true );
518 void ExtTheory::registerTerm( Node n
) {
519 if( d_extf_kind
.find( n
.getKind() )!=d_extf_kind
.end() ){
520 if( d_ext_func_terms
.find( n
)==d_ext_func_terms
.end() ){
521 Trace("extt-debug") << "Found extended function : " << n
<< " in " << d_parent
->getId() << std::endl
;
522 d_ext_func_terms
[n
] = true;
524 std::map
< Node
, bool > visited
;
525 collectVars( n
, d_extf_info
[n
].d_vars
, visited
);
530 void ExtTheory::registerTermRec( Node n
) {
531 std::map
< Node
, bool > visited
;
532 registerTermRec( n
, visited
);
535 void ExtTheory::registerTermRec( Node n
, std::map
< Node
, bool >& visited
) {
536 if( visited
.find( n
)==visited
.end() ){
539 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
540 registerTermRec( n
[i
], visited
);
546 void ExtTheory::markReduced( Node n
, bool contextDepend
) {
547 d_ext_func_terms
[n
] = false;
548 if( !contextDepend
){
549 d_ci_inactive
.insert( n
);
553 if( d_has_extf
.get()==n
){
554 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
555 //if not already reduced
556 if( (*it
).second
&& !isContextIndependentInactive( (*it
).first
) ){
557 d_has_extf
= (*it
).first
;
565 void ExtTheory::markCongruent( Node a
, Node b
) {
566 NodeBoolMap::const_iterator it
= d_ext_func_terms
.find( b
);
567 if( it
!=d_ext_func_terms
.end() ){
568 if( d_ext_func_terms
.find( a
)==d_ext_func_terms
.end() ){
569 d_ext_func_terms
[a
] = (*it
).second
;
571 d_ext_func_terms
[a
] = d_ext_func_terms
[a
] && (*it
).second
;
573 d_ext_func_terms
[b
] = false;
577 bool ExtTheory::isContextIndependentInactive( Node n
) {
578 return d_ci_inactive
.find( n
)!=d_ci_inactive
.end();
581 bool ExtTheory::hasActiveTerm() {
582 return !d_has_extf
.get().isNull();
586 bool ExtTheory::isActive( Node n
) {
587 NodeBoolMap::const_iterator it
= d_ext_func_terms
.find( n
);
588 if( it
!=d_ext_func_terms
.end() ){
589 return (*it
).second
&& !isContextIndependentInactive( n
);
595 void ExtTheory::getActive( std::vector
< Node
>& active
) {
596 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
597 //if not already reduced
598 if( (*it
).second
&& !isContextIndependentInactive( (*it
).first
) ){
599 active
.push_back( (*it
).first
);
604 void ExtTheory::getActive( std::vector
< Node
>& active
, Kind k
) {
605 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
606 //if not already reduced
607 if( (*it
).first
.getKind()==k
&& (*it
).second
&& !isContextIndependentInactive( (*it
).first
) ){
608 active
.push_back( (*it
).first
);
613 }/* CVC4::theory namespace */
614 }/* CVC4 namespace */