From b0d7ac44fb7be5c56cd0c743114e792a985bb3b7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 17 Feb 2016 17:35:56 -0600 Subject: [PATCH] Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct. --- src/smt/smt_engine.cpp | 66 ++++- src/smt/smt_engine.h | 2 +- src/theory/quantifiers/inst_match.cpp | 14 +- src/theory/quantifiers/inst_match.h | 24 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 43 +++- src/theory/quantifiers/inst_strategy_cbqi.h | 2 + .../quantifiers/quantifiers_attributes.cpp | 10 +- .../quantifiers/quantifiers_attributes.h | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 236 ++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 20 +- src/theory/quantifiers/term_database.cpp | 156 ++++++++---- src/theory/quantifiers/term_database.h | 45 +++- src/theory/quantifiers/theory_quantifiers.cpp | 2 + src/theory/quantifiers_engine.cpp | 25 +- src/theory/quantifiers_engine.h | 6 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- 17 files changed, 399 insertions(+), 258 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3dc64d61a..95995a765 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5056,34 +5056,74 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } -Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) { +Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException) { SmtScope smts(this); + if(!d_logic.isPure(THEORY_ARITH)){ + Warning() << "Unexpected logic for quantifier elimination." << endl; + } Trace("smt-qe") << "Do quantifier elimination " << e << std::endl; - Result r = query(e); + Node n_e = Node::fromExpr( e ); + if( n_e.getKind()!=kind::EXISTS ){ + throw ModalException("Expecting an existentially quantified formula as argument to get-qe."); + } + //tag the quantified formula with the quant-elim attribute + TypeNode t = NodeManager::currentNM()->booleanType(); + Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr."); + std::vector< Node > node_values; + d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); + n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr); + n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr); + std::vector< Node > e_children; + e_children.push_back( n_e[0] ); + e_children.push_back( n_e[1] ); + e_children.push_back( n_attr ); + Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children ); + Trace("smt-qe-debug") << "Query : " << nn_e << std::endl; + Assert( nn_e.getNumChildren()==3 ); + Result r = query(nn_e.toExpr()); Trace("smt-qe") << "Query returned " << r << std::endl; - if(r.asSatisfiabilityResult().isSat() == Result::SAT) { - Node input = Node::fromExpr( e ); - input = Rewriter::rewrite( input ); - Trace("smt-qe") << "Replace instances in rewritten input: " << input << std::endl; + if(r.asSatisfiabilityResult().isSat() == Result::SAT || ( !doFull && r.asSatisfiabilityResult().isSat() != Result::UNSAT ) ) { + //get the instantiations for all quantified formulas std::map< Node, std::vector< Node > > insts; d_theoryEngine->getInstantiations( insts ); + //find the quantified formula that corresponds to the input + Node top_q; + for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){ + Trace("smt-qe-debug") << "* quantifier " << it->first << " had " << it->second.size() << " instances." << std::endl; + if( it->first.getNumChildren()==3 && it->first[2]==n_attr ){ + top_q = it->first; + } + } std::map< Node, Node > visited; - Node en = d_private->replaceQuantifiersWithInstantiations( input, insts, visited ); + Node ret_n; + if( top_q.isNull() ){ + //no instances needed + ret_n = NodeManager::currentNM()->mkConst(true); + visited[top_q] = ret_n; + }else{ + //replace by a conjunction of instances + ret_n = d_private->replaceQuantifiersWithInstantiations( top_q, insts, visited ); + } //ensure all instantiations were accounted for for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){ if( visited.find( it->first )==visited.end() ){ stringstream ss; ss << "While performing quantifier elimination, processed a quantified formula : " << it->first; - ss << " that was not related to the query. Try option --simplification=none." << std::endl; + ss << " that was not related to the query. Try option --simplification=none."; InternalError(ss.str().c_str()); } } - Trace("smt-qe") << "Returned : " << en << std::endl; - en = Rewriter::rewrite( en ); - return en.toExpr(); - }else{ - return NodeManager::currentNM()->mkConst(false).toExpr(); + Trace("smt-qe") << "Returned : " << ret_n << std::endl; + ret_n = Rewriter::rewrite( ret_n.negate() ); + return ret_n.toExpr(); + }else { + if(r.asSatisfiabilityResult().isSat() != Result::UNSAT){ + stringstream ss; + ss << "While performing quantifier elimination, unexpected result : " << r << " for query."; + InternalError(ss.str().c_str()); + } + return NodeManager::currentNM()->mkConst(true).toExpr(); } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5aa33731e..68ea9c595 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -555,7 +555,7 @@ public: /** * Do quantifier elimination, doFull false means just output one disjunct */ - Expr doQuantifierElimination(const Expr& e, bool doFull); + Expr doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException); /** * Get an unsatisfiable core (only if immediately preceded by an diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index f2d5c640d..ead2bc57c 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -212,13 +212,14 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term } } -void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const { +void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const { if( terms.size()==q[0].getNumChildren() ){ - insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + insts.push_back( qe->getInstantiation( q, terms, true ) ); }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second.getInstantiations( insts, q, vars, terms ); + it->second.getInstantiations( insts, q, terms, qe ); terms.pop_back(); } } @@ -310,14 +311,15 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te } } -void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{ +void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ - insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + insts.push_back( qe->getInstantiation( q, terms, true ) ); }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second->getInstantiations( insts, q, vars, terms ); + it->second->getInstantiations( insts, q, terms, qe ); terms.pop_back(); } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index abe31b48d..35353863c 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,7 +101,7 @@ public: std::map< Node, InstMatchTrie > d_data; private: void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -132,13 +132,9 @@ public: std::vector< TNode > terms; print( out, q, terms ); } - void getInstantiations( std::vector< Node >& insts, Node q ) { - std::vector< TNode > terms; - std::vector< TNode > vars; - for( unsigned i=0; i& insts, Node q, QuantifiersEngine * qe ) { + std::vector< Node > terms; + getInstantiations( insts, q, terms, qe ); } void clear() { d_data.clear(); } };/* class InstMatchTrie */ @@ -152,7 +148,7 @@ public: context::CDO< bool > d_valid; private: void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -183,13 +179,9 @@ public: std::vector< TNode > terms; print( out, q, terms ); } - void getInstantiations( std::vector< Node >& insts, Node q ) { - std::vector< TNode > terms; - std::vector< TNode > vars; - for( unsigned i=0; i& insts, Node q, QuantifiersEngine * qe ) { + std::vector< Node > terms; + getInstantiations( insts, q, terms, qe ); } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d5ef2e290..ad400413e 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,8 +34,7 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ) - , d_added_cbqi_lemma( qe->getUserContext() ){ + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) { } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -98,6 +97,14 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { }else{ Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; } + //if doing partial quantifier elimination, do not process this if already processed once + if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){ + if( d_added_inst.find( q )!=d_added_inst.end() ){ + d_quantEngine->getModel()->setQuantifierActive( q, false ); + d_cbqi_set_quant_inactive = true; + d_incomplete_check = true; + } + } } } } @@ -201,20 +208,25 @@ bool InstStrategyCbqi::doCbqi( Node q ){ std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ bool ret = false; - //if has an instantiation pattern, don't do it - if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ - ret = false; + if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ + ret = true; }else{ - if( options::cbqiAll() ){ - ret = true; + //if has an instantiation pattern, don't do it + if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ + ret = false; }else{ - //if quantifier has a non-arithmetic variable, then do not use cbqi - //if quantifier has an APPLY_UF term, then do not use cbqi - Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); - std::map< Node, bool > visited; - ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited ); + if( options::cbqiAll() ){ + ret = true; + }else{ + //if quantifier has a non-arithmetic variable, then do not use cbqi + //if quantifier has an APPLY_UF term, then do not use cbqi + Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + std::map< Node, bool > visited; + ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited ); + } } } + Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret; }else{ @@ -623,7 +635,12 @@ bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //check if we need virtual term substitution (if used delta or infinity) bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); - return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ); + if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ + d_added_inst.insert( d_curr_quant ); + return true; + }else{ + return false; + } } bool InstStrategyCegqi::addLemma( Node lem ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 5511af209..8de844eb8 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -39,6 +39,8 @@ protected: bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** whether we have instantiated quantified formulas */ + NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 8c6b30124..040eadc9f 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -24,7 +24,7 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector node_values, std::string str_value ){ +void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; if( attr=="axiom" ){ Trace("quant-attr-debug") << "Set axiom " << n << std::endl; @@ -58,5 +58,13 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; RrPriorityAttribute rrpa; n.setAttribute( rrpa, lvl ); + }else if( attr=="quant-elim" ){ + Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; + QuantElimAttribute qea; + n.setAttribute( qea, true ); + }else if( attr=="quant-elim-partial" ){ + Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl; + QuantElimPartialAttribute qepa; + n.setAttribute( qepa, true ); } } diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index bad58eef8..55461e5c1 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -36,7 +36,7 @@ struct QuantifiersAttributes * This function will apply a custom set of attributes to all top-level universal * quantifiers contained in n */ - static void setUserAttribute( const std::string& attr, Node n, std::vector node_values, std::string str_value ); + static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ); }; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 881210d78..3c155c421 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -229,36 +229,27 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ - RewriteStatus status = REWRITE_DONE; - Node ret = in; - //get the arguments - std::vector< Node > args; - for( int i=0; i<(int)in[0].getNumChildren(); i++ ){ - args.push_back( in[0][i] ); - } - //get the instantiation pattern list - Node ipl; + RewriteStatus status = REWRITE_DONE; + Node ret = in; + //get the body + if( in.getKind()==EXISTS ){ + std::vector< Node > children; + children.push_back( in[0] ); + children.push_back( in[1].negate() ); if( in.getNumChildren()==3 ){ - ipl = in[2]; - } - //get the body - if( in.getKind()==EXISTS ){ - std::vector< Node > children; - children.push_back( in[0] ); - children.push_back( in[1].negate() ); - if( in.getNumChildren()==3 ){ - children.push_back( in[2] ); - } - ret = NodeManager::currentNM()->mkNode( FORALL, children ); - ret = ret.negate(); - status = REWRITE_AGAIN_FULL; - }else{ + children.push_back( in[2] ); + } + ret = NodeManager::currentNM()->mkNode( FORALL, children ); + ret = ret.negate(); + status = REWRITE_AGAIN_FULL; + }else if( in.getKind()==FORALL ){ + //compute attributes + QAttributes qa; + TermDb::computeQuantAttributes( in, qa ); + if( !qa.isRewriteRule() ){ for( int op=0; op& currCond, std::v } } -Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ){ +Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){ std::map< Node, bool > curr_cond; std::map< Node, Node > cache; std::map< Node, Node > icache; - Node h = TermDb::getFunDefHead( q ); - if( !h.isNull() ){ + if( qa.isFunDef() ){ + Node h = TermDb::getFunDefHead( q ); + Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently Node fbody = TermDb::getFunDefBody( q ); Assert( !body.isNull() ); @@ -782,7 +773,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ return false; } -Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){ +Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){ Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; std::map< Node, Node > pcons; @@ -799,7 +790,8 @@ Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){ } } if( options::condVarSplitQuant() ){ - if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){ + if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){ + Assert( !qa.isFunDef() ); Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; unsigned index_max = body.getKind()==ITE ? 0 : 1; @@ -956,7 +948,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto return false; } -Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){ +Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; QuantPhaseReq qpr( body ); std::vector< Node > vars; @@ -976,15 +968,15 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node > //remake with eliminated nodes body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); body = Rewriter::rewrite( body ); - if( !ipl.isNull() ){ - ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( !qa.d_ipl.isNull() ){ + qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); } Trace("var-elim-quant") << "Return " << body << std::endl; } return body; } -Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ +Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){ //the parent id's for each variable, if using purifyQuant std::map< Node, std::vector< int > > var_parent; if( options::purifyQuant() ){ @@ -994,7 +986,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& Node prev; do{ prev = body; - body = computeVarElimination2( body, args, ipl, var_parent ); + body = computeVarElimination2( body, args, qa, var_parent ); }while( prev!=body && !args.empty() ); } return body; @@ -1289,13 +1281,13 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node return f; } -Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ +Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){ std::vector< Node > activeArgs; //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables - if( options::ceGuidedInst() && TermDb::isSygusConjectureAnnotation( ipl ) ){ + if( options::ceGuidedInst() && qa.d_sygus ){ activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); }else{ - computeArgVec2( args, activeArgs, body, ipl ); + computeArgVec2( args, activeArgs, body, qa.d_ipl ); } if( activeArgs.empty() ){ return body; @@ -1303,14 +1295,14 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) ); children.push_back( body ); - if( !ipl.isNull() ){ - children.push_back( ipl ); + if( !qa.d_ipl.isNull() ){ + children.push_back( qa.d_ipl ); } return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } } -Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){ +Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){ if( body.getKind()==FORALL ){ //combine arguments std::vector< Node > newArgs; @@ -1318,26 +1310,26 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, newArgs.push_back( body[0][i] ); } newArgs.insert( newArgs.end(), args.begin(), args.end() ); - return mkForAll( newArgs, body[ 1 ], ipl ); + return mkForAll( newArgs, body[ 1 ], qa ); }else{ if( body.getKind()==NOT ){ //push not downwards if( body[0].getKind()==NOT ){ - return computeMiniscoping( f, args, body[0][0], ipl ); + return computeMiniscoping( f, args, body[0][0], qa ); }else if( body[0].getKind()==AND ){ if( options::miniscopeQuantFreeVar() ){ NodeBuilder<> t(kind::OR); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); } - return computeMiniscoping( f, args, t.constructNode(), ipl ); + return computeMiniscoping( f, args, t.constructNode(), qa ); } }else if( body[0].getKind()==OR ){ if( options::miniscopeQuant() ){ NodeBuilder<> t(kind::AND); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ Node trm = body[0][i].negate(); - t << computeMiniscoping( f, args, trm, ipl ); + t << computeMiniscoping( f, args, trm, qa ); } return t.constructNode(); } @@ -1347,7 +1339,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, //break apart NodeBuilder<> t(kind::AND); for( unsigned i=0; i& args, return body_split; }else if( body_split.getNumChildren()>0 ){ newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - body_split << mkForAll( args, newBody, ipl ); + body_split << mkForAll( args, newBody, qa ); return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; } } @@ -1384,7 +1376,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, //if( body==f[1] ){ // return f; //}else{ - return mkForAll( args, body, ipl ); + return mkForAll( args, body, qa ); //} } @@ -1490,27 +1482,29 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return n; } } - return mkForAll( args, body, Node::null() ); + QAttributes qa; + return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ +bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){ + bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef(); if( computeOption==COMPUTE_ELIM_SYMBOLS ){ return true; }else if( computeOption==COMPUTE_MINISCOPING ){ - return true; + return is_std; }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ - return options::aggressiveMiniscopeQuant(); + return options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ - return options::iteDtTesterSplitQuant() || options::condVarSplitQuant(); + return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std; }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant(); + return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ @@ -1521,70 +1515,62 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption } //general method for computing various rewrites -Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){ - if( f.getKind()==FORALL ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl; - std::vector< Node > args; - for( unsigned i=0; i new_conds; - n = computeProcessTerms( n, args, new_conds, f ); - if( !new_conds.empty() ){ - new_conds.push_back( n ); - n = NodeManager::currentNM()->mkNode( OR, new_conds ); - } - }else if( computeOption==COMPUTE_COND_SPLIT ){ - n = computeCondSplit( n, ipl ); - }else if( computeOption==COMPUTE_PRENEX ){ - n = computePrenex( n, args, true ); - }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - n = computeVarElimination( n, args, ipl ); - //}else if( computeOption==COMPUTE_CNF ){ - //n = computeCNF( n, args, defs, false ); - //ipl = Node::null(); - }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - std::vector< Node > conj; - computePurifyExpand( n, conj, args, ipl ); - if( !conj.empty() ){ - return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - }else{ - return f; - } +Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; + std::vector< Node > args; + for( unsigned i=0; i new_conds; + n = computeProcessTerms( n, args, new_conds, f, qa ); + if( !new_conds.empty() ){ + new_conds.push_back( n ); + n = NodeManager::currentNM()->mkNode( OR, new_conds ); } - Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; - if( f[1]==n && args.size()==f[0].getNumChildren() ){ + }else if( computeOption==COMPUTE_COND_SPLIT ){ + n = computeCondSplit( n, qa ); + }else if( computeOption==COMPUTE_PRENEX ){ + n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ + n = computeVarElimination( n, args, qa ); + //}else if( computeOption==COMPUTE_CNF ){ + //n = computeCNF( n, args, defs, false ); + //ipl = Node::null(); + }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ + std::vector< Node > conj; + computePurifyExpand( n, conj, args, qa ); + if( !conj.empty() ){ + return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + }else{ return f; + } + } + Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; + if( f[1]==n && args.size()==f[0].getNumChildren() ){ + return f; + }else{ + if( args.empty() ){ + return n; }else{ - if( args.empty() ){ - return n; - }else{ - std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); - children.push_back( n ); - if( !ipl.isNull() ){ - children.push_back( ipl ); - } - return NodeManager::currentNM()->mkNode(kind::FORALL, children ); + std::vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); + children.push_back( n ); + if( !qa.d_ipl.isNull() ){ + children.push_back( qa.d_ipl ); } + return NodeManager::currentNM()->mkNode(kind::FORALL, children ); } - }else{ - return f; } } @@ -1885,7 +1871,7 @@ Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, s } } -void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ) { +void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ) { if( body.getKind()==OR ){ Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl; std::map< int, std::vector< Node > > disj; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 47997f9a7..dbb28827c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -26,6 +26,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class QAttributes; + class QuantifiersRewriter { private: static int getPurifyIdLit2( Node n, std::map< Node, int >& visited ); @@ -37,7 +39,7 @@ public: static int getPurifyIdLit( Node n ); private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); + static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); @@ -52,21 +54,21 @@ private: std::map< Node, std::vector< int > >& var_parent ); static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, std::map< Node, std::vector< int > >& var_parent, int parentId ); - static Node computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ); + static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); + static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions - static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ); - static Node computeCondSplit( Node body, Node ipl ); + static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); + static Node computeCondSplit( Node body, QAttributes& qa ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); static Node computeSplit( Node f, std::vector< Node >& args, Node body ); - static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); + static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); - static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ); + static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ); private: enum{ COMPUTE_ELIM_SYMBOLS = 0, @@ -82,7 +84,7 @@ private: //COMPUTE_CNF, COMPUTE_LAST }; - static Node computeOperation( Node f, bool isNested, int computeOption ); + static Node computeOperation( Node f, int computeOption, QAttributes& qa ); public: static RewriteResponse preRewrite(TNode in); static RewriteResponse postRewrite(TNode in); @@ -90,7 +92,7 @@ public: static inline void shutdown() {} private: /** options */ - static bool doOperation( Node f, bool isNested, int computeOption ); + static bool doOperation( Node f, int computeOption, QAttributes& qa ); private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); public: diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a679ccfa8..284cae2e0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1787,69 +1787,107 @@ bool TermDb::isSygusConjectureAnnotation( Node ipl ){ return false; } +bool TermDb::isQuantElimAnnotation( Node ipl ) { + if( !ipl.isNull() ){ + for( unsigned i=0; igetRewriteEngine()==NULL ){ + Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; + } + //set rewrite engine as owner + d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); + } + if( d_qattr[q].isFunDef() ){ + Node f = d_qattr[q].d_fundef_f; + if( d_fun_defs.find( f )!=d_fun_defs.end() ){ + Message() << "Cannot define function " << f << " more than once." << std::endl; + exit( 1 ); + } + d_fun_defs[f] = true; + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() ); + } + if( d_qattr[q].d_sygus ){ + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + } + if( d_qattr[q].d_synthesis ){ + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + } +} + +void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; if( q.getNumChildren()==3 ){ + qa.d_ipl = q[2]; for( unsigned i=0; isetOwner( q, d_quantEngine->getFunDefEngine() ); + qa.d_fundef_f = q[2][i][0].getOperator(); } if( avar.getAttribute(SygusAttribute()) ){ //not necessarily nested existential //Assert( q[1].getKind()==NOT ); //Assert( q[1][0].getKind()==FORALL ); - Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; - d_qattr_sygus[q] = true; - if( d_quantEngine->getCegInstantiation()==NULL ){ - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + qa.d_sygus = true; } if( avar.getAttribute(SynthesisAttribute()) ){ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; - d_qattr_synthesis[q] = true; - if( d_quantEngine->getCegInstantiation()==NULL ){ - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + qa.d_synthesis = true; } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ - d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute()); - Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl; + qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); + Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; } if( avar.hasAttribute(RrPriorityAttribute()) ){ - d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute()); - Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl; + qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute()); + Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl; } + if( avar.getAttribute(QuantElimAttribute()) ){ + Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl; + qa.d_quant_elim = true; + //don't set owner, should happen naturally + } + if( avar.getAttribute(QuantElimPartialAttribute()) ){ + Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl; + qa.d_quant_elim = true; + qa.d_quant_elim_partial = true; + //don't set owner, should happen naturally + } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; Assert( i==0 ); - if( d_quantEngine->getRewriteEngine()==NULL ){ - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; - } - //set rewrite engine as owner - d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); + qa.d_rr = avar; } } } @@ -1857,69 +1895,85 @@ void TermDb::computeAttributes( Node q ) { } bool TermDb::isQAttrConjecture( Node q ) { - std::map< Node, bool >::iterator it = d_qattr_conjecture.find( q ); - if( it==d_qattr_conjecture.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return false; }else{ - return it->second; + return it->second.d_conjecture; } } bool TermDb::isQAttrAxiom( Node q ) { - std::map< Node, bool >::iterator it = d_qattr_axiom.find( q ); - if( it==d_qattr_axiom.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return false; }else{ - return it->second; + return it->second.d_axiom; } } bool TermDb::isQAttrFunDef( Node q ) { - std::map< Node, bool >::iterator it = d_qattr_fundef.find( q ); - if( it==d_qattr_fundef.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return false; }else{ - return it->second; + return it->second.isFunDef(); } } bool TermDb::isQAttrSygus( Node q ) { - std::map< Node, bool >::iterator it = d_qattr_sygus.find( q ); - if( it==d_qattr_sygus.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return false; }else{ - return it->second; + return it->second.d_sygus; } } bool TermDb::isQAttrSynthesis( Node q ) { - std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q ); - if( it==d_qattr_synthesis.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return false; }else{ - return it->second; + return it->second.d_synthesis; } } int TermDb::getQAttrQuantInstLevel( Node q ) { - std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q ); - if( it==d_qattr_qinstLevel.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return -1; }else{ - return it->second; + return it->second.d_qinstLevel; } } int TermDb::getQAttrRewriteRulePriority( Node q ) { - std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q ); - if( it==d_qattr_rr_priority.end() ){ + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ return -1; }else{ - return it->second; + return it->second.d_rr_priority; } } +bool TermDb::isQAttrQuantElim( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_quant_elim; + } +} +bool TermDb::isQAttrQuantElimPartial( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_quant_elim_partial; + } +} TermDbSygus::TermDbSygus(){ d_true = NodeManager::currentNM()->mkConst( true ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 0c4e94517..3fa0fbd29 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -99,6 +99,14 @@ typedef expr::Attribute SygusProxyAttribute; struct AbsTypeFunDefAttributeId {}; typedef expr::Attribute AbsTypeFunDefAttribute; +/** Attribute true for quantifiers that we are doing quantifier elimination on */ +struct QuantElimAttributeId {}; +typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute; + +/** Attribute true for quantifiers that we are doing partial quantifier elimination on */ +struct QuantElimPartialAttributeId {}; +typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute; + class QuantifiersEngine; namespace inst{ @@ -119,6 +127,26 @@ public: };/* class TermArgTrie */ +class QAttributes{ +public: + QAttributes() : d_conjecture(false), d_axiom(false), d_sygus(false), + d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} + ~QAttributes(){} + Node d_rr; + bool d_conjecture; + bool d_axiom; + Node d_fundef_f; + bool d_sygus; + bool d_synthesis; + int d_rr_priority; + int d_qinstLevel; + bool d_quant_elim; + bool d_quant_elim_partial; + Node d_ipl; + bool isRewriteRule() { return !d_rr.isNull(); } + bool isFunDef() { return !d_fundef_f.isNull(); } +}; + namespace fmcheck { class FullModelChecker; } @@ -440,15 +468,11 @@ public: //general queries concerning quantified formulas wrt modules static Node getFunDefHead( Node q ); /** get fun def body */ static Node getFunDefBody( Node q ); + /** is quant elim annotation */ + static bool isQuantElimAnnotation( Node ipl ); //attributes private: - std::map< Node, bool > d_qattr_conjecture; - std::map< Node, bool > d_qattr_axiom; - std::map< Node, bool > d_qattr_fundef; - std::map< Node, bool > d_qattr_sygus; - std::map< Node, bool > d_qattr_synthesis; - std::map< Node, int > d_qattr_rr_priority; - std::map< Node, int > d_qattr_qinstLevel; + std::map< Node, QAttributes > d_qattr; //record attributes void computeAttributes( Node q ); public: @@ -466,7 +490,12 @@ public: int getQAttrQuantInstLevel( Node q ); /** get rewrite rule priority */ int getQAttrRewriteRulePriority( Node q ); - + /** is quant elim */ + bool isQAttrQuantElim( Node q ); + /** is quant elim partial */ + bool isQAttrQuantElimPartial( Node q ); + /** compute quantifier attributes */ + static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */ class TermDbSygus { diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 86fc057ea..e3992f1a7 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -47,6 +47,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); + out.handleUserAttribute( "quant-elim", this ); + out.handleUserAttribute( "quant-elim-partial", this ); } TheoryQuantifiers::~TheoryQuantifiers() { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f3201bd60..ca8a09082 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -686,8 +686,7 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); - Node body = getInstantiation( f, vars, terms ); - //do virtual term substitution + Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution if( doVts ){ body = Rewriter::rewrite( body ); Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; @@ -811,7 +810,7 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ } -Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ){ +Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Node body; //process partial instantiation if necessary if( d_term_db->d_vars[q].size()!=vars.size() ){ @@ -842,18 +841,26 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std } } } + if( doVts ){ + //do virtual term substitution + body = Rewriter::rewrite( body ); + Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; + Node body_r = d_term_db->rewriteVtsSymbols( body ); + Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; + body = body_r; + } return body; } -Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m ){ +Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ std::vector< Node > vars; std::vector< Node > terms; computeTermVector( q, m, vars, terms ); - return getInstantiation( q, vars, terms ); + return getInstantiation( q, vars, terms, doVts ); } -Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms ) { - return getInstantiation( q, d_term_db->d_vars[q], terms ); +Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) { + return getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); } /* @@ -1109,11 +1116,11 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - it->second->getInstantiations( insts[it->first], it->first ); + it->second->getInstantiations( insts[it->first], it->first, this ); } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - it->second.getInstantiations( insts[it->first], it->first ); + it->second.getInstantiations( insts[it->first], it->first, this ); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 49c9eeff8..28fcbbc85 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -293,11 +293,11 @@ private: void flushLemmas(); public: /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ); + Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** get instantiation */ - Node getInstantiation( Node q, InstMatch& m ); + Node getInstantiation( Node q, InstMatch& m, bool doVts = false ); /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& terms ); + Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false ); /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); /** add lemma lem */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dcb3fec0a..8228861be 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1729,7 +1729,7 @@ void TheoryEngine::ppUnconstrainedSimp(vector& assertions) } -void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value) { +void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector& node_values, std::string str_value) { Trace("te-attr") << "set user attribute " << attr << " " << n << endl; if( d_attr_handle.find( attr )!=d_attr_handle.end() ){ for( size_t i=0; i node_values, std::string str_value); + void setUserAttribute(const std::string& attr, Node n, std::vector& node_values, std::string str_value); /** * Handle user attribute. -- 2.30.2