diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-16 13:57:53 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-16 13:57:53 -0500 |
commit | eb27070783709a410e6655ba9af6da6de5b0da9d (patch) | |
tree | c4fcb9203e2e72c9a96a51641ac15207f292a75b /src | |
parent | fd3844131f334e929bfb04eb2dcb6229cf1190cd (diff) |
Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
6 files changed, 31 insertions, 23 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 98cd175fd..5e4b6828e 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -744,12 +744,14 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No for( unsigned i=0; i<c.getNumChildren(); i++ ){ if( c[i].getType().isInteger() ){ if( fm->isInterval(c[i]) ){ + Trace("fmc-exh-debug") << "...set " << i << " based on interval." << std::endl; for( unsigned b=0; b<2; b++ ){ if( !fm->isStar(c[i][b]) ){ riter.d_bounds[b][i] = c[i][b]; } } }else if( !fm->isStar(c[i]) ){ + Trace("fmc-exh-debug") << "...set " << i << " based on point." << std::endl; riter.d_bounds[0][i] = c[i]; riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 4b173c833..70ee01b92 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -274,7 +274,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl; + Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl; if( !riter.d_incomplete ){ int triedLemmas = 0; int addedLemmas = 0; @@ -299,6 +299,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_statistics.d_exh_inst_lemmas += addedLemmas; } }else{ + Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl; Assert( riter.d_incomplete ); } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 4c58aa886..0d7c9352c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1652,20 +1652,6 @@ bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, boo return false; } -bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) { - if( n.getKind()==UNINTERPRETED_CONSTANT ){ - return true; - }else if( visited.find( n )==visited.end() ){ - visited[n] = true; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( containsUninterpretedConstant2( n[i], visited ) ){ - return true; - } - } - } - return false; -} - bool TermDb::containsTerm( Node n, Node t ) { std::map< Node, bool > visited; return containsTerm2( n, t, visited ); @@ -1696,8 +1682,22 @@ int TermDb::getTermDepth( Node n ) { } bool TermDb::containsUninterpretedConstant( Node n ) { - std::map< Node, bool > visited; - return containsUninterpretedConstant2( n, visited ); + if (!n.hasAttribute(ContainsUConstAttribute()) ){ + bool ret = false; + if( n.getKind()==UNINTERPRETED_CONSTANT ){ + ret = true; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( containsUninterpretedConstant( n[i] ) ){ + ret = true; + break; + } + } + } + ContainsUConstAttribute cuca; + n.setAttribute(cuca, ret ? 1 : 0); + } + return n.getAttribute(ContainsUConstAttribute())!=0; } Node TermDb::simpleNegate( Node n ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fcacbd686..6b8f9c783 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -71,6 +71,9 @@ typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; struct TermDepthAttributeId {}; typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute; +struct ContainsUConstAttributeId {}; +typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute; + struct ModelBasisAttributeId {}; typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; //for APPLY_UF terms, 1 : term has direct child with model basis attribute, @@ -429,7 +432,6 @@ private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); - static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ); //general utilities public: /** simple check for whether n contains t as subterm */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 568483380..4be55ebb5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -88,6 +88,9 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_te( te ), d_lemmas_produced_c(u), d_skolemized(u), + //d_ierCounter(c), + //d_ierCounter_lc(c), + //d_ierCounterLastLc(c), d_presolve(u, true), d_presolve_in(u), d_presolve_cache(u), @@ -141,7 +144,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; d_ierCounter_lc = 0; - d_ierCounterLastLc = d_ierCounter_lc; + d_ierCounterLastLc = 0; d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); } @@ -465,11 +468,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_FULL ){ //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){ - d_ierCounter++; + d_ierCounter = d_ierCounter + 1; d_ierCounterLastLc = d_ierCounter_lc; } }else if( e==Theory::EFFORT_LAST_CALL ){ - d_ierCounter_lc++; + d_ierCounter_lc = d_ierCounter_lc + 1; } }else if( quant_e==QEFFORT_MODEL ){ if( e==Theory::EFFORT_LAST_CALL ){ @@ -1339,7 +1342,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, Assert( f.isNull() || f.getKind()==FORALL ); Node r = getRepresentative( a ); if( options::finiteModelFind() ){ - if( r.isConst() ){ + if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any if( d_qe->getModel() ){ std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0c43223d8..228ac9ee9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -203,7 +203,7 @@ private: std::map< Node, int > d_total_inst_debug; std::map< Node, int > d_temp_inst_debug; int d_total_inst_count_debug; - /** inst round counters */ + /** inst round counters TODO: make context-dependent? */ int d_ierCounter; int d_ierCounter_lc; int d_ierCounterLastLc; |