From 29bdfca306a7cd35801c7d9cb3023d78a8b82a1f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 25 Nov 2014 16:15:10 +0100 Subject: [PATCH] Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers. --- src/parser/smt2/Smt2.g | 4 + .../quantifiers/candidate_generator.cpp | 9 +- .../quantifiers/ce_guided_instantiation.cpp | 4 +- src/theory/quantifiers/kinds | 3 + src/theory/quantifiers/options | 2 + src/theory/quantifiers/term_database.cpp | 86 ++++++++++++++----- src/theory/quantifiers/term_database.h | 8 +- src/theory/quantifiers/theory_quantifiers.cpp | 33 ++++--- src/theory/quantifiers/theory_quantifiers.h | 7 +- .../theory_quantifiers_type_rules.h | 14 +++ src/theory/quantifiers_engine.cpp | 4 +- src/theory/quantifiers_engine.h | 2 +- 12 files changed, 122 insertions(+), 54 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bdad45606..511b67997 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1620,6 +1620,8 @@ builtinOp[CVC4::Kind& kind] | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + + | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } // NOTE: Theory operators go here ; @@ -2026,6 +2028,8 @@ DTSIZE_TOK : 'dt.size'; FMFCARD_TOK : 'fmf.card'; +INST_CLOSURE_TOK : 'inst-closure'; + EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; // Other set theory operators are not // tokenized and handled directly when diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index cfaa6d1ad..9e3fed20a 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -197,16 +197,17 @@ void CandidateGeneratorQEAll::reset( Node eqc ) { Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ - Node n = (*d_eq); + TNode n = (*d_eq); ++d_eq; if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ - if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n ); + if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 ){ - n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index ); + nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); } d_firstTime = false; //an equivalence class with the same type as the pattern, return it - return n; + return nh; } } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ffe64beba..bf9409f06 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -248,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { for( unsigned i=0; id_candidates.size(); i++ ){ Node t = getModelTerm( conj->d_candidates[i] ); model_terms.push_back( t ); - Trace("cegqi-engine") << t << " "; + Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " "; } Trace("cegqi-engine") << std::endl; d_quantEngine->addInstantiation( q, model_terms, false ); @@ -279,7 +279,7 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node for( unsigned i=0; i " << nv << " "; if( nv.isNull() ){ success = false; } diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index a8774440e..793e4a611 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -44,6 +44,8 @@ sort INST_PATTERN_LIST_TYPE \ # a list of instantiation patterns operator INST_PATTERN_LIST 1: "a list of instantiation patterns" +operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure." + typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule @@ -51,6 +53,7 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule +typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule # for rewrite rules # types... diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a428633cc..cac78af46 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions +option termDbInstClosure --term-db-inst-closure bool :default false + only consider inst closure terms for E-matching endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a95de086a..34c40c8c4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -111,13 +111,17 @@ Node TermDb::getOperator( Node n ) { } } -void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ +void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; } + bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); + if( withinInstClosure ){ + d_iclosure_processed.insert( n ); + } d_type_map[ n.getType() ].push_back( n ); //if this is an atomic trigger, consider adding it //Call the children? @@ -137,9 +141,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - for( size_t i=0; i& added, bool withinQuant ){ } } } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - } + } + rec = true; + }else if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ + d_iclosure_processed.insert( n ); + rec = true; + } + if( rec ){ + for( size_t i=0; i& subs, bool subsRep, } bool TermDb::hasTermCurrent( Node n ) { - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); - if( options::termDbMode()==TERM_DB_ALL ){ - return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ - return d_has_map.find( n )!=d_has_map.end(); - }else{ - Assert( false ); + if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ return false; + }else{ + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } } -void TermDb::setHasTerm( Node n ) { - if( inst::Trigger::isAtomicTrigger( n ) ){ - if( d_has_map.find( n )==d_has_map.end() ){ - d_has_map[n] = true; - for( unsigned i=0; i::iterator it = d_has_eqc.find( r ); + if( it==d_has_eqc.end() ){ + Node h; + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( h.isNull() && !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + ++eqc_i; + if( hasTermCurrent( n ) ){ + h = n; + } + } + d_has_eqc[r] = h; + return h; + }else{ + return it->second; } + }else{ + //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc + return Node::null(); + } + } +} + +void TermDb::setHasTerm( Node n ) { + //if( inst::Trigger::isAtomicTrigger( n ) ){ + if( d_has_map.find( n )==d_has_map.end() ){ + d_has_map[n] = true; + for( unsigned i=0; igetMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2b151bb04..cb9f5eeef 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -123,6 +123,8 @@ private: QuantifiersEngine* d_quantEngine; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_processed; + /** terms processed */ + std::hash_set< Node, NodeHashFunction > d_iclosure_processed; private: /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; @@ -144,6 +146,8 @@ public: std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; + /** map from reps to a term in eqc in d_has_map */ + std::map< Node, Node > d_has_eqc; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; @@ -152,7 +156,7 @@ public: /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; /** add a term to the database */ - void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); /** get operator*/ @@ -176,6 +180,8 @@ public: bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ bool hasTermCurrent( Node n ); + /** get has term eqc */ + Node getHasTermEqc( Node r ); //for model basis private: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5c68e52a7..de0f98af6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_numRestarts(0), d_masterEqualityEngine(0) { d_numInstantiations = 0; @@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) { } } +void TheoryQuantifiers::computeCareGraph() { + //do nothing +} + void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { if(fullModel) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { @@ -126,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) { case kind::FORALL: assertUniversal( assertion ); break; + case kind::INST_CLOSURE: + getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + break; + case kind::EQUAL: + //do nothing + break; case kind::NOT: { switch( assertion[0].getKind()) { case kind::FORALL: assertExistential( assertion ); break; + case kind::EQUAL: + //do nothing + break; + case kind::INST_CLOSURE: //cannot negate inst closure default: Unhandled(assertion[0].getKind()); break; @@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){ //}else{ // return false; //} - - if( !d_out->flipDecision() ){ - return restart(); - } - return true; -} - -bool TheoryQuantifiers::restart(){ - static const int restartLimit = 0; - if( d_numRestarts==restartLimit ){ - Debug("quantifiers-flip") << "No more restarts." << std::endl; - return false; - }else{ - d_numRestarts++; - Debug("quantifiers-flip") << "Do restart." << std::endl; - return true; - } + return false; } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index aace13b24..6d3fa4d46 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -44,17 +44,15 @@ private: /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; - /** number of restarts */ - int d_numRestarts; eq::EqualityEngine* d_masterEqualityEngine; - +private: + void computeCareGraph(); public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); @@ -73,7 +71,6 @@ public: private: void assertUniversal( Node n ); void assertExistential( Node n ); - bool restart(); };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index e44712412..341e656c7 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -126,6 +126,20 @@ struct QuantifierInstPatternListTypeRule { };/* struct QuantifierInstPatternListTypeRule */ +struct QuantifierInstClosureTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::INST_CLOSURE ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isBoolean() ){ + throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean"); + } + } + return nodeManager->booleanType(); + } +};/* struct QuantifierInstClosureTypeRule */ + class RewriteRuleTypeRule { public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 04b6c5d16..4dc8df09d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -472,9 +472,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } -void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ +void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant ); + getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); //maybe have triggered instantiations if we are doing eager instantiation if( options::eagerInstQuant() ){ flushLemmas(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 199fe79b9..2b466b96b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -290,7 +290,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false ); + void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; /** debug print equality engine */ -- 2.30.2