From 87fbe99f81b9c72e9acb34e0fae61f56164535c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Mar 2018 15:56:16 -0600 Subject: [PATCH] Optimization for sygus streaming mode (#1636) --- .../sygus/ce_guided_conjecture.cpp | 109 +++++++++++------- .../quantifiers/sygus/ce_guided_conjecture.h | 6 + 2 files changed, 72 insertions(+), 43 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 3e71eedad..1dd4dcbeb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -290,16 +290,14 @@ void CegConjecture::doCheck(std::vector& lems) } } - std::vector< Node > ic; - ic.push_back( d_quant.negate() ); - //immediately skolemize inner existentials Node instr = Rewriter::rewrite(inst); + Node lem; if (instr.getKind() == NOT && instr[0].getKind() == FORALL) { if (constructed_cand) { - ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate()); + lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate(); } if (sk_refine) { @@ -312,7 +310,7 @@ void CegConjecture::doCheck(std::vector& lems) if (constructed_cand) { // use the instance itself - ic.push_back(instr); + lem = instr; } if (sk_refine) { @@ -321,8 +319,8 @@ void CegConjecture::doCheck(std::vector& lems) d_ce_sk.push_back(Node::null()); } } - if( constructed_cand ){ - Node lem = nm->mkNode(OR, ic); + if (!lem.isNull()) + { lem = Rewriter::rewrite( lem ); //eagerly unfold applications of evaluation function if( options::sygusDirectEval() ){ @@ -330,9 +328,25 @@ void CegConjecture::doCheck(std::vector& lems) std::map< Node, Node > visited_n; lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n ); } - lem = getStreamGuardedLemma(lem); - lems.push_back( lem ); + // record the instantiation + // this is used for remembering the solution recordInstantiation(candidate_values); + if (lem.isConst() && !lem.getConst() && options::sygusStream()) + { + // short circuit the check + // instead, we immediately print the current solution. + // this saves us from introducing a check lemma and a new guard. + printAndContinueStream(); + } + else + { + // This is the "verification lemma", which states + // either this conjecture does not have a solution, or candidate_values + // is a solution for this conjecture. + lem = nm->mkNode(OR, d_quant.negate(), lem); + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); + } } } @@ -479,43 +493,13 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { return curr_stream_guard; }else{ if( !value ){ - Assert(d_master != nullptr); Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl; - // we have generated a solution, print it - // get the current output stream - // this output stream should coincide with wherever --dump-synth is output on - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - printSynthSolution( *nodeManagerOptions.getOut(), false ); // need to make the next stream guard needs_new_stream_guard = true; - - // We will not refine the current candidate solution since it is a solution - // thus, we clear information regarding the current refinement - d_ce_sk.clear(); - // However, we need to exclude the current solution using an - // explicit refinement - // so that we proceed to the next solution. - std::vector terms; - d_master->getTermList(d_candidates, terms); - Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl; - std::vector< Node > exp; - for (const Node& cprog : terms) - { - Node sol = cprog; - if( !d_cinfo[cprog].d_inst.empty() ){ - sol = d_cinfo[cprog].d_inst.back(); - // add to explanation of exclusion - d_qe->getTermDatabaseSygus() - ->getExplain() - ->getExplanationForConstantEquality(cprog, sol, exp); - } - Trace("cegqi-debug") << " " << cprog << " -> " << sol << std::endl; - } - Assert( !exp.empty() ); - Node exc_lem = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ); - exc_lem = exc_lem.negate(); - Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl; - d_qe->getOutputChannel().lemma( exc_lem ); + // the guard has propagated false, indicating that a verify + // lemma was unsatisfiable. Hence, the previous candidate is + // an actual solution. We print and continue the stream. + printAndContinueStream(); } } } @@ -539,6 +523,45 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { return Node::null(); } +void CegConjecture::printAndContinueStream() +{ + Assert(d_master != nullptr); + // we have generated a solution, print it + // get the current output stream + // this output stream should coincide with wherever --dump-synth is output on + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + printSynthSolution(*nodeManagerOptions.getOut(), false); + + // We will not refine the current candidate solution since it is a solution + // thus, we clear information regarding the current refinement + d_ce_sk.clear(); + // However, we need to exclude the current solution using an explicit + // blocking clause, so that we proceed to the next solution. + std::vector terms; + d_master->getTermList(d_candidates, terms); + std::vector exp; + for (const Node& cprog : terms) + { + Node sol = cprog; + if (!d_cinfo[cprog].d_inst.empty()) + { + sol = d_cinfo[cprog].d_inst.back(); + // add to explanation of exclusion + d_qe->getTermDatabaseSygus() + ->getExplain() + ->getExplanationForConstantEquality(cprog, sol, exp); + } + } + Assert(!exp.empty()); + Node exc_lem = exp.size() == 1 + ? exp[0] + : NodeManager::currentNM()->mkNode(kind::AND, exp); + exc_lem = exc_lem.negate(); + Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " + << exc_lem << std::endl; + d_qe->getOutputChannel().lemma(exc_lem); +} + void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) { Trace("cegqi-debug") << "Printing synth solution..." << std::endl; Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() ); diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 8ab871d08..215a4d161 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -226,6 +226,12 @@ private: * returned by getCurrentStreamGuard, otherwise this returns n. */ Node getStreamGuardedLemma(Node n) const; + /** + * Prints the current synthesis solution to the output stream indicated by + * the Options object, send a lemma blocking the current solution to the + * output channel. + */ + void printAndContinueStream(); //-------------------------------- end sygus stream //-------------------------------- non-syntax guided (deprecated) /** Whether we are syntax-guided (e.g. was the input in SyGuS format). -- 2.30.2