diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-15 10:39:29 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-15 10:39:29 +0200 |
commit | bad7f4fe4dca4c6511c2862bf81b6791640ac78f (patch) | |
tree | 0be31a9300766d39ae36c9efba02e2c5a68dd156 /src/theory | |
parent | ace360b4da1edef06088a366dc21b58f9431efc2 (diff) |
Fix bug related to quantifiers + incremental, thanks John Backes for the bug report. Other minor cleanup.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 29 | ||||
-rw-r--r-- | src/theory/theory_model.h | 5 |
7 files changed, 26 insertions, 44 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 3cf603100..896cf5dff 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1048,7 +1048,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< for( unsigned i=0; i<n.getNumChildren(); i++ ){ vec.push_back( 0 ); TypeNode tn = n[i].getType(); - if( TermDb::isClosedEnumerableType( tn ) ){ + if( getTermDatabase()->isClosedEnumerableType( tn ) ){ types.push_back( tn ); }else{ return; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d076c6510..bb35ac4cd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -418,7 +418,7 @@ bool TermDb::mayComplete( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); if( it==d_may_complete.end() ){ bool mc = false; - if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ + if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); @@ -964,7 +964,19 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { } bool TermDb::isClosedEnumerableType( TypeNode tn ) { - return !tn.isArray() && !tn.isSort() && !tn.isCodatatype(); + std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn ); + if( it==d_typ_closed_enum.end() ){ + bool ret = true; + if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){ + ret = false; + }else{ + //TODO: all subfields must be closed enumerable? + } + d_typ_closed_enum[tn] = ret; + return ret; + }else{ + return it->second; + } } Node TermDb::getFreeVariableForInstConstant( Node n ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fb80cb8a8..7c136a186 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -279,11 +279,13 @@ private: //type enumerators std::map< TypeNode, unsigned > d_typ_enum_map; std::vector< TypeEnumerator > d_typ_enum; + // closed enumerable type cache + std::map< TypeNode, bool > d_typ_closed_enum; public: //get nth term for type Node getEnumerateTerm( TypeNode tn, unsigned index ); //does this type have an enumerator that produces constants that are handled by ground theory solvers - static bool isClosedEnumerableType( TypeNode tn ); + bool isClosedEnumerableType( TypeNode tn ); //miscellaneous public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1a5be5a57..23d46fd40 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,7 +80,8 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), -d_lemmas_produced_c(u){ +d_lemmas_produced_c(u), +d_skolemized(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; @@ -1000,13 +1001,14 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool printed = false; - for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ + for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ + Node q = (*it).first; printed = true; - out << "Skolem constants of " << it->first << " : " << std::endl; + out << "Skolem constants of " << q << " : " << std::endl; out << " ( "; - for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){ + for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){ if( i>0 ){ out << ", "; } - out << d_term_db->d_skolem_constants[it->first][i]; + out << d_term_db->d_skolem_constants[q][i]; } out << " )" << std::endl; out << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2658d09f0..cc8baa1c0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -178,7 +178,7 @@ private: std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; /** quantifiers that have been skolemized */ - std::map< Node, bool > d_skolemized; + BoolMap d_skolemized; /** term database */ quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5766a26c1..c4bc94bd2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -236,35 +236,6 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ return Node::null(); } -//FIXME: need to ensure that theory enumerators exist for each sort -Node TheoryModel::getNewDomainValue( TypeNode tn ){ - if( tn.isSort() ){ - return Node::null(); - }else{ - TypeEnumerator te(tn); - while( !te.isFinished() ){ - Node r = *te; - if(Debug.isOn("getNewDomainValue")) { - Debug("getNewDomainValue") << "getNewDomainValue( " << tn << ")" << endl; - Debug("getNewDomainValue") << "+ TypeEnumerator gave: " << r << endl; - Debug("getNewDomainValue") << "+ d_type_reps are:"; - for(vector<Node>::const_iterator i = d_rep_set.d_type_reps[tn].begin(); - i != d_rep_set.d_type_reps[tn].end(); - ++i) { - Debug("getNewDomainValue") << " " << *i; - } - Debug("getNewDomainValue") << endl; - } - if( std::find(d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r) ==d_rep_set.d_type_reps[tn].end() ) { - Debug("getNewDomainValue") << "+ it's new, so returning " << r << endl; - return r; - } - ++te; - } - return Node::null(); - } -} - /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 092b5e8c7..e023edadd 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -72,11 +72,6 @@ public: * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude */ Node getDomainValue( TypeNode tn, std::vector< Node >& exclude ); - /** get new domain value - * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn] - * If it cannot find such a node, it returns null. - */ - Node getNewDomainValue( TypeNode tn ); public: /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); |