From 9ac5255577a07e3bef123908d55003f89dea7619 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 26 Aug 2016 16:27:57 -0500 Subject: [PATCH] Basic support for EPR+CBQI. Minor cleanup. --- src/options/quantifiers_options | 3 + src/theory/quantifiers/inst_strategy_cbqi.cpp | 78 +++++++++++++++---- src/theory/quantifiers/inst_strategy_cbqi.h | 2 +- src/theory/quantifiers/quant_util.cpp | 68 ++++++++++++++++ src/theory/quantifiers/quant_util.h | 26 ++++++- src/theory/quantifiers/relevant_domain.h | 1 + src/theory/quantifiers/term_database.cpp | 1 - src/theory/quantifiers/theory_quantifiers.cpp | 5 +- src/theory/quantifiers_engine.cpp | 27 ++++++- src/theory/quantifiers_engine.h | 5 ++ src/theory/strings/theory_strings.cpp | 1 - 11 files changed, 196 insertions(+), 21 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index cb4f292c1..9f8f088de 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -306,6 +306,9 @@ option cbqiLitDepend --cbqi-lit-dep bool :default false option cbqiInnermost --cbqi-innermost bool :default false only process innermost quantified formulas in counterexample-based quantifier instantiation +option quantEpr --quant-epr bool :default false + infer whether in effectively propositional fragment, use for cbqi + ### local theory extensions options option localTheoryExt --local-t-ext bool :default false diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 21df4c712..b9a415e46 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -82,6 +82,35 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); + //totality lemmas for EPR + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + for( unsigned i=0; iisEPR( tn ) ){ + //add totality lemma + std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); + if( itc!=qepr->d_consts.end() ){ + Assert( !itc->second.empty() ); + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); + std::vector< Node > disj; + for( unsigned j=0; jsecond.size(); j++ ){ + disj.push_back( ic.eqNode( itc->second[j] ) ); + } + Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + Trace("cbqi") << "EPR totality lemma : " << tlem << std::endl; + d_quantEngine->getOutputChannel().lemma( tlem ); + }else{ + Assert( false ); + } + }else{ + Assert( !options::cbqiAll() ); + } + } + } + } + //compute dependencies between quantified formulas if( options::cbqiLitDepend() || options::cbqiInnermost() ){ std::vector< Node > ics; @@ -243,21 +272,28 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit } return false; } -bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){ +int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ + int hmin = 1; for( unsigned i=0; igetQuantEPR(); + if( qepr!=NULL ){ + handled = qepr->isEPR( tn ) ? 1 : -1; } } + if( handled==-1 ){ + return -1; + }else if( handledgetTermDatabase()->getInstConstantBody( q ); - std::map< Node, bool > visited; - ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited ); + int ncbqiv = hasNonCbqiVariable( q ); + if( ncbqiv==1 ){ + //all variables imply this will be handled regardless of body (e.g. for EPR) + ret = true; + }else if( ncbqiv==0 ){ + std::map< Node, bool > visited; + ret = !hasNonCbqiOperator( q[1], visited ); + } } } } @@ -727,6 +769,16 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){ return true; }else{ + TypeNode tn = n.getType(); + if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + //legal if in the finite set of constants of type tn + if( qepr->isEPRConstant( tn, n ) ){ + return true; + } + } + } //only legal if current quantified formula contains n return TermDb::containsTerm( d_curr_quant, n ); } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 20d872c36..18931f8f6 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -52,7 +52,7 @@ protected: /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } /** helper functions */ - bool hasNonCbqiVariable( Node q ); + int hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b9aab0236..8ba6aa611 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -419,3 +419,71 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, } } +void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) { + int vindex = hasPol ? ( pol ? 1 : -1 ) : 0; + if( visited[vindex].find( n )==visited[vindex].end() ){ + visited[vindex][n] = true; + if( n.getKind()==FORALL ){ + if( beneathQuant || !hasPol || !pol ){ + for( unsigned i=0; i0 ){ + if( tn.isSort() ){ + if( d_non_epr.find( tn )==d_non_epr.end() ){ + Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl; + d_non_epr[tn] = true; + } + } + for( unsigned i=0; i > visited; + registerNode( assertion, visited, false, true, true ); +} + +void QuantEPR::finishInit() { + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){ + if( d_non_epr.find( it->first )!=d_non_epr.end() ){ + it->second.clear(); + }else{ + if( it->second.empty() ){ + it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) ); + } + if( Trace.isOn("quant-epr") ){ + Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + Trace("quant-epr") << " " << it->second[i] << std::endl; + } + } + } + } +} + +bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) { + return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end(); +} + diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 79cdae437..049644ffb 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -149,7 +149,7 @@ public: }; -class EqualityQuery : public QuantifiersUtil{ +class EqualityQuery : public QuantifiersUtil { public: EqualityQuery(){} virtual ~EqualityQuery(){}; @@ -171,6 +171,30 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ +class QuantEPR +{ +private: + void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); + /** non-epr */ + std::map< TypeNode, bool > d_non_epr; +public: + QuantEPR(){} + virtual ~QuantEPR(){} + /** constants per type */ + std::map< TypeNode, std::vector< Node > > d_consts; + /* reset */ + //bool reset( Theory::Effort e ) {} + /** identify */ + //std::string identify() const { return "QuantEPR"; } + /** register assertion */ + void registerAssertion( Node assertion ); + /** finish init */ + void finishInit(); + /** is EPR */ + bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; } + /** is EPR constant */ + bool isEPRConstant( TypeNode tn, Node k ); +}; } } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 2b90520fd..8bc8e1f04 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -72,6 +72,7 @@ public: RDomain * getRDomain( Node n, int i, bool getParent = true ); };/* class RelevantDomain */ + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d3a5e178f..5d8564adf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -3125,7 +3125,6 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::string name = std::string( str.begin() + found +1, str.end() ); out << name; }else{ - Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl; out << op; } if( n.getNumChildren()>0 ){ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index f6ee639b6..e97a76ce6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -89,7 +89,10 @@ void TheoryQuantifiers::presolve() { } void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) { - getQuantifiersEngine()->ppNotifyAssertions( assertions ); + Trace("quantifiers-presolve") << "TheoryQuantifiers::ppNotifyAssertions" << std::endl; + if( getQuantifiersEngine() ){ + getQuantifiersEngine()->ppNotifyAssertions( assertions ); + } } Node TheoryQuantifiers::getValue(TNode n) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0c7deb85d..603f6f5fd 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -112,6 +112,17 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_quant_rel = NULL; } + if( options::quantEpr() ){ + if( !options::incrementalSolving() ){ + d_qepr = new QuantEPR; + }else{ + d_qepr = NULL; + } + }else{ + d_qepr = NULL; + } + + d_qcf = NULL; d_sg_gen = NULL; d_inst_engine = NULL; @@ -152,6 +163,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_alpha_equiv; delete d_builder; + delete d_qepr; delete d_rr_engine; delete d_bint; delete d_model_engine; @@ -275,7 +287,7 @@ void QuantifiersEngine::finishInit(){ d_modules.push_back( d_fs ); needsRelDom = true; } - + if( needsRelDom ){ d_rel_dom = new quantifiers::RelevantDomain( this, d_model ); d_util.push_back( d_rel_dom ); @@ -344,9 +356,18 @@ void QuantifiersEngine::presolve() { } void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) { - if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ + Trace("quant-engine-proc") << "ppNotifyAssertions in QE" << std::endl; + if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){ for( unsigned i=0; iregisterAssertion( assertions[i] ); + } + } + if( d_qepr!=NULL ){ + d_qepr->finishInit(); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7b4453330..7f0785340 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -113,6 +113,9 @@ private: quantifiers::AlphaEquivalence * d_alpha_equiv; /** model builder */ quantifiers::QModelBuilder* d_builder; + /** utility for effectively propositional logic */ + QuantEPR * d_qepr; +private: /** instantiation engine */ quantifiers::InstantiationEngine* d_inst_engine; /** model engine */ @@ -228,6 +231,8 @@ public: QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } + /** get utility for EPR */ + QuantEPR* getQuantEPR() { return d_qepr; } public: //modules /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7caa1cbb1..4526300f8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -905,7 +905,6 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te } for (unsigned c = 0; c < currentPairs.size(); ++ c) { Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; - Trace("ajr-temp") << currentPairs[c].first << ", " << currentPairs[c].second << std::endl; addCarePair(currentPairs[c].first, currentPairs[c].second); } } -- 2.30.2