summaryrefslogtreecommitdiff
path: root/src/theory/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/inst_match.cpp')
-rw-r--r--src/theory/inst_match.cpp167
1 files changed, 85 insertions, 82 deletions
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp
index 32d6c958b..abcf5aa7f 100644
--- a/src/theory/inst_match.cpp
+++ b/src/theory/inst_match.cpp
@@ -20,6 +20,10 @@
#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_candidate_generator.h"
#include "theory/uf/equality_engine.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
using namespace std;
using namespace CVC4;
@@ -29,7 +33,8 @@ using namespace CVC4::theory;
bool CandidateGenerator::isLegalCandidate( Node n ){
- return !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) );
+ return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ) ||
+ ( Options::current()->finiteModelFind && n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 );
}
void CandidateGeneratorQueue::addCandidate( Node n ) {
@@ -115,9 +120,9 @@ void InstMatch::debugPrint( const char* c ){
}
void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
- for( int i=0; i<(int)qe->d_inst_constants[f].size(); i++ ){
- if( d_map.find( qe->d_inst_constants[f][i] )==d_map.end() ){
- d_map[ qe->d_inst_constants[f][i] ] = qe->getFreeVariableForInstConstant( qe->d_inst_constants[f][i] );
+ for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){
+ if( d_map.find( qe->getTermDatabase()->d_inst_constants[f][i] )==d_map.end() ){
+ d_map[ qe->getTermDatabase()->d_inst_constants[f][i] ] = qe->getTermDatabase()->getFreeVariableForInstConstant( qe->getTermDatabase()->d_inst_constants[f][i] );
}
}
}
@@ -127,7 +132,7 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){
if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
- d_map[ it->first ] = qe->getFreeVariableForInstConstant( it->first );
+ d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
}
}
}
@@ -137,7 +142,7 @@ void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
- d_map[ it->first ] = qe->getFreeVariableForInstConstant( it->first );
+ d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
}
}
}
@@ -154,7 +159,7 @@ void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >
if( it!=d_map.end() && !it->second.isNull() ){
match.push_back( it->second );
}else{
- match.push_back( qe->getFreeVariableForInstConstant( vars[i] ) );
+ match.push_back( qe->getTermDatabase()->getFreeVariableForInstConstant( vars[i] ) );
}
}
}
@@ -169,7 +174,7 @@ void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< No
void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m.d_map[ qe->getInstantiationConstant( f, i_index ) ];
+ Node n = m.d_map[ qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ];
d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
}
}
@@ -180,7 +185,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m
return true;
}else{
int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m.d_map[ qe->getInstantiationConstant( f, i_index ) ];
+ Node n = m.d_map[ qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ];
std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
if( it!=d_data.end() ){
if( it->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){
@@ -190,7 +195,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m
if( modEq ){
//check modulo equality if any other instantiation match exists
if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getRepresentative( n ),
+ eq::EqClassIterator eqc( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->getRepresentative( n ),
((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
while( !eqc.isFinished() ){
Node en = (*eqc);
@@ -344,7 +349,9 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe )
Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
<< m.d_map.size() << ")" << ", " << d_children.size() << std::endl;
Assert( !d_match_pattern.isNull() );
- if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
+ if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
+ return true;
+ }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
return getMatchArithmetic( t, m, qe );
}else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
return false;
@@ -421,7 +428,6 @@ bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, boo
t = d_cg->getNextCandidate();
//if t not null, try to fit it into match m
if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
- //Assert( t.getType()==d_match_pattern.getType() );
success = getMatch( t, m, qe );
}
}while( !success && !t.isNull() );
@@ -592,16 +598,16 @@ bool InstMatchGenerator::nonunifiable( TNode t0, const std::vector<Node> & vars)
return false;
}
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe, int instLimit, bool addSplits ){
+int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
//now, try to add instantiation for each match produced
int addedLemmas = 0;
InstMatch m;
while( getNextMatch( m, qe ) ){
//m.makeInternal( d_quantEngine->getEqualityQuery() );
m.add( baseMatch );
- if( qe->addInstantiation( f, m, addSplits ) ){
+ if( qe->addInstantiation( f, m ) ){
addedLemmas++;
- if( instLimit>0 && addedLemmas==instLimit ){
+ if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
return addedLemmas;
}
}
@@ -706,29 +712,62 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
}
}
-void InstMatchGeneratorMulti::collectInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq ){
+int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+ int addedLemmas = 0;
+ Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
+ for( int i=0; i<(int)d_children.size(); i++ ){
+ Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
+ std::vector< InstMatch > newMatches;
+ InstMatch m;
+ while( d_children[i]->getNextMatch( m, qe ) ){
+ m.makeRepresentative( qe );
+ newMatches.push_back( InstMatch( &m ) );
+ m.clear();
+ }
+ for( int j=0; j<(int)newMatches.size(); j++ ){
+ processNewMatch( qe, newMatches[j], i, addedLemmas );
+ }
+ }
+ return addedLemmas;
+}
+
+void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
+ //see if these produce new matches
+ d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
+ //possibly only do the following if we know that new matches will be produced?
+ //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
+ // we can safely skip the following lines, even when we have already produced this match.
+ Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
+ //process new instantiations
+ int childIndex = (fromChildIndex+1)%(int)d_children.size();
+ std::vector< IndexedTrie > unique_var_tries;
+ processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
+ unique_var_tries, 0, childIndex, fromChildIndex, true );
+}
+
+void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
+ std::vector< IndexedTrie >& unique_var_tries,
+ int trieIndex, int childIndex, int endChildIndex, bool modEq ){
if( childIndex==endChildIndex ){
//now, process unique variables
- collectInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
+ processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
}else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getInstantiationConstant( d_f, curr_index );
+ Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
if( m.d_map.find( curr_ic )==m.d_map.end() ){
//if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
// //unique variable(s), defer calculation
// unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
// int newChildIndex = (childIndex+1)%(int)d_children.size();
- // collectInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- // 0, newChildIndex, endChildIndex, modEq );
+ // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
+ // 0, newChildIndex, endChildIndex, modEq );
//}else{
//shared and non-set variable, add to InstMatch
for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
InstMatch mn( &m );
mn.d_map[ curr_ic ] = it->first;
- collectInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
+ processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
+ trieIndex+1, childIndex, endChildIndex, modEq );
}
//}
}else{
@@ -736,8 +775,8 @@ void InstMatchGeneratorMulti::collectInstantiations( QuantifiersEngine* qe, Inst
Node n = m.d_map[ curr_ic ];
std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
if( it!=tr->d_data.end() ){
- collectInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
+ processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
+ trieIndex+1, childIndex, endChildIndex, modEq );
}
if( modEq ){
//check modulo equality for other possible instantiations
@@ -749,8 +788,8 @@ void InstMatchGeneratorMulti::collectInstantiations( QuantifiersEngine* qe, Inst
if( en!=n ){
std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
if( itc!=tr->d_data.end() ){
- collectInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
+ processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
+ trieIndex+1, childIndex, endChildIndex, modEq );
}
}
++eqc;
@@ -760,14 +799,14 @@ void InstMatchGeneratorMulti::collectInstantiations( QuantifiersEngine* qe, Inst
}
}else{
int newChildIndex = (childIndex+1)%(int)d_children.size();
- collectInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- 0, newChildIndex, endChildIndex, modEq );
+ processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
+ 0, newChildIndex, endChildIndex, modEq );
}
}
-void InstMatchGeneratorMulti::collectInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr, int trieIndex ){
+void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
+ std::vector< IndexedTrie >& unique_var_tries,
+ int uvtIndex, InstMatchTrie* tr, int trieIndex ){
if( uvtIndex<(int)unique_var_tries.size() ){
int childIndex = unique_var_tries[uvtIndex].first.first;
if( !tr ){
@@ -776,58 +815,25 @@ void InstMatchGeneratorMulti::collectInstantiations2( QuantifiersEngine* qe, Ins
}
if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getInstantiationConstant( d_f, curr_index );
+ Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
//unique non-set variable, add to InstMatch
for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
InstMatch mn( &m );
mn.d_map[ curr_ic ] = it->first;
- collectInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
+ processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
}
}else{
- collectInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
+ processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
}
}else{
//m is an instantiation
- if( qe->addInstantiation( d_f, m, true ) ){
+ if( qe->addInstantiation( d_f, m ) ){
addedLemmas++;
Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
}
}
}
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe, int instLimit, bool addSplits ){
- int addedLemmas = 0;
- Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
- std::vector< InstMatch > newMatches;
- InstMatch m;
- while( d_children[i]->getNextMatch( m, qe ) ){
- m.makeRepresentative( qe );
- newMatches.push_back( InstMatch( &m ) );
- m.clear();
- }
- for( int j=0; j<(int)newMatches.size(); j++ ){
- processNewMatch( qe, newMatches[j], i, addedLemmas );
- }
- }
- return addedLemmas;
-}
-
-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
- //see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
- //possibly only do the following if we know that new matches will be produced?
- //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
- // we can safely skip the following lines, even when we have already produced this match.
- Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
- //collect new instantiations
- int childIndex = (fromChildIndex+1)%(int)d_children.size();
- std::vector< IndexedTrie > unique_var_tries;
- collectInstantiations( qe, m, addedLemmas,
- d_children_trie[childIndex].getTrie(), unique_var_tries, 0, childIndex, fromChildIndex, true );
-}
-
int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
Assert( Options::current()->eagerInstQuant );
int addedLemmas = 0;
@@ -843,47 +849,44 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
return addedLemmas;
}
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe, int instLimit, bool addSplits ){
+int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
InstMatch m;
m.add( baseMatch );
int addedLemmas = 0;
if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
for( int i=0; i<2; i++ ){
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]),
- instLimit, addSplits );
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
}
}else{
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]),
- instLimit, addSplits );
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
}
return addedLemmas;
}
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex,
- TermArgTrie* tat, int instLimit, bool addSplits ){
+void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
if( argIndex==(int)d_match_pattern.getNumChildren() ){
//m is an instantiation
- if( qe->addInstantiation( d_f, m, addSplits ) ){
+ if( qe->addInstantiation( d_f, m ) ){
addedLemmas++;
Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
}
}else{
if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
Node ic = d_match_pattern[argIndex];
- for( std::map< Node, TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+ for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
Node t = it->first;
if( m.d_map[ ic ].isNull() || m.d_map[ ic ]==t ){
Node prev = m.d_map[ ic ];
m.d_map[ ic ] = t;
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second), instLimit, addSplits );
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
m.d_map[ ic ] = prev;
}
}
}else{
Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map< Node, TermArgTrie >::iterator it = tat->d_data.find( r );
+ std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
if( it!=tat->d_data.end() ){
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second), instLimit, addSplits );
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback