From bad7f4fe4dca4c6511c2862bf81b6791640ac78f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 15 Sep 2015 10:39:29 +0200 Subject: [PATCH] Fix bug related to quantifiers + incremental, thanks John Backes for the bug report. Other minor cleanup. --- .../quantifiers/conjecture_generator.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 16 ++++++++-- src/theory/quantifiers/term_database.h | 4 ++- src/theory/quantifiers_engine.cpp | 12 ++++---- src/theory/quantifiers_engine.h | 2 +- src/theory/theory_model.cpp | 29 ------------------- src/theory/theory_model.h | 5 ---- test/regress/regress0/push-pop/Makefile.am | 3 +- .../regress0/push-pop/bug-fmf-fun-skolem.smt2 | 25 ++++++++++++++++ 9 files changed, 53 insertions(+), 45 deletions(-) create mode 100644 test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 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; iisClosedEnumerableType( 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; id_skolem_constants[it->first].size(); i++ ){ + for( unsigned i=0; id_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::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); diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index bcd8da228..501e7b2c6 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -40,7 +40,8 @@ BUG_TESTS = \ quant-fun-proc.smt2 \ quant-fun-proc-unmacro.smt2 \ quant-fun-proc-unfd.smt2 \ - bug654-dd.smt2 + bug654-dd.smt2 \ + bug-fmf-fun-skolem.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 new file mode 100644 index 000000000..d5effc083 --- /dev/null +++ b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 @@ -0,0 +1,25 @@ +; COMMAND-LINE: --incremental --fmf-fun +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l))))) + +(declare-fun input () Int) +(declare-fun p () Bool) +(declare-fun acc () Lst) +(assert (and (= acc (ite (>= input 0) (cons input nil) nil)) + (= p (>= (sum acc) 0)))) + + +; EXPECT: unsat +(push 1) +(assert (not p)) +(check-sat) +(pop 1) + +; EXPECT: unsat +(push 1) +(assert (not p)) +(check-sat) +(pop 1) + + -- 2.30.2