1 /********************* */
2 /*! \file term_database.cpp
4 ** Original author: Andrew Reynolds
5 ** Major contributors: Francois Bobot
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Implementation of term databse class
15 #include "theory/quantifiers/term_database.h"
16 #include "theory/quantifiers_engine.h"
17 #include "theory/quantifiers/trigger.h"
18 #include "theory/theory_engine.h"
19 #include "theory/quantifiers/first_order_model.h"
20 #include "theory/quantifiers/options.h"
21 #include "theory/quantifiers/theory_quantifiers.h"
25 using namespace CVC4::kind
;
26 using namespace CVC4::context
;
27 using namespace CVC4::theory
;
28 using namespace CVC4::theory::quantifiers
;
30 using namespace CVC4::theory::inst
;
32 bool TermArgTrie::addTerm2( QuantifiersEngine
* qe
, Node n
, int argIndex
){
33 if( argIndex
<(int)n
.getNumChildren() ){
34 Node r
= qe
->getEqualityQuery()->getRepresentative( n
[ argIndex
] );
35 std::map
< Node
, TermArgTrie
>::iterator it
= d_data
.find( r
);
36 if( it
==d_data
.end() ){
37 d_data
[r
].addTerm2( qe
, n
, argIndex
+1 );
40 return it
->second
.addTerm2( qe
, n
, argIndex
+1 );
43 //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
44 d_data
[n
].d_data
.clear();
49 TermDb::TermDb( context::Context
* c
, context::UserContext
* u
, QuantifiersEngine
* qe
) : d_quantEngine( qe
), d_op_ccount( u
) {
54 unsigned TermDb::getNumGroundTerms( Node f
) {
55 std::map
< Node
, std::vector
< Node
> >::iterator it
= d_op_map
.find( f
);
56 if( it
!=d_op_map
.end() ){
57 return it
->second
.size();
61 //return d_op_ccount[f];
64 Node
TermDb::getOperator( Node n
) {
65 //return n.getOperator();
67 if( n
.getKind()==SELECT
|| n
.getKind()==STORE
){
68 //since it is parametric, use a particular one as op
69 TypeNode tn1
= n
[0].getType();
70 TypeNode tn2
= n
[1].getType();
71 Node op
= n
.getOperator();
72 std::map
< Node
, std::map
< TypeNode
, std::map
< TypeNode
, Node
> > >::iterator ito
= d_par_op_map
.find( op
);
73 if( ito
!=d_par_op_map
.end() ){
74 std::map
< TypeNode
, std::map
< TypeNode
, Node
> >::iterator it
= ito
->second
.find( tn1
);
75 if( it
!=ito
->second
.end() ){
76 std::map
< TypeNode
, Node
>::iterator it2
= it
->second
.find( tn2
);
77 if( it2
!=it
->second
.end() ){
82 d_par_op_map
[op
][tn1
][tn2
] = n
;
84 }else if( n
.getKind()==APPLY_UF
){
85 return n
.getOperator();
91 void TermDb::addTerm( Node n
, std::set
< Node
>& added
, bool withinQuant
){
92 //don't add terms in quantifier bodies
93 if( withinQuant
&& !options::registerQuantBodyTerms() ){
96 if( d_processed
.find( n
)==d_processed
.end() ){
97 d_processed
.insert(n
);
98 d_type_map
[ n
.getType() ].push_back( n
);
99 //if this is an atomic trigger, consider adding it
101 if( inst::Trigger::isAtomicTrigger( n
) ){
102 if( !TermDb::hasInstConstAttr(n
) ){
103 Trace("term-db") << "register term in db " << n
<< std::endl
;
104 //std::cout << "register trigger term " << n << std::endl;
105 Node op
= getOperator( n
);
107 int occ = d_op_ccount[op];
108 if( occ<(int)d_op_map[op].size() ){
109 d_op_map[op][occ] = n;
111 d_op_map[op].push_back( n );
113 d_op_ccount[op].set( occ + 1 );
115 d_op_map
[op
].push_back( n
);
118 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
119 addTerm( n
[i
], added
, withinQuant
);
120 if( options::eagerInstQuant() ){
121 if( !n
.hasAttribute(InstLevelAttribute()) && n
.getAttribute(InstLevelAttribute())==0 ){
123 for( size_t i
=0; i
<d_op_triggers
[op
].size(); i
++ ){
124 addedLemmas
+= d_op_triggers
[op
][i
]->addTerm( n
);
126 //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
127 d_quantEngine
->flushLemmas( &d_quantEngine
->getOutputChannel() );
133 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
134 addTerm( n
[i
], added
, withinQuant
);
140 void TermDb::reset( Theory::Effort effort
){
141 int nonCongruentCount
= 0;
142 int congruentCount
= 0;
143 int alreadyCongruentCount
= 0;
144 //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
145 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= d_op_map
.begin(); it
!= d_op_map
.end(); ++it
){
146 d_op_nonred_count
[ it
->first
] = 0;
147 if( !it
->second
.empty() ){
148 if( it
->second
[0].getType().isBoolean() ){
149 d_pred_map_trie
[ 0 ][ it
->first
].d_data
.clear();
150 d_pred_map_trie
[ 1 ][ it
->first
].d_data
.clear();
152 d_func_map_trie
[ it
->first
].d_data
.clear();
153 for( int i
=0; i
<(int)it
->second
.size(); i
++ ){
154 Node n
= it
->second
[i
];
155 computeModelBasisArgAttribute( n
);
156 if( !n
.getAttribute(NoMatchAttribute()) ){
157 if( !d_func_map_trie
[ it
->first
].addTerm( d_quantEngine
, n
) ){
158 NoMatchAttribute nma
;
159 n
.setAttribute(nma
,true);
160 Debug("term-db-cong") << n
<< " is redundant." << std::endl
;
164 d_op_nonred_count
[ it
->first
]++;
168 alreadyCongruentCount
++;
174 for( int i
=0; i
<2; i
++ ){
175 Node n
= NodeManager::currentNM()->mkConst( i
==1 );
176 if( d_quantEngine
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
177 eq::EqClassIterator
eqc( d_quantEngine
->getEqualityQuery()->getEngine()->getRepresentative( n
),
178 d_quantEngine
->getEqualityQuery()->getEngine() );
179 while( !eqc
.isFinished() ){
181 computeModelBasisArgAttribute( en
);
182 if( en
.getKind()==APPLY_UF
&& !TermDb::hasInstConstAttr(en
) ){
183 if( !en
.getAttribute(NoMatchAttribute()) ){
184 Node op
= getOperator( en
);
185 if( !d_pred_map_trie
[i
][op
].addTerm( d_quantEngine
, en
) ){
186 NoMatchAttribute nma
;
187 en
.setAttribute(nma
,true);
188 Debug("term-db-cong") << en
<< " is redundant." << std::endl
;
192 d_op_nonred_count
[ op
]++;
195 alreadyCongruentCount
++;
202 Debug("term-db-cong") << "TermDb: Reset" << std::endl
;
203 Debug("term-db-cong") << "Congruent/Non-Congruent = ";
204 Debug("term-db-cong") << congruentCount
<< "(" << alreadyCongruentCount
<< ") / " << nonCongruentCount
<< std::endl
;
207 Node
TermDb::getModelBasisTerm( TypeNode tn
, int i
){
208 if( d_model_basis_term
.find( tn
)==d_model_basis_term
.end() ){
210 if( tn
.isInteger() || tn
.isReal() ){
211 mbt
= NodeManager::currentNM()->mkConst( Rational( 0 ) );
212 }else if( !tn
.isSort() ){
213 mbt
= tn
.mkGroundTerm();
215 if( options::fmfFreshDistConst() || d_type_map
[ tn
].empty() ){
216 std::stringstream ss
;
217 ss
<< Expr::setlanguage(options::outputLanguage());
219 mbt
= NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "is a model basis term" );
220 Trace("mkVar") << "ModelBasis:: Make variable " << mbt
<< " : " << tn
<< std::endl
;
222 mbt
= d_type_map
[ tn
][ 0 ];
225 ModelBasisAttribute mba
;
226 mbt
.setAttribute(mba
,true);
227 d_model_basis_term
[tn
] = mbt
;
228 Trace("model-basis-term") << "Choose " << mbt
<< " as model basis term for " << tn
<< std::endl
;
230 return d_model_basis_term
[tn
];
233 Node
TermDb::getModelBasisOpTerm( Node op
){
234 if( d_model_basis_op_term
.find( op
)==d_model_basis_op_term
.end() ){
235 TypeNode t
= op
.getType();
236 std::vector
< Node
> children
;
237 children
.push_back( op
);
238 for( int i
=0; i
<(int)(t
.getNumChildren()-1); i
++ ){
239 children
.push_back( getModelBasisTerm( t
[i
] ) );
241 if( children
.size()==1 ){
242 d_model_basis_op_term
[op
] = op
;
244 d_model_basis_op_term
[op
] = NodeManager::currentNM()->mkNode( APPLY_UF
, children
);
247 return d_model_basis_op_term
[op
];
250 Node
TermDb::getModelBasis( Node f
, Node n
){
252 if( d_model_basis_terms
.find( f
)==d_model_basis_terms
.end() ){
253 for( int j
=0; j
<(int)f
[0].getNumChildren(); j
++ ){
254 d_model_basis_terms
[f
].push_back( getModelBasisTerm( f
[0][j
].getType() ) );
257 Node gn
= n
.substitute( d_inst_constants
[f
].begin(), d_inst_constants
[f
].end(),
258 d_model_basis_terms
[f
].begin(), d_model_basis_terms
[f
].end() );
262 Node
TermDb::getModelBasisBody( Node f
){
263 if( d_model_basis_body
.find( f
)==d_model_basis_body
.end() ){
264 Node n
= getInstConstantBody( f
);
265 d_model_basis_body
[f
] = getModelBasis( f
, n
);
267 return d_model_basis_body
[f
];
270 void TermDb::computeModelBasisArgAttribute( Node n
){
271 if( !n
.hasAttribute(ModelBasisArgAttribute()) ){
272 //ensure that the model basis terms have been defined
273 if( n
.getKind()==APPLY_UF
){
274 getModelBasisOpTerm( n
.getOperator() );
277 //determine if it has model basis attribute
278 for( int j
=0; j
<(int)n
.getNumChildren(); j
++ ){
279 if( n
[j
].getAttribute(ModelBasisAttribute()) ){
283 ModelBasisArgAttribute mbaa
;
284 n
.setAttribute( mbaa
, val
);
288 void TermDb::makeInstantiationConstantsFor( Node f
){
289 if( d_inst_constants
.find( f
)==d_inst_constants
.end() ){
290 Debug("quantifiers-engine") << "Instantiation constants for " << f
<< " : " << std::endl
;
291 for( int i
=0; i
<(int)f
[0].getNumChildren(); i
++ ){
292 d_vars
[f
].push_back( f
[0][i
] );
293 //make instantiation constants
294 Node ic
= NodeManager::currentNM()->mkInstConstant( f
[0][i
].getType() );
295 d_inst_constants_map
[ic
] = f
;
296 d_inst_constants
[ f
].push_back( ic
);
297 Debug("quantifiers-engine") << " " << ic
<< std::endl
;
298 //set the var number attribute
299 InstVarNumAttribute ivna
;
300 ic
.setAttribute(ivna
,i
);
301 InstConstantAttribute ica
;
302 ic
.setAttribute(ica
,f
);
303 //also set the no-match attribute
304 NoMatchAttribute nma
;
305 ic
.setAttribute(nma
,true);
311 Node
TermDb::getInstConstAttr( Node n
) {
312 if (!n
.hasAttribute(InstConstantAttribute()) ){
314 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
315 f
= getInstConstAttr(n
[i
]);
320 InstConstantAttribute ica
;
321 n
.setAttribute(ica
,f
);
323 //also set the no-match attribute
324 NoMatchAttribute nma
;
325 n
.setAttribute(nma
,true);
328 return n
.getAttribute(InstConstantAttribute());
331 bool TermDb::hasInstConstAttr( Node n
) {
332 return !getInstConstAttr(n
).isNull();
335 void TermDb::getBoundVars( Node n
, std::vector
< Node
>& bvs
) {
336 if (n
.getKind()==BOUND_VARIABLE
){
337 if ( std::find( bvs
.begin(), bvs
.end(), n
)==bvs
.end() ){
341 for( unsigned i
=0; i
<n
.getNumChildren(); i
++) {
342 getBoundVars(n
[i
], bvs
);
348 /** get the i^th instantiation constant of f */
349 Node
TermDb::getInstantiationConstant( Node f
, int i
) const {
350 std::map
< Node
, std::vector
< Node
> >::const_iterator it
= d_inst_constants
.find( f
);
351 if( it
!=d_inst_constants
.end() ){
352 return it
->second
[i
];
358 /** get number of instantiation constants for f */
359 int TermDb::getNumInstantiationConstants( Node f
) const {
360 std::map
< Node
, std::vector
< Node
> >::const_iterator it
= d_inst_constants
.find( f
);
361 if( it
!=d_inst_constants
.end() ){
362 return (int)it
->second
.size();
368 Node
TermDb::getInstConstantBody( Node f
){
369 std::map
< Node
, Node
>::iterator it
= d_inst_const_body
.find( f
);
370 if( it
==d_inst_const_body
.end() ){
371 makeInstantiationConstantsFor( f
);
372 Node n
= getInstConstantNode( f
[1], f
);
373 d_inst_const_body
[ f
] = n
;
380 Node
TermDb::getCounterexampleLiteral( Node f
){
381 if( d_ce_lit
.find( f
)==d_ce_lit
.end() ){
382 Node ceBody
= getInstConstantBody( f
);
383 //check if any variable are of bad types, and fail if so
384 for( size_t i
=0; i
<d_inst_constants
[f
].size(); i
++ ){
385 if( d_inst_constants
[f
][i
].getType().isBoolean() ){
386 d_ce_lit
[ f
] = Node::null();
390 //otherwise, ensure literal
391 Node ceLit
= d_quantEngine
->getValuation().ensureLiteral( ceBody
.notNode() );
392 d_ce_lit
[ f
] = ceLit
;
394 return d_ce_lit
[ f
];
397 Node
TermDb::getInstConstantNode( Node n
, Node f
){
398 return convertNodeToPattern(n
,f
,d_vars
[f
],d_inst_constants
[ f
]);
401 Node
TermDb::convertNodeToPattern( Node n
, Node f
, const std::vector
<Node
> & vars
,
402 const std::vector
<Node
> & inst_constants
){
403 Node n2
= n
.substitute( vars
.begin(), vars
.end(),
404 inst_constants
.begin(),
405 inst_constants
.end() );
411 Node
TermDb::getSkolemizedBody( Node f
){
412 Assert( f
.getKind()==FORALL
);
413 if( d_skolem_body
.find( f
)==d_skolem_body
.end() ){
414 std::vector
< Node
> vars
;
415 for( int i
=0; i
<(int)f
[0].getNumChildren(); i
++ ){
416 Node skv
= NodeManager::currentNM()->mkSkolem( "skv", f
[0][i
].getType(), "is a termdb-created skolemized body" );
417 d_skolem_constants
[ f
].push_back( skv
);
418 vars
.push_back( f
[0][i
] );
419 //carry information for sort inference
420 if( options::sortInference() ){
421 d_quantEngine
->getTheoryEngine()->getSortInference()->setSkolemVar( f
, f
[0][i
], skv
);
424 d_skolem_body
[ f
] = f
[ 1 ].substitute( vars
.begin(), vars
.end(),
425 d_skolem_constants
[ f
].begin(), d_skolem_constants
[ f
].end() );
427 return d_skolem_body
[ f
];
430 Node
TermDb::getFreeVariableForInstConstant( Node n
){
431 TypeNode tn
= n
.getType();
432 if( d_free_vars
.find( tn
)==d_free_vars
.end() ){
433 for( unsigned i
=0; i
<d_type_map
[ tn
].size(); i
++ ){
434 if( !quantifiers::TermDb::hasInstConstAttr(d_type_map
[ tn
][ i
]) ){
435 d_free_vars
[tn
] = d_type_map
[ tn
][ i
];
438 if( d_free_vars
.find( tn
)==d_free_vars
.end() ){
439 //if integer or real, make zero
440 if( tn
.isInteger() || tn
.isReal() ){
442 d_free_vars
[tn
] = NodeManager::currentNM()->mkConst( z
);
444 d_free_vars
[tn
] = NodeManager::currentNM()->mkSkolem( "freevar", tn
, "is a free variable created by termdb" );
445 Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars
[tn
] << " : " << tn
<< std::endl
;
449 return d_free_vars
[tn
];
452 const std::vector
<Node
> & TermDb::getParents(TNode n
, TNode f
, int arg
){
453 std::hash_map
< Node
, std::hash_map
< Node
, std::hash_map
< int, std::vector
< Node
> >,NodeHashFunction
>,NodeHashFunction
>::const_iterator
454 rn
= d_parents
.find( n
);
455 if( rn
!=d_parents
.end() ){
456 std::hash_map
< Node
, std::hash_map
< int, std::vector
< Node
> > , NodeHashFunction
> ::const_iterator
457 rf
= rn
->second
.find(f
);
458 if( rf
!= rn
->second
.end() ){
459 std::hash_map
< int, std::vector
< Node
> > ::const_iterator
460 ra
= rf
->second
.find(arg
);
461 if( ra
!= rf
->second
.end() ){
466 static std::vector
<Node
> empty
;
470 void TermDb::computeVarContains( Node n
) {
471 if( d_var_contains
.find( n
)==d_var_contains
.end() ){
472 d_var_contains
[n
].clear();
473 computeVarContains2( n
, n
);
477 void TermDb::computeVarContains2( Node n
, Node parent
){
478 if( n
.getKind()==INST_CONSTANT
){
479 if( std::find( d_var_contains
[parent
].begin(), d_var_contains
[parent
].end(), n
)==d_var_contains
[parent
].end() ){
480 d_var_contains
[parent
].push_back( n
);
483 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
484 computeVarContains2( n
[i
], parent
);
489 bool TermDb::isVariableSubsume( Node n1
, Node n2
){
493 //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
494 computeVarContains( n1
);
495 computeVarContains( n2
);
496 for( int i
=0; i
<(int)d_var_contains
[n2
].size(); i
++ ){
497 if( std::find( d_var_contains
[n1
].begin(), d_var_contains
[n1
].end(), d_var_contains
[n2
][i
] )==d_var_contains
[n1
].end() ){
498 //Notice() << "no" << std::endl;
502 //Notice() << "yes" << std::endl;
507 void TermDb::getVarContains( Node f
, std::vector
< Node
>& pats
, std::map
< Node
, std::vector
< Node
> >& varContains
){
508 for( int i
=0; i
<(int)pats
.size(); i
++ ){
509 computeVarContains( pats
[i
] );
510 varContains
[ pats
[i
] ].clear();
511 for( int j
=0; j
<(int)d_var_contains
[pats
[i
]].size(); j
++ ){
512 if( d_var_contains
[pats
[i
]][j
].getAttribute(InstConstantAttribute())==f
){
513 varContains
[ pats
[i
] ].push_back( d_var_contains
[pats
[i
]][j
] );
519 void TermDb::getVarContainsNode( Node f
, Node n
, std::vector
< Node
>& varContains
){
520 computeVarContains( n
);
521 for( int j
=0; j
<(int)d_var_contains
[n
].size(); j
++ ){
522 if( d_var_contains
[n
][j
].getAttribute(InstConstantAttribute())==f
){
523 varContains
.push_back( d_var_contains
[n
][j
] );
528 /** is n1 an instance of n2 or vice versa? */
529 int TermDb::isInstanceOf( Node n1
, Node n2
){
532 }else if( n1
.getKind()==n2
.getKind() ){
533 if( n1
.getKind()==APPLY_UF
){
534 if( n1
.getOperator()==n2
.getOperator() ){
536 for( int i
=0; i
<(int)n1
.getNumChildren(); i
++ ){
538 int cResult
= isInstanceOf( n1
[i
], n2
[i
] );
541 }else if( cResult
!=result
){
554 }else if( n2
.getKind()==INST_CONSTANT
){
555 computeVarContains( n1
);
556 //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
559 if( d_var_contains
[ n1
].size()==1 && d_var_contains
[ n1
][ 0 ]==n2
){
562 }else if( n1
.getKind()==INST_CONSTANT
){
563 computeVarContains( n2
);
564 //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
567 if( d_var_contains
[ n2
].size()==1 && d_var_contains
[ n2
][ 0 ]==n1
){
574 bool TermDb::isUnifiableInstanceOf( Node n1
, Node n2
, std::map
< Node
, Node
>& subs
){
577 }else if( n2
.getKind()==INST_CONSTANT
){
578 //if( !node_contains( n1, n2 ) ){
581 if( subs
.find( n2
)==subs
.end() ){
583 }else if( subs
[n2
]!=n1
){
587 }else if( n1
.getKind()==n2
.getKind() && n1
.getMetaKind()==kind::metakind::PARAMETERIZED
){
588 if( n1
.getOperator()!=n2
.getOperator() ){
591 for( int i
=0; i
<(int)n1
.getNumChildren(); i
++ ){
592 if( !isUnifiableInstanceOf( n1
[i
], n2
[i
], subs
) ){
602 void TermDb::filterInstances( std::vector
< Node
>& nodes
){
603 std::vector
< bool > active
;
604 active
.resize( nodes
.size(), true );
605 for( int i
=0; i
<(int)nodes
.size(); i
++ ){
606 for( int j
=i
+1; j
<(int)nodes
.size(); j
++ ){
607 if( active
[i
] && active
[j
] ){
608 int result
= isInstanceOf( nodes
[i
], nodes
[j
] );
610 Trace("filter-instances") << nodes
[j
] << " is an instance of " << nodes
[i
] << std::endl
;
612 }else if( result
==-1 ){
613 Trace("filter-instances") << nodes
[i
] << " is an instance of " << nodes
[j
] << std::endl
;
619 std::vector
< Node
> temp
;
620 for( int i
=0; i
<(int)nodes
.size(); i
++ ){
622 temp
.push_back( nodes
[i
] );
626 nodes
.insert( nodes
.begin(), temp
.begin(), temp
.end() );
629 void TermDb::registerTrigger( theory::inst::Trigger
* tr
, Node op
){
630 if( std::find( d_op_triggers
[op
].begin(), d_op_triggers
[op
].end(), tr
)==d_op_triggers
[op
].end() ){
631 d_op_triggers
[op
].push_back( tr
);
635 bool TermDb::isRewriteRule( Node q
) {
636 return !getRewriteRule( q
).isNull();
639 Node
TermDb::getRewriteRule( Node q
) {
640 if( q
.getKind()==FORALL
&& q
.getNumChildren()==3 && q
[2].getNumChildren()>0 && q
[2][0][0].getKind()==REWRITE_RULE
){