}
+
+/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, 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.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+ std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+ if( it!=d_data.end() ){
+ it->second->addInstMatch2( qe, f, m, c, index+1, imtio );
+ }else{
+ CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+ d_data[n] = imt;
+ imt->d_valid = true;
+ imt->addInstMatch2( qe, f, m, c, index+1, imtio );
+ }
+ }
+}
+
+/** exists match */
+bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
+ if( !d_valid ){
+ return false;
+ }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
+ return true;
+ }else{
+ int i_index = imtio ? imtio->d_order[index] : index;
+ Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+ std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+ if( it!=d_data.end() ){
+ if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+ return true;
+ }
+ }
+ //check if m is an instance of another instantiation if modInst is true
+ if( modInst ){
+ if( !n.isNull() ){
+ Node nl;
+ it = d_data.find( nl );
+ if( it!=d_data.end() ){
+ if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+ return true;
+ }
+ }
+ }
+ }
+ if( modEq ){
+ //check modulo equality if any other instantiation match exists
+ if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+ eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+ qe->getEqualityQuery()->getEngine() );
+ while( !eqc.isFinished() ){
+ Node en = (*eqc);
+ if( en!=n ){
+ std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
+ if( itc!=d_data.end() ){
+ if( itc->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+ return true;
+ }
+ }
+ }
+ ++eqc;
+ }
+ }
+ }
+ return false;
+ }
+}
+
+bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+ return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
+}
+
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+ if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
+ addInstMatch2( qe, f, m, c, 0, imtio );
+ return true;
+ }else{
+ return false;
+ }
+}
+
+
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
#include "util/hash.h"
+#include "context/cdo.h"
#include <ext/hash_set>
#include <map>
bool modInst = false, ImtIndexOrder* imtio = NULL );
};/* class InstMatchTrie */
+
+/** trie for InstMatch objects */
+class CDInstMatchTrie {
+public:
+ class ImtIndexOrder {
+ public:
+ std::vector< int > d_order;
+ };/* class InstMatchTrie ImtIndexOrder */
+private:
+ /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+ void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
+ /** exists match */
+ bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
+public:
+ /** the data */
+ std::map< Node, CDInstMatchTrie* > d_data;
+ /** is valid */
+ context::CDO< bool > d_valid;
+public:
+ CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
+ ~CDInstMatchTrie(){}
+public:
+ /** return true if m exists in this trie
+ modEq is if we check modulo equality
+ modInst is if we return true if m is an instance of a match that exists
+ */
+ bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
+ bool modInst = false, ImtIndexOrder* imtio = NULL );
+ /** add match m for quantifier f, take into account equalities if modEq = true,
+ if imtio is non-null, this is the order to add to trie
+ return true if successful
+ */
+ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+ bool modInst = false, ImtIndexOrder* imtio = NULL );
+};/* class CDInstMatchTrie */
+
class InstMatchTrieOrdered{
private:
InstMatchTrie::ImtIndexOrder* d_imtio;
}else{
d_isup = NULL;
}
- InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
- InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+ int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE;
+ InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 );
i_ag->setGenerateAdditional( true );
addInstStrategy( i_ag );
//addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
# Whether to use smart triggers
option smartTriggers /--disable-smart-triggers bool :default true
disable smart triggers
+# Whether to use relevent triggers
+option relevantTriggers /--relevant-triggers bool :default true
+ prefer triggers that are more relevant based on SInE style method
# Whether to consider terms in the bodies of quantifiers for matching
option registerQuantBodyTerms --register-quant-body-terms bool :default false
using namespace CVC4::theory;
using namespace CVC4::theory::inst;
-QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
+QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
-d_quant_rel( false ){ //currently do not care about relevance
+d_quant_rel( false ),
+d_lemmas_produced_c(u){
d_eq_query = new EqualityQueryQuantifiersEngine( this );
d_term_db = new quantifiers::TermDb( this );
d_tr_trie = new inst::TriggerTrie;
return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
}
+context::Context* QuantifiersEngine::getUserContext(){
+ return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
+}
+
OutputChannel& QuantifiersEngine::getOutputChannel(){
return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
}
bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
- if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+ if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
return true;
}
}
bool QuantifiersEngine::addLemma( Node lem ){
Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
lem = Rewriter::rewrite(lem);
- if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
+ if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
//d_curr_out->lemma( lem );
- d_lemmas_produced[ lem ] = true;
+ d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
return true;
}
}
//check for duplication modulo equality
- if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
+ inst::CDInstMatchTrie* imt;
+ std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
+ if( it!=d_inst_match_trie.end() ){
+ imt = it->second;
+ }else{
+ imt = new CDInstMatchTrie( getUserContext() );
+ d_inst_match_trie[f] = imt;
+ }
+ Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+ if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
Trace("inst-add-debug") << " -> Already exists." << std::endl;
++(d_statistics.d_inst_duplicate);
return false;
}
+ Trace("inst-add-debug") << "compute terms" << std::endl;
//compute the vector of terms for the instantiation
std::vector< Node > terms;
for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
std::vector< Node > d_quants;
/** list of all lemmas produced */
std::map< Node, bool > d_lemmas_produced;
+ BoolMap d_lemmas_produced_c;
/** lemmas waiting */
std::vector< Node > d_lemmas_waiting;
/** has added lemma this round */
bool d_hasAddedLemma;
/** list of all instantiations produced for each quantifier */
- std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
+ std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie;
/** term database */
quantifiers::TermDb* d_term_db;
/** all triggers will be stored in this trie */
private:
KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
public:
- QuantifiersEngine(context::Context* c, TheoryEngine* te);
+ QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
~QuantifiersEngine();
/** get instantiator for id */
//Instantiator* getInstantiator( theory::TheoryId id );
quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
+ /** get default sat context for quantifiers engine */
+ context::Context* getUserContext();
/** get default output channel for the quantifiers engine */
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
}
// initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(context, this);
+ d_quantEngine = new QuantifiersEngine(context, userContext, this);
// build model information if applicable
d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
projects / cvc5.git / commitdiff