From d9d13027f1f1e3cc462dc5885dfd0b529bf57512 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 22 Jan 2015 11:47:39 +0100 Subject: [PATCH] Add option --lte-partial-inst. Remove inst-closure. --- src/parser/smt2/Smt2.g | 4 - src/theory/quantifiers/kinds | 3 - src/theory/quantifiers/options | 4 +- src/theory/quantifiers/quant_util.cpp | 141 +++++++++++++++++- src/theory/quantifiers/quant_util.h | 31 +++- src/theory/quantifiers/term_database.cpp | 35 ++--- src/theory/quantifiers/term_database.h | 8 +- src/theory/quantifiers/theory_quantifiers.cpp | 10 -- .../theory_quantifiers_type_rules.h | 15 -- src/theory/quantifiers_engine.cpp | 27 +++- src/theory/quantifiers_engine.h | 4 +- 11 files changed, 216 insertions(+), 66 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a83299d3b..81e93ebe6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2002,8 +2002,6 @@ builtinOp[CVC4::Kind& kind] | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } - | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } - | FP_TOK { $kind = CVC4::kind::FLOATINGPOINT_FP; } | FP_EQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_EQ; } | FP_ABS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ABS; } @@ -2472,8 +2470,6 @@ 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/kinds b/src/theory/quantifiers/kinds index 793e4a611..a8774440e 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -44,8 +44,6 @@ 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 @@ -53,7 +51,6 @@ 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 afa894473..009a0ada6 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -205,7 +205,7 @@ option sygusNormalFormArg --sygus-nf-arg bool :default true 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 +option ltePartialInst --lte-partial-inst bool :default false + partially instantiate local theory quantifiers endmodule diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 62a87bb99..2a9a764b9 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4; @@ -253,4 +254,142 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol = false; } } -} \ No newline at end of file +} + + +QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){ + +} + +/** add quantifier */ +bool QuantLtePartialInst::addQuantifier( Node q ) { + if( d_do_inst.find( q )!=d_do_inst.end() ){ + if( d_do_inst[q] ){ + d_lte_asserts.push_back( q ); + return true; + }else{ + return false; + } + }else{ + d_vars[q].clear(); + //check if this quantified formula is eligible for partial instantiation + std::map< Node, bool > vars; + for( unsigned i=0; i& vars ) { + if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){ + for( unsigned i=0; igetMasterEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + TypeNode tn = r.getType(); + d_reps[tn].push_back( r ); + ++eqcs_i; + } +} + +/** get instantiations */ +void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { + Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; + reset(); + for( unsigned i=0; i bvs; + for( unsigned j=0; jmkNode( BOUND_VAR_LIST, bvs ); + } + std::vector< Node > conj; + std::vector< Node > terms; + std::vector< TypeNode > types; + for( unsigned j=0; jmkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); + } + } +} + +void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){ + if( index==vars.size() ){ + Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( bvl.isNull() ){ + conj.push_back( body ); + Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; + }else{ + Node nq; + if( q.getNumChildren()==3 ){ + Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); + }else{ + nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); + } + Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; + LtePartialInstAttribute ltpia; + nq.setAttribute(ltpia,true); + conj.push_back( nq ); + } + }else{ + std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] ); + if( it!=d_reps.end() ){ + terms.push_back( Node::null() ); + Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + terms[index] = it->second[i]; + getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 ); + } + terms.pop_back(); + }else{ + Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl; + } + } +} diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 575a7237d..c1c39fa0f 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -27,7 +27,8 @@ namespace CVC4 { namespace theory { - +class QuantifiersEngine; + class QuantArith { public: @@ -109,6 +110,34 @@ public: virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ +class QuantLtePartialInst { +private: + std::map< TypeNode, std::vector< Node > > d_reps; + // should we instantiate quantifier + std::map< Node, bool > d_do_inst; + // have we instantiated quantifier + std::map< Node, bool > d_inst; + std::map< Node, std::vector< Node > > d_vars; + /** pointer to quant engine */ + QuantifiersEngine * d_qe; + /** list of relevant quantifiers asserted in the current context */ + context::CDList d_lte_asserts; + /** reset */ + void reset(); + /** get instantiations */ + void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index ); + /** get eligible inst variables */ + void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); +public: + QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ); + /** add quantifier */ + bool addQuantifier( Node q ); + /** get instantiations */ + void getInstantiations( std::vector< Node >& lemmas ); +}; + + } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index efa12b893..bb0b3248d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -111,7 +111,7 @@ Node TermDb::getOperator( Node n ) { } } -void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){ +void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; @@ -119,9 +119,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi 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? @@ -154,13 +151,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi } } 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 ) { - if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ - return false; + //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{ - //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; - } + Assert( false ); + return false; } } @@ -344,6 +334,7 @@ Node TermDb::getHasTermEqc( Node r ) { if( hasTermCurrent( r ) ){ return r; }else{ + /* if( options::termDbInstClosure() ){ std::map< Node, Node >::iterator it = d_has_eqc.find( r ); if( it==d_has_eqc.end() ){ @@ -362,10 +353,10 @@ Node TermDb::getHasTermEqc( Node r ) { }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(); } + */ + //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc + return Node::null(); } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index cb9f5eeef..fca2e1261 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -84,6 +84,10 @@ typedef expr::Attribute QuantInstLevelAttri struct RrPriorityAttributeId {}; typedef expr::Attribute RrPriorityAttribute; +/** Attribute true for quantifiers that do not need to be partially instantiated */ +struct LtePartialInstAttributeId {}; +typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; + class QuantifiersEngine; namespace inst{ @@ -123,8 +127,6 @@ 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; @@ -156,7 +158,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, bool withinInstClosure = false ); + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); /** get operator*/ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index de0f98af6..89549a71b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -129,22 +129,12 @@ 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; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 341e656c7..2d5cce6ed 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -125,21 +125,6 @@ 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 d6c6f4667..3ef5b4a65 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -153,6 +153,11 @@ d_lemmas_produced_c(u){ }else{ d_ceg_inst = NULL; } + if( options::ltePartialInst() ){ + d_lte_part_inst = new QuantLtePartialInst( this, c ); + }else{ + d_lte_part_inst = NULL; + } if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; @@ -191,6 +196,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_eq_query; delete d_sg_gen; delete d_ceg_inst; + delete d_lte_part_inst; for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } @@ -254,10 +260,14 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_FULL ){ d_ierCounter++; + //process partial instantiations for LTE + if( d_lte_part_inst ){ + d_lte_part_inst->getInstantiations( d_lemmas_waiting ); + } }else if( e==Theory::EFFORT_LAST_CALL ){ d_ierCounter_lc++; } - bool needsCheck = false; + bool needsCheck = !d_lemmas_waiting.empty(); bool needsModel = false; bool needsFullModel = false; std::vector< QuantifiersModule* > qm; @@ -285,6 +295,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; + if( !d_lemmas_waiting.empty() ){ + Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; + } Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; Trace("quant-engine-ee") << "Equality engine : " << std::endl; @@ -295,7 +308,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_conflict = false; d_hasAddedLemma = false; - //flush previous lemmas (for instance, if was interupted) + //flush previous lemmas (for instance, if was interupted), or other lemmas to process flushLemmas(); if( d_hasAddedLemma ){ return; @@ -450,6 +463,12 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } //assert to modules TODO : handle !pol if( pol ){ + if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ + Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; + if( d_lte_part_inst->addQuantifier( f ) ){ + return; + } + } //register the quantifier registerQuantifier( f ); //assert it to each module @@ -478,9 +497,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } -void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ +void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); + getTermDatabase()->addTerm( n, added, withinQuant ); //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 ac782a536..2fc479f4c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -134,6 +134,8 @@ private: quantifiers::ConjectureGenerator * d_sg_gen; /** ceg instantiation */ quantifiers::CegInstantiation * d_ceg_inst; + /** lte partial instantiation */ + QuantLtePartialInst * d_lte_part_inst; public: //effort levels enum { QEFFORT_CONFLICT, @@ -295,7 +297,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); + void addTermToDatabase( Node n, bool withinQuant = false ); /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; /** debug print equality engine */ -- 2.30.2