From: Andrew Reynolds Date: Thu, 1 Feb 2018 19:52:34 +0000 (-0600) Subject: Add interface in sygus to get synthesis solution Nodes (#1552) X-Git-Tag: cvc5-1.0.0~5339 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64192c63a0011e4737eec2d27cf4deabf74d6c0a;p=cvc5.git Add interface in sygus to get synthesis solution Nodes (#1552) --- diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 74d5cef47..cc00599d3 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -560,67 +560,22 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { 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() ); - for( unsigned i=0; igetSolution( i, tn, status, true ); - if( !sol.isNull() ){ - sol = sol.getKind()==LAMBDA ? sol[1] : sol; - } - }else{ - Node cprog = getCandidate( i ); - if( !d_cinfo[cprog].d_inst.empty() ){ - // the solution is just the last instantiated term - sol = d_cinfo[cprog].d_inst.back(); - status = 1; - - //check if there was a template - Node sf = d_quant[0][i]; - Node templ = d_ceg_si->getTemplate( sf ); - if( !templ.isNull() ){ - Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl; - // if it was not embedded into the grammar - if( !options::sygusTemplEmbedGrammar() ){ - TNode templa = d_ceg_si->getTemplateArg( sf ); - // make the builtin version of the full solution - TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - TNode tsol = sol; - sol = templ.substitute( templa, tsol ); - Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; - sol = Rewriter::rewrite( sol ); - Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; - // now, reconstruct to the syntax - sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); - sol = sol.getKind()==LAMBDA ? sol[1] : sol; - Trace("cegqi-inv-debug") << "Reconstructed to syntax : " << sol << std::endl; - }else{ - Trace("cegqi-inv-debug") << "...was embedding into grammar." << std::endl; - } - }else{ - Trace("cegqi-inv-debug") << sf << " did not use template" << std::endl; - } - }else{ - Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl; - } - } - if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){ + std::vector sols; + std::vector statuses; + getSynthSolutionsInternal(sols, statuses, singleInvocation); + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node sol = sols[i]; + if (!sol.isNull()) + { + Node prog = d_embed_quant[0][i]; + int status = statuses[i]; + TypeNode tn = prog.getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + std::stringstream ss; + ss << prog; + std::string f(ss.str()); + f.erase(f.begin()); out << "(define-fun " << f << " "; if( dt.getSygusVarList().isNull() ){ out << "() "; @@ -695,6 +650,122 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation } } +void CegConjecture::getSynthSolutions(std::map& sol_map, + bool singleInvocation) +{ + NodeManager* nm = NodeManager::currentNM(); + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); + std::vector sols; + std::vector statuses; + getSynthSolutionsInternal(sols, statuses, singleInvocation); + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node sol = sols[i]; + int status = statuses[i]; + // get the builtin solution + Node bsol = sol; + if (status != 0) + { + // convert sygus to builtin here + bsol = sygusDb->sygusToBuiltin(sol, sol.getType()); + } + // convert to lambda + TypeNode tn = d_embed_quant[0][i].getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Node bvl = Node::fromExpr(dt.getSygusVarList()); + if (!bvl.isNull()) + { + bsol = nm->mkNode(LAMBDA, bvl, bsol); + } + // store in map + Node fvar = d_quant[0][i]; + Assert(fvar.getType() == bsol.getType()); + sol_map[fvar] = bsol; + } +} + +void CegConjecture::getSynthSolutionsInternal(std::vector& sols, + std::vector& statuses, + bool singleInvocation) +{ + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node prog = d_embed_quant[0][i]; + Trace("cegqi-debug") << " get solution for " << prog << std::endl; + TypeNode tn = prog.getType(); + Assert(tn.isDatatype()); + // get the solution + Node sol; + int status = -1; + if (singleInvocation) + { + Assert(d_ceg_si != NULL); + sol = d_ceg_si->getSolution(i, tn, status, true); + if (!sol.isNull()) + { + sol = sol.getKind() == LAMBDA ? sol[1] : sol; + } + } + else + { + Node cprog = getCandidate(i); + if (!d_cinfo[cprog].d_inst.empty()) + { + // the solution is just the last instantiated term + sol = d_cinfo[cprog].d_inst.back(); + status = 1; + + // check if there was a template + Node sf = d_quant[0][i]; + Node templ = d_ceg_si->getTemplate(sf); + if (!templ.isNull()) + { + Trace("cegqi-inv-debug") + << sf << " used template : " << templ << std::endl; + // if it was not embedded into the grammar + if (!options::sygusTemplEmbedGrammar()) + { + TNode templa = d_ceg_si->getTemplateArg(sf); + // make the builtin version of the full solution + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); + sol = sygusDb->sygusToBuiltin(sol, sol.getType()); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol + << ", type : " << sol.getType() << std::endl; + TNode tsol = sol; + sol = templ.substitute(templa, tsol); + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite(sol); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + // now, reconstruct to the syntax + sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); + sol = sol.getKind() == LAMBDA ? sol[1] : sol; + Trace("cegqi-inv-debug") + << "Reconstructed to syntax : " << sol << std::endl; + } + else + { + Trace("cegqi-inv-debug") + << "...was embedding into grammar." << std::endl; + } + } + else + { + Trace("cegqi-inv-debug") + << sf << " did not use template" << std::endl; + } + } + else + { + Trace("cegqi-warn") << "WARNING : No recorded instantiations for " + "syntax-guided solution!" + << std::endl; + } + } + sols.push_back(sol); + statuses.push_back(status); + } +} + Node CegConjecture::getSymmetryBreakingPredicate( Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) { diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index e57b545e6..011967ca1 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -79,8 +79,25 @@ public: * singleInvocation is whether the solution was found by single invocation techniques. */ //-------------------------------end for counterexample-guided check/refine - + /** + * prints the synthesis solution to output stream out. + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ void printSynthSolution( std::ostream& out, bool singleInvocation ); + /** get synth solutions + * + * This returns a map from function-to-synthesize variables to their + * builtin solution, which has the same type. For example, for synthesis + * conjecture exists f. forall x. f( x )>x, this function may return the map + * containing the entry: + * f -> (lambda x. x+1) + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ + void getSynthSolutions(std::map& sol_map, bool singleInvocation); /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */ Node getGuard(); /** is ground */ @@ -184,6 +201,27 @@ private: d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] ); } } + /** get synth solutions internal + * + * This function constructs the body of solutions for all + * functions-to-synthesize in this conjecture and stores them in sols, in + * order. For each solution added to sols, we add an integer indicating what + * kind of solution n is, where if sols[i] = n, then + * if status[i] = 0: n is the (builtin term) corresponding to the solution, + * if status[i] = 1: n is the sygus representation of the solution. + * We store builtin versions under some conditions (such as when the sygus + * grammar is being ignored). + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + * + * For example, for conjecture exists fg. forall x. f(x)>g(x), this function + * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is + * the sygus datatype constructor corresponding to variable x. + */ + void getSynthSolutionsInternal(std::vector& sols, + std::vector& status, + bool singleInvocation); //-------------------------------- sygus stream /** the streaming guards for sygus streaming mode */ std::vector< Node > d_stream_guards; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index b54ce4805..dc359d252 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -310,14 +310,28 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto } void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj->isAssigned() ){ - // print the conjecture + if( d_conj->isAssigned() ) + { d_conj->printSynthSolution( out, d_last_inst_si ); - }else{ + } + else + { Assert( false ); } } +void CegInstantiation::getSynthSolutions(std::map& sol_map) +{ + if (d_conj->isAssigned()) + { + d_conj->getSynthSolutions(sol_map, d_last_inst_si); + } + else + { + Assert(false); + } +} + void CegInstantiation::preregisterAssertion( Node n ) { //check if it sygus conjecture if( QuantAttributes::checkSygusConjecture( n ) ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 86f0c4c9f..691363311 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -55,6 +55,17 @@ public: std::string identify() const { return "CegInstantiation"; } /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize + * with their solutions, for all active conjectures (currently just the one + * assigned to d_conj). This should be called immediately after the solver + * answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * CegConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map& sol_map); /** preregister assertion (before rewrite) */ void preregisterAssertion( Node n ); public: