From f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Nov 2020 16:53:48 -0600 Subject: [PATCH] Enable new implementation of CEGQI based on nested quantifier elimination (#5477) This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation. The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly. Fixes #5365, fixes #5279, fixes #4849, fixes #4433. This PR also required fixes related to how quantifier elimination is computed. --- src/smt/quant_elim_solver.cpp | 28 +- src/smt/set_defaults.cpp | 13 +- src/smt/smt_engine.cpp | 8 - src/smt/smt_engine.h | 12 - .../quantifiers/cegqi/ceg_instantiator.cpp | 14 - .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 269 ++++-------------- .../quantifiers/cegqi/inst_strategy_cegqi.h | 49 +--- src/theory/quantifiers/inst_match_trie.cpp | 56 ++++ src/theory/quantifiers/inst_match_trie.h | 16 ++ src/theory/quantifiers/instantiate.cpp | 43 ++- .../sygus/ce_guided_single_inv.cpp | 2 + src/theory/quantifiers_engine.cpp | 24 -- src/theory/quantifiers_engine.h | 11 - src/theory/theory_engine.cpp | 25 -- src/theory/theory_engine.h | 13 +- test/regress/CMakeLists.txt | 4 + .../regress1/quantifiers/issue4433-nqe.smt2 | 9 + .../regress1/quantifiers/issue4849-nqe.smt2 | 7 + .../regress1/quantifiers/issue5279-nqe.smt2 | 5 + .../regress1/quantifiers/issue5365-nqe.smt2 | 14 + 20 files changed, 234 insertions(+), 388 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue4433-nqe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue4849-nqe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5279-nqe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5365-nqe.smt2 diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 38fd57790..59e9dfc9e 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" @@ -33,7 +34,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, bool doFull) { - Trace("smt-qe") << "Do quantifier elimination " << q << std::endl; + Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) { throw ModalException( @@ -73,6 +74,10 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // failed, return original return q; } + // must use original quantified formula to compute QE, which ensures that + // e.g. term formula removal is not run on the body. Notice that we assume + // that the (single) quantified formula is preprocessed, rewritten + // version of the input quantified formula q. std::vector inst_qs; te->getInstantiatedQuantifiedFormulas(inst_qs); Assert(inst_qs.size() <= 1); @@ -81,9 +86,24 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, { Node topq = inst_qs[0]; Assert(topq.getKind() == FORALL); - Trace("smt-qe") << "Get qe for " << topq << std::endl; - ret = te->getInstantiatedConjunction(topq); - Trace("smt-qe") << "Returned : " << ret << std::endl; + Trace("smt-qe") << "Get qe based on preprocessed quantified formula " + << topq << std::endl; + std::vector> insts; + te->getInstantiationTermVectors(topq, insts); + std::vector vars(ne[0].begin(), ne[0].end()); + std::vector conjs; + // apply the instantiation on the original body + for (const std::vector& inst : insts) + { + // note we do not convert to witness form here, since we could be + // an internal subsolver + Subs s; + s.add(vars, inst); + Node c = s.apply(ne[1].negate()); + conjs.push_back(c); + } + ret = nm->mkAnd(conjs); + Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) { ret = Rewriter::rewrite(ret.negate()); diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 0c2d06f1d..aaff29479 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -838,10 +838,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::cegqi.set(false); } // Do we need to track instantiations? - // Needed for sygus due to single invocation techniques. - if (options::cegqiNestedQE() - || (options::unsatCores() && !options::trackInstLemmas.wasSetByUser()) - || is_sygus) + if (options::unsatCores() && !options::trackInstLemmas.wasSetByUser()) { options::trackInstLemmas.set(true); } @@ -1188,13 +1185,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // only supported in pure arithmetic or pure BV options::cegqiNestedQE.set(false); } - // prenexing - if (options::cegqiNestedQE()) - { - // only complete with prenex = normal - options::prenexQuant.set(options::PrenexQuantMode::NORMAL); - } - else if (options::globalNegate()) + if (options::globalNegate()) { if (!options::prenexQuant.wasSetByUser()) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27bcdc036..2a0cde015 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1560,14 +1560,6 @@ void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) te->getInstantiatedQuantifiedFormulas(qs); } -void SmtEngine::getInstantiations(Node q, std::vector& insts) -{ - SmtScope smts(this); - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->getInstantiations(q, insts); -} - void SmtEngine::getInstantiationTermVectors( Node q, std::vector>& tvecs) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 6c721b9b0..1c83fa61f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -651,18 +651,6 @@ class CVC4_PUBLIC SmtEngine */ void getInstantiatedQuantifiedFormulas(std::vector& qs); - /** - * Get instantiations for quantified formula q. - * - * If q was a quantified formula that was instantiated on the last call to - * check-sat (i.e. q is returned as part of the vector in the method - * getInstantiatedQuantifiedFormulas above), then the list of instantiations - * of that formula that were generated are added to insts. - * - * In particular, if q is of the form forall x. P(x), then insts is a list - * of formulas of the form P(t1), ..., P(tn). - */ - void getInstantiations(Node q, std::vector& insts); /** * Get instantiation term vectors for quantified formula q. * diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 488a25316..59666f6fd 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -630,20 +630,6 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv) && vinst->allowModelValue(this, sf, pv, d_effort)) { -#ifdef CVC4_ASSERTIONS - // the instantiation strategy for quantified linear integer/real - // arithmetic with arbitrary quantifier nesting is "monotonic" as a - // consequence of Lemmas 5, 9 and Theorem 4 of Reynolds et al, "Solving - // Quantified Linear Arithmetic by Counterexample Guided Instantiation", - // FMSD 2017. We throw an assertion failure if we detect a case where the - // strategy was not monotonic. - if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH) - && d_qe->getLogicInfo().isLinear()) - { - Trace("cegqi-warn") << "Had to resort to model value." << std::endl; - Assert(false); - } -#endif Node mv = getModelValue( pv ); TermProperties pv_prop_m; Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 561817aa8..1a67a2b16 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -56,20 +56,20 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_cbqi_set_quant_inactive(false), d_incomplete_check(false), d_added_cbqi_lemma(qe->getUserContext()), - d_elim_quants(qe->getSatContext()), d_vtsCache(new VtsTermCache(qe)), - d_bv_invert(nullptr), - d_nested_qe_waitlist_size(qe->getUserContext()), - d_nested_qe_waitlist_proc(qe->getUserContext()) + d_bv_invert(nullptr) { - d_qid_count = 0; d_small_const = NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); d_check_vts_lemma_lc = false; if (options::cegqiBv()) { // if doing instantiation for BV, need the inverter class - d_bv_invert.reset(new quantifiers::BvInverter); + d_bv_invert.reset(new BvInverter); + } + if (options::cegqiNestedQE()) + { + d_nestedQe.reset(new NestedQe(qe->getUserContext())); } } @@ -177,16 +177,6 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) if( doCbqi( quants[i] ) ){ registerCbqiLemma( quants[i] ); } - if( options::cegqiNestedQE() ){ - //record these as counterexample quantifiers - QAttributes qa; - QuantAttributes::computeQuantAttributes( quants[i], qa ); - if( !qa.d_qid_num.isNull() ){ - d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; - d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; - Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; - } - } } } // The decision strategy for this quantified formula ensures that its @@ -226,7 +216,6 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - Assert(hasAddedCbqiLemma(q)); if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl; @@ -242,20 +231,6 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; d_active_quant.erase( q ); - d_elim_quants.insert( q ); - Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; - //process from waitlist - while( d_nested_qe_waitlist_proc[q]= 0); - Assert(index < (int)d_nested_qe_waitlist[q].size()); - Node nq = d_nested_qe_waitlist[q][index]; - Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); - Node dqelem = nq.eqNode( nqeqn ); - Trace("cegqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; - d_quantEngine->getOutputChannel().lemma( dqelem ); - d_nested_qe_waitlist_proc[q] = index + 1; - } } } }else{ @@ -312,14 +287,10 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ Node q = it->first; Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; - if( d_nested_qe.find( q )==d_nested_qe.end() ){ - process( q, e, ee ); - if( d_quantEngine->inConflict() ){ - break; - } - }else{ - Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; - Assert(false); + process(q, e, ee); + if (d_quantEngine->inConflict()) + { + break; } } if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ @@ -355,55 +326,6 @@ bool InstStrategyCegqi::checkCompleteFor(Node q) } } -Node InstStrategyCegqi::getIdMarkedQuantNode(Node n, - std::map& visited) -{ - std::map< Node, Node >::iterator it = visited.find( n ); - if( it==visited.end() ){ - Node ret = n; - if( n.getKind()==FORALL ){ - QAttributes qa; - QuantAttributes::computeQuantAttributes( n, qa ); - if( qa.d_qid_num.isNull() ){ - std::vector< Node > rc; - rc.push_back( n[0] ); - rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); - Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); - QuantIdNumAttribute ida; - avar.setAttribute(ida,d_qid_count); - d_qid_count++; - std::vector< Node > iplc; - iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); - if( n.getNumChildren()==3 ){ - for( unsigned i=0; imkNode( INST_PATTERN_LIST, iplc ) ); - ret = NodeManager::currentNM()->mkNode( FORALL, rc ); - } - }else if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - void InstStrategyCegqi::checkOwnership(Node q) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ @@ -417,34 +339,13 @@ void InstStrategyCegqi::checkOwnership(Node q) void InstStrategyCegqi::preRegisterQuantifier(Node q) { - // mark all nested quantifiers with id - if (options::cegqiNestedQE()) + if (doCbqi(q)) { - if( d_quantEngine->getOwner(q)==this ) + if (processNestedQe(q, true)) { - std::map visited; - Node mq = getIdMarkedQuantNode(q[1], visited); - if (mq != q[1]) - { - // do not do cbqi, we are reducing this quantified formula to a marked - // one - d_do_cbqi[q] = CEG_UNHANDLED; - // instead do reduction - std::vector qqc; - qqc.push_back(q[0]); - qqc.push_back(mq); - if (q.getNumChildren() == 3) - { - qqc.push_back(q[2]); - } - Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc); - Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq); - Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; - d_quantEngine->addLemma(mlem); - } + // will process using nested quantifier elimination + return; } - } - if( doCbqi( q ) ){ // get the instantiator if (options::cegqiPreRegInst()) { @@ -470,10 +371,6 @@ TrustNode InstStrategyCegqi::rewriteInstantiation(Node q, inst = d_vtsCache->rewriteVtsSymbols(inst); Trace("quant-vts-debug") << "...got " << inst << std::endl; } - if (options::cegqiNestedQE()) - { - inst = doNestedQE(q, terms, inst, doVts); - } if (prevInst != inst) { // not proof producing yet @@ -487,110 +384,6 @@ InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const return d_irew.get(); } -Node InstStrategyCegqi::doNestedQENode( - Node q, Node ceq, Node n, std::vector& inst_terms, bool doVts) -{ - // there is a nested quantified formula (forall y. nq[y,x]) such that - // q is (forall y. nq[y,t]) for ground terms t, - // ceq is (forall y. nq[y,e]) for CE variables e. - // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e]. - // in this case, q is equivalent to the quantifier-free formula C[t]. - if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ - d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); - Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl; - Trace("cegqi-nqe") << " " << ceq << std::endl; - Trace("cegqi-nqe") << " " << d_nested_qe[ceq] << std::endl; - //should not contain quantifiers - Assert(!expr::hasClosure(d_nested_qe[ceq])); - } - Assert(d_quantEngine->getTermUtil()->d_inst_constants[q].size() - == inst_terms.size()); - //replace inst constants with instantiation - Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), - d_quantEngine->getTermUtil()->d_inst_constants[q].end(), - inst_terms.begin(), inst_terms.end() ); - if( doVts ){ - //do virtual term substitution - ret = Rewriter::rewrite( ret ); - ret = d_vtsCache->rewriteVtsSymbols(ret); - } - Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl; - Trace("cegqi-nqe") << " " << n << std::endl; - Trace("cegqi-nqe") << " " << ret << std::endl; - return ret; -} - -Node InstStrategyCegqi::doNestedQERec(Node q, - Node n, - std::map& visited, - std::vector& inst_terms, - bool doVts) -{ - if( visited.find( n )==visited.end() ){ - Node ret = n; - if( n.getKind()==FORALL ){ - QAttributes qa; - QuantAttributes::computeQuantAttributes( n, qa ); - if( !qa.d_qid_num.isNull() ){ - //if it has an id, check whether we have done quantifier elimination for this id - std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); - if( it!=d_id_to_ce_quant.end() ){ - Node ceq = it->second; - bool doNestedQe = d_elim_quants.contains( ceq ); - if( doNestedQe ){ - ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); - }else{ - Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl; - Node nr = Rewriter::rewrite( n ); - Trace("cegqi-nqe") << " " << ceq << std::endl; - Trace("cegqi-nqe") << " " << nr << std::endl; - int wlsize = d_nested_qe_waitlist_size[ceq] + 1; - d_nested_qe_waitlist_size[ceq] = wlsize; - if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ - d_nested_qe_waitlist[ceq][wlsize] = nr; - }else{ - d_nested_qe_waitlist[ceq].push_back( nr ); - } - d_nested_qe_info[nr].d_q = q; - d_nested_qe_info[nr].d_inst_terms.clear(); - d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); - d_nested_qe_info[nr].d_doVts = doVts; - //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. - Assert(!options::cegqiInnermost()); - } - } - } - }else if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - }else{ - return n; - } -} - -Node InstStrategyCegqi::doNestedQE(Node q, - std::vector& inst_terms, - Node lem, - bool doVts) -{ - std::map< Node, Node > visited; - return doNestedQERec( q, lem, visited, inst_terms, doVts ); -} - void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { // must register with the instantiator @@ -631,6 +424,13 @@ bool InstStrategyCegqi::doCbqi(Node q) } void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { + // If we are doing nested quantifier elimination, check if q was already + // processed. + if (processNestedQe(q, false)) + { + // don't need to process this, since it has been reduced + return; + } if( e==0 ){ CegInstantiator * cinst = getInstantiator( q ); Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; @@ -743,6 +543,33 @@ void InstStrategyCegqi::presolve() { } } +bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) +{ + if (d_nestedQe != nullptr) + { + if (isPreregister) + { + // If at preregister, we are done if we have nested quantification. + // We will process nested quantification. + return NestedQe::hasNestedQuantification(q); + } + // if not a preregister, we process, which may trigger quantifier + // elimination in subsolvers. + std::vector lems; + if (d_nestedQe->process(q, lems)) + { + // add lemmas to process + for (const Node& lem : lems) + { + d_quantEngine->addLemma(lem); + } + // don't need to process this, since it has been reduced + return true; + } + } + return false; +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 0a3472968..2ca232699 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -21,6 +21,7 @@ #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/nested_qe.h" #include "theory/quantifiers/cegqi/vts_term_cache.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" @@ -143,8 +144,6 @@ class InstStrategyCegqi : public QuantifiersModule bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; - /** whether we have added cbqi lemma */ - NodeSet d_elim_quants; /** parent guards */ std::map< Node, std::vector< Node > > d_parent_quant; std::map< Node, std::vector< Node > > d_children_quant; @@ -193,6 +192,14 @@ class InstStrategyCegqi : public QuantifiersModule void registerCounterexampleLemma(Node q, Node lem); /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } + /** + * Return true if q can be processed with nested quantifier elimination. + * This may add a lemma on the output channel of quantifiers engine if so. + * + * @param q The quantified formula to process + * @param isPreregister Whether this method is being called at preregister. + */ + bool processNestedQe(Node q, bool isPreregister); /** process functions */ void process(Node q, Theory::Effort effort, int e); /** @@ -204,44 +211,10 @@ class InstStrategyCegqi : public QuantifiersModule Node getCounterexampleLiteral(Node q); /** map from universal quantifiers to their counterexample literals */ std::map d_ce_lit; - - //for identification - uint64_t d_qid_count; - //nested qe map - std::map< Node, Node > d_nested_qe; - //mark ids on quantifiers - Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); - // id to ce quant - std::map< Node, Node > d_id_to_ce_quant; - std::map< Node, Node > d_ce_quant_to_id; - //do nested quantifier elimination recursive - Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); - Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); - //elimination information (for delayed elimination) - class NestedQEInfo { - public: - NestedQEInfo() : d_doVts(false){} - ~NestedQEInfo(){} - Node d_q; - std::vector< Node > d_inst_terms; - bool d_doVts; - }; - std::map< Node, NestedQEInfo > d_nested_qe_info; - NodeIntMap d_nested_qe_waitlist_size; - NodeIntMap d_nested_qe_waitlist_proc; - std::map< Node, std::vector< Node > > d_nested_qe_waitlist; - - /** Do nested quantifier elimination. - * - * This rewrites the quantified formulas in inst based on nested quantifier - * elimination. In this method, inst is the instantiation of quantified - * formula q for the vector terms. The flag doVts indicates whether we must - * apply virtual term substitution (if terms contains virtual terms). - */ - Node doNestedQE(Node q, std::vector& terms, Node inst, bool doVts); + /** The nested quantifier elimination utility */ + std::unique_ptr d_nestedQe; }; - } } } diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 759fa026b..aaf7cb4bc 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -256,6 +256,32 @@ void InstMatchTrie::getExplanationForInstLemmas( } } +void InstMatchTrie::getInstantiations( + Node q, std::vector>& insts) const +{ + std::vector terms; + getInstantiations(q, insts, terms); +} + +void InstMatchTrie::getInstantiations(Node q, + std::vector>& insts, + std::vector& terms) const +{ + if (terms.size() == q[0].getNumChildren()) + { + insts.push_back(terms); + } + else + { + for (const std::pair& d : d_data) + { + terms.push_back(d.first); + d.second.getInstantiations(q, insts, terms); + terms.pop_back(); + } + } +} + CDInstMatchTrie::~CDInstMatchTrie() { for (std::pair& d : d_data) @@ -517,6 +543,36 @@ void CDInstMatchTrie::getExplanationForInstLemmas( } } +void CDInstMatchTrie::getInstantiations( + Node q, std::vector>& insts) const +{ + std::vector terms; + getInstantiations(q, insts, terms); +} + +void CDInstMatchTrie::getInstantiations(Node q, + std::vector>& insts, + std::vector& terms) const +{ + if (!d_valid.get()) + { + // do nothing + } + else if (terms.size() == q[0].getNumChildren()) + { + insts.push_back(terms); + } + else + { + for (const std::pair& d : d_data) + { + terms.push_back(d.first); + d.second->getInstantiations(q, insts, terms); + terms.pop_back(); + } + } +} + } /* CVC4::theory::inst namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 67a942c57..a63954838 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -125,6 +125,10 @@ class InstMatchTrie Node lem, ImtIndexOrder* imtio = NULL, unsigned index = 0); + /** + * Adds the instantiations for q into insts. + */ + void getInstantiations(Node q, std::vector>& insts) const; /** get instantiations * @@ -174,6 +178,10 @@ class InstMatchTrie std::map d_data; private: + /** Helper for getInstantiations.*/ + void getInstantiations(Node q, + std::vector>& insts, + std::vector& terms) const; /** helper for print * terms accumulates the path we are on in the trie. */ @@ -293,6 +301,10 @@ class CDInstMatchTrie std::vector& m, Node lem, unsigned index = 0); + /** + * Adds the instantiations for q into insts. + */ + void getInstantiations(Node q, std::vector>& insts) const; /** get instantiations * @@ -338,6 +350,10 @@ class CDInstMatchTrie } private: + /** Helper for getInstantiations.*/ + void getInstantiations(Node q, + std::vector>& insts, + std::vector& terms) const; /** the data */ std::map d_data; /** is valid */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 8549b1eae..fb622452e 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -714,14 +714,39 @@ bool Instantiate::getUnsatCoreLemmas(std::vector& active_lemmas) void Instantiate::getInstantiationTermVectors( Node q, std::vector >& tvecs) { - std::vector lemmas; - getInstantiations(q, lemmas); - std::map quant; - std::map > tvec; - getExplanationForInstLemmas(lemmas, quant, tvec); - for (std::pair >& t : tvec) + // if track instantiations is true, we use the instantiation + explanation + // methods for doing minimization based on unsat cores. + if (options::trackInstLemmas()) + { + std::vector lemmas; + getInstantiations(q, lemmas); + std::map quant; + std::map > tvec; + getExplanationForInstLemmas(lemmas, quant, tvec); + for (std::pair >& t : tvec) + { + tvecs.push_back(t.second); + } + return; + } + + if (options::incrementalSolving()) + { + std::map::const_iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + it->second->getInstantiations(q, tvecs); + } + } + else { - tvecs.push_back(t.second); + std::map::const_iterator it = + d_inst_match_trie.find(q); + if (it != d_inst_match_trie.end()) + { + it->second.getInstantiations(q, tvecs); + } } } @@ -730,14 +755,14 @@ void Instantiate::getInstantiationTermVectors( { if (options::incrementalSolving()) { - for (std::pair& t : d_c_inst_match_trie) + for (const auto& t : d_c_inst_match_trie) { getInstantiationTermVectors(t.first, insts[t.first]); } } else { - for (std::pair& t : d_inst_match_trie) + for (const auto& t : d_inst_match_trie) { getInstantiationTermVectors(t.first, insts[t.first]); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index ac7d6efc7..e9e15ef3b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -241,6 +241,8 @@ bool CegSingleInv::solve() Node body = siq[1]; for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++) { + // note we do not convert to witness form here, since we could be + // an internal subsolver std::vector& inst = d_inst[i]; Trace("sygus-si") << " Instantiation: " << inst << std::endl; // instantiation should have same arity since we are not allowed to diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7f0b46c99..297f11690 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1013,10 +1013,6 @@ void QuantifiersEngine::flushLemmas(){ } } -bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) { - return d_instantiate->getUnsatCoreLemmas(active_lemmas); -} - void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { d_instantiate->getInstantiationTermVectors(q, tvecs); } @@ -1025,14 +1021,6 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector d_instantiate->getInstantiationTermVectors(insts); } -void QuantifiersEngine::getExplanationForInstLemmas( - const std::vector& lems, - std::map& quant, - std::map >& tvec) -{ - d_instantiate->getExplanationForInstLemmas(lems, quant, tvec); -} - void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool printed = false; // print the skolemizations @@ -1066,18 +1054,6 @@ void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& d_instantiate->getInstantiatedQuantifiedFormulas(qs); } -void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { - d_instantiate->getInstantiations(insts); -} - -void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) { - d_instantiate->getInstantiations(q, insts); -} - -Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { - return d_instantiate->getInstantiatedConjunction(q); -} - QuantifiersEngine::Statistics::Statistics() : d_time("theory::QuantifiersEngine::time"), d_qcf_time("theory::QuantifiersEngine::time_qcf"), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e266e2058..8dcaf668f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -278,22 +278,11 @@ public: void printSynthSolution(std::ostream& out); /** get list of quantified formulas that were instantiated */ void getInstantiatedQuantifiedFormulas(std::vector& qs); - /** get instantiations */ - void getInstantiations(Node q, std::vector& insts); - void getInstantiations(std::map >& insts); /** get instantiation term vectors */ void getInstantiationTermVectors(Node q, std::vector >& tvecs); void getInstantiationTermVectors( std::map > >& insts); - /** get instantiated conjunction */ - Node getInstantiatedConjunction(Node q); - /** get unsat core lemmas */ - bool getUnsatCoreLemmas(std::vector& active_lemmas); - /** get explanation for instantiation lemmas */ - void getExplanationForInstLemmas(const std::vector& lems, - std::map& quant, - std::map >& tvec); /** get synth solutions * diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d54538049..dc59cbbf5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1215,14 +1215,6 @@ void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) } } -void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiations( q, insts ); - }else{ - Assert(false); - } -} - void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( q, tvecs ); @@ -1231,14 +1223,6 @@ void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector } } -void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiations( insts ); - }else{ - Assert(false); - } -} - void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( insts ); @@ -1247,15 +1231,6 @@ void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std } } -Node TheoryEngine::getInstantiatedConjunction( Node q ) { - if( d_quantEngine ){ - return d_quantEngine->getInstantiatedConjunction( q ); - }else{ - Assert(false); - return Node::null(); - } -} - TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ee3611a53..1412d7464 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -686,22 +686,13 @@ class TheoryEngine { /** * Get instantiation methods - * first inputs forall x.q[x] and returns ( q[a], ..., q[z] ) - * second inputs forall x.q[x] and returns ( a, ..., z ) - * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) + * the first given forall x.q[x] returns ( a, ..., z ) + * the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) * , ... , forall x.qn[x] -> ( qn[a]...qn[z] ) */ - void getInstantiations( Node q, std::vector< Node >& insts ); void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); - void getInstantiations( std::map< Node, std::vector< Node > >& insts ); void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); - /** - * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. - * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q - */ - Node getInstantiatedConjunction( Node q ); - /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9935adf59..7e87c337a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1606,9 +1606,13 @@ set(regress_1_tests regress1/quantifiers/issue4062-cegqi-aux.smt2 regress1/quantifiers/issue4243-prereg-inc.smt2 regress1/quantifiers/issue4290-cegqi-r.smt2 + regress1/quantifiers/issue4433-nqe.smt2 regress1/quantifiers/issue4620-erq-witness-unsound.smt2 regress1/quantifiers/issue4685-wrewrite.smt2 + regress1/quantifiers/issue4849-nqe.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 + regress1/quantifiers/issue5279-nqe.smt2 + regress1/quantifiers/issue5365-nqe.smt2 regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 diff --git a/test/regress/regress1/quantifiers/issue4433-nqe.smt2 b/test/regress/regress1/quantifiers/issue4433-nqe.smt2 new file mode 100644 index 000000000..1ab35a43f --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4433-nqe.smt2 @@ -0,0 +1,9 @@ +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status unsat) +(assert + (forall ((a Int) (b Int)) + (xor (xor (= a 0) (= b 0)) + (forall ((c Int)) + (= (ite (= a 0) 0 1) (ite (= c 0) 0 1)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 new file mode 100644 index 000000000..dd7a22e39 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cegqi-nested-qe -q +; EXPECT: sat +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status sat) +(assert (forall ((a Int)) (exists ((b Int)) (= (ite (= a 0) 0 1) (ite (= b 0) 0 1))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5279-nqe.smt2 b/test/regress/regress1/quantifiers/issue5279-nqe.smt2 new file mode 100644 index 000000000..b87f36ebe --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5279-nqe.smt2 @@ -0,0 +1,5 @@ +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status unsat) +(assert (forall ((a Int) (b Bool)) (= a (ite b 0 1)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5365-nqe.smt2 b/test/regress/regress1/quantifiers/issue5365-nqe.smt2 new file mode 100644 index 000000000..c19cb6a3f --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5365-nqe.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --cegqi-nested-qe -q +; EXPECT: sat +(set-logic BV) +(set-option :cegqi-nested-qe true) +(set-info :status sat) +(assert + (exists ((a (_ BitVec 32))) + (forall ((b (_ BitVec 32)) (c (_ BitVec 32))) + (exists ((d (_ BitVec 32)) (e (_ BitVec 32))) + (forall ((g (_ BitVec 32))) + (exists ((f (_ BitVec 32))) + (=> (= (_ bv0 32) a) + (= (bvadd e g) (bvand d f) b c)))))))) +(check-sat) -- 2.30.2