summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp114
1 files changed, 68 insertions, 46 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0388ae7d4..4d7e93ef2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -275,26 +275,65 @@ void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
}
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
- std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant );
- if( options::efficientEMatching() ){
- uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
- d_ith->newTerms(added);
- }
+ std::set< Node > added;
+ getTermDatabase()->addTerm( n, added, withinQuant );
+ if( options::efficientEMatching() ){
+ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
+ d_ith->newTerms(added);
+ }
#ifdef COMPUTE_RELEVANCE
- //added contains also the Node that just have been asserted in this branch
- for( std::set< Node >::iterator i=added.begin(), end=added.end();
- i!=end; i++ ){
- if( !withinQuant ){
- setRelevance( i->getOperator(), 0 );
- }
+ //added contains also the Node that just have been asserted in this branch
+ for( std::set< Node >::iterator i=added.begin(), end=added.end();
+ i!=end; i++ ){
+ if( !withinQuant ){
+ setRelevance( i->getOperator(), 0 );
+ }
}
#endif
}
+void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
+ for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
+ Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
+ if( !n.isNull() ){
+ vars.push_back( f[0][i] );
+ terms.push_back( n );
+ }
+ }
+}
+
+Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+ Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ //process partial instantiation if necessary
+ if( d_term_db->d_vars[f].size()!=vars.size() ){
+ std::vector< Node > uninst_vars;
+ //doing a partial instantiation, must add quantifier for all uninstantiated variables
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
+ uninst_vars.push_back( f[0][i] );
+ }
+ }
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
+ body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
+ Trace("partial-inst") << "Partial instantiation : " << d_rewritten_quant[f] << std::endl;
+ Trace("partial-inst") << " : " << body << std::endl;
+ }
+ return body;
+}
+
+Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
+ std::vector< Node > vars;
+ std::vector< Node > terms;
+ computeTermVector( f, m, vars, terms );
+ return getInstantiation( f, vars, terms );
+}
+
+bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+ return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, NULL, modInst );
+}
+
bool QuantifiersEngine::addLemma( Node lem ){
- //AJR: the following check is necessary until FULL_CHECK is guarenteed after d_out->lemma(...)
Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
lem = Rewriter::rewrite(lem);
if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
@@ -309,22 +348,16 @@ bool QuantifiersEngine::addLemma( Node lem ){
}
}
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms )
-{
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
Assert( f.getKind()==FORALL );
Assert( !f.hasAttribute(InstConstantAttribute()) );
Assert( vars.size()==terms.size() );
- Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- Node lem;
- if( d_term_db->d_vars[f].size()==vars.size() ){
- NodeBuilder<> nb(kind::OR);
- nb << d_rewritten_quant[f].notNode() << body;
- lem = nb;
- }else{
- //doing a partial instantiation, must add quantifier for all uninstantiated variables
- Notice() << "Partial instantiation not implemented yet." << std::endl;
- Unimplemented();
- }
+ Node body = getInstantiation( f, vars, terms );
+ //make the lemma
+ NodeBuilder<> nb(kind::OR);
+ nb << d_rewritten_quant[f].notNode() << body;
+ Node lem = nb;
+ //check for duplication
if( addLemma( lem ) ){
Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
uint64_t maxInstLevel = 0;
@@ -360,11 +393,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
}
}
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool makeComplete ){
+bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m ){
//make sure there are values for each variable we are instantiating
- if( makeComplete ){
- m.makeComplete( f, this );
- }
+ m.makeComplete( f, this );
//make it representative, this is helpful for recognizing duplication
m.makeRepresentative( this );
Trace("inst-add") << "Add instantiation: " << m << std::endl;
@@ -375,23 +406,14 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool makeComplet
return false;
}
//compute the vector of terms for the instantiation
- std::vector< Node > match;
- m.computeTermVec( d_term_db->d_inst_constants[f], match );
- //add the instantiation
- bool addedInst = false;
- if( match.size()==d_term_db->d_vars[f].size() ){
- addedInst = addInstantiation( f, d_term_db->d_vars[f], match );
- }else{
- //must compute the subset of variables we are instantiating
- std::vector< Node > vars;
- for( size_t i=0; i<d_term_db->d_vars[f].size(); i++ ){
- Node val = m.get( getTermDatabase()->getInstantiationConstant( f, i ) );
- if( !val.isNull() ){
- vars.push_back( d_term_db->d_vars[f][i] );
- }
- }
- addedInst = addInstantiation( f, vars, match );
+ std::vector< Node > terms;
+ for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
+ Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
+ Assert( !n.isNull() );
+ terms.push_back( n );
}
+ //add the instantiation
+ bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
//report the result
if( addedInst ){
Trace("inst-add") << " -> Success." << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback