From eb27070783709a410e6655ba9af6da6de5b0da9d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 16 Mar 2016 13:57:53 -0500 Subject: [PATCH] Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification. --- src/theory/quantifiers/full_model_check.cpp | 2 ++ src/theory/quantifiers/model_engine.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 32 ++++++++++----------- src/theory/quantifiers/term_database.h | 4 ++- src/theory/quantifiers_engine.cpp | 11 ++++--- 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; iisInterval(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 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 InstVarNumAttribute; struct TermDepthAttributeId {}; typedef expr::Attribute TermDepthAttribute; +struct ContainsUConstAttributeId {}; +typedef expr::Attribute ContainsUConstAttribute; + struct ModelBasisAttributeId {}; typedef expr::Attribute 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; -- 2.30.2