From: Andrew Reynolds Date: Tue, 15 Dec 2020 21:19:08 +0000 (-0600) Subject: Consolidate basic sygus utilities regarding sygus conjectures (#5421) X-Git-Tag: cvc5-1.0.0~2442 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c4598683e4edd217ed524d47c68a053b6881f4c;p=cvc5.git Consolidate basic sygus utilities regarding sygus conjectures (#5421) This is required for new work on generalizing CAV 2015 single invocation techniques. It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4657449f8..d9c38ec65 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -776,6 +776,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/sygus_unif_rl.h theory/quantifiers/sygus/sygus_unif_strat.cpp theory/quantifiers/sygus/sygus_unif_strat.h + theory/quantifiers/sygus/sygus_utils.cpp + theory/quantifiers/sygus/sygus_utils.h theory/quantifiers/sygus/synth_conjecture.cpp theory/quantifiers/sygus/synth_conjecture.h theory/quantifiers/sygus/synth_engine.cpp diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index ea767e771..caf63b0ec 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/smt_engine_subsolver.h" using namespace std; @@ -293,15 +294,8 @@ bool SygusInference::solveSygus(const std::vector& assertions, // sygus attribute to mark the conjecture as a sygus conjecture Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl; - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - theory::SygusAttribute ca; - sygusVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); - Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars); - - body = nm->mkNode(FORALL, fbvl, body, instAttrList); + body = quantifiers::SygusUtils::mkSygusConjecture(ff_vars, body); Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 8465a63a0..ecf1e281d 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" using namespace std; @@ -429,12 +430,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // sygus attribute to mark the conjecture as a sygus conjecture Trace("srs-input") << "Make sygus conjecture..." << std::endl; - Node iaVar = nm->mkSkolem("sygus", nm->booleanType()); - // the attribute to mark the conjecture as being a sygus conjecture - theory::SygusAttribute ca; - iaVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, iaVar); - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); // we are "synthesizing" functions for each type of subterm std::vector synthConj; unsigned fCounter = 1; @@ -451,10 +446,9 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // this marks that the grammar used for solutions for sfun is the type of // gvar, which is the sygus datatype type constructed above. sfun.setAttribute(ssg, gvar); - Node fvarBvl = nm->mkNode(BOUND_VAR_LIST, sfun); Node body = nm->mkConst(false); - body = nm->mkNode(FORALL, fvarBvl, body, instAttrList); + body = theory::quantifiers::SygusUtils::mkSygusConjecture({sfun}, body); synthConj.push_back(body); } Node trueNode = nm->mkConst(true); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index fa369b467..67f02b558 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -155,12 +156,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, res = nm->mkNode(EXISTS, bvl, res); } // sygus attribute - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - theory::SygusAttribute ca; - sygusVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - std::vector iplc; - iplc.push_back(instAttr); Node aconj = axioms.size() == 0 ? nm->mkConst(true) : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms)); @@ -171,18 +166,14 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, sc = nm->mkNode(EXISTS, vbvl, sc); Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); - instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); // build in the side condition // exists x. A( x ) ^ input_axioms( x ) // as an additional annotation on the sygus conjecture. In other words, // the abducts A we procedure must be consistent with our axioms. - iplc.push_back(instAttr); - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); - - Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); // forall A. exists x. ~( A( x ) => ~input( x ) ) - res = nm->mkNode(FORALL, fbvl, res, instAttrList); + res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr}); Trace("sygus-abduct-debug") << "...finish" << std::endl; res = theory::Rewriter::rewrite(res); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 79fc1a36e..23d924581 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -21,6 +21,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -44,14 +45,10 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q) Assert(q.getKind() == FORALL); for (const Node& f : q[0]) { - Node gv = f.getAttribute(SygusSynthGrammarAttribute()); - if (!gv.isNull()) + TypeNode tn = SygusUtils::getSygusTypeForSynthFun(f); + if (tn.isDatatype() && tn.getDType().isSygus()) { - TypeNode tn = gv.getType(); - if (tn.isDatatype() && tn.getDType().isSygus()) - { - return true; - } + return true; } } return false; @@ -144,7 +141,7 @@ Node CegGrammarConstructor::process(Node q, SygusGrammarNorm sygus_norm(d_qe); tn = sygus_norm.normalizeSygusType(tn, sfvl); }else{ - sfvl = getSygusVarList(sf); + sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf); // check which arguments are irrelevant std::unordered_set arg_irrelevant; d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); @@ -213,7 +210,7 @@ Node CegGrammarConstructor::process(Node q, { Node sf = q[0][i]; d_synth_fun_vars[sf] = ebvl[i]; - Node sfvl = getSygusVarList(sf); + Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf); TypeNode tn = ebvl[i].getType(); // check if there is a template std::map::const_iterator itt = templates.find(sf); @@ -1581,27 +1578,6 @@ TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); } -Node CegGrammarConstructor::getSygusVarList(Node f) -{ - Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute()); - if (sfvl.isNull() && f.getType().isFunction()) - { - NodeManager* nm = NodeManager::currentNM(); - std::vector argTypes = f.getType().getArgTypes(); - // make default variable list if none was specified by input - std::vector bvs; - for (unsigned j = 0, size = argTypes.size(); j < size; j++) - { - std::stringstream ss; - ss << "arg" << j; - bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j])); - } - sfvl = nm->mkNode(BOUND_VAR_LIST, bvs); - f.setAttribute(SygusSynthFunVarListAttribute(), sfvl); - } - return sfvl; -} - CegGrammarConstructor::SygusDatatypeGenerator::SygusDatatypeGenerator( const std::string& name) : d_sdt(name) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 872bed060..6edfbebd5 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -145,14 +145,6 @@ public: * fun is for naming */ static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); - /** - * Returns the sygus variable list for function-to-synthesize variable f. - * These are the names of the arguments of f, which should be included in the - * grammar for f. This returns either the variable list set explicitly via the - * attribute SygusSynthFunVarListAttribute, or a fresh variable list of the - * proper type otherwise. It will return null if f is not a function. - */ - static Node getSygusVarList(Node f); /** * Returns true iff there are syntax restrictions on the * functions-to-synthesize of sygus conjecture q. diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp new file mode 100644 index 000000000..ca87e1049 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -0,0 +1,180 @@ +/********************* */ +/*! \file sygus_utils.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief generic sygus utilities + **/ + +#include "theory/quantifiers/sygus/sygus_utils.h" + +#include "expr/node_algorithm.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * Attribute for specifying a solution for a function-to-synthesize. This is + * used for marking certain functions that we have solved for, e.g. during + * preprocessing. + */ +struct SygusSolutionAttributeId +{ +}; +typedef expr::Attribute SygusSolutionAttribute; + +Node SygusUtils::mkSygusConjecture(const std::vector& fs, + Node conj, + const std::vector& iattrs) +{ + Assert(!fs.empty()); + NodeManager* nm = NodeManager::currentNM(); + SygusAttribute ca; + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + sygusVar.setAttribute(ca, true); + std::vector ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)}; + // insert the remaining instantiation attributes + ipls.insert(ipls.end(), iattrs.begin(), iattrs.end()); + Node ipl = nm->mkNode(INST_PATTERN_LIST, ipls); + Node bvl = nm->mkNode(BOUND_VAR_LIST, fs); + return nm->mkNode(FORALL, bvl, conj, ipl); +} + +Node SygusUtils::mkSygusConjecture(const std::vector& fs, Node conj) +{ + std::vector iattrs; + return mkSygusConjecture(fs, conj, iattrs); +} + +Node SygusUtils::mkSygusConjecture(const std::vector& fs, + Node conj, + const Subs& solvedf) +{ + Assert(!fs.empty()); + NodeManager* nm = NodeManager::currentNM(); + std::vector iattrs; + // take existing properties, without the previous solves + SygusSolutionAttribute ssa; + // add the current solves, which should be a superset of the previous ones + for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++) + { + Node eq = solvedf.getEquality(i); + Node var = nm->mkSkolem("solved", nm->booleanType()); + var.setAttribute(ssa, eq); + Node ipv = nm->mkNode(INST_ATTRIBUTE, var); + iattrs.push_back(ipv); + } + return mkSygusConjecture(fs, conj, iattrs); +} + +void SygusUtils::decomposeSygusConjecture(Node q, + std::vector& fs, + std::vector& unsf, + Subs& solvedf) +{ + Assert(q.getKind() == FORALL); + Assert(q.getNumChildren() == 3); + Node ipl = q[2]; + Assert(ipl.getKind() == INST_PATTERN_LIST); + fs.insert(fs.end(), q[0].begin(), q[0].end()); + SygusSolutionAttribute ssa; + for (const Node& ip : ipl) + { + if (ip.getKind() == INST_ATTRIBUTE) + { + Node ipv = ip[0]; + // does it specify a sygus solution? + if (ipv.hasAttribute(ssa)) + { + Node eq = ipv.getAttribute(ssa); + Assert(std::find(fs.begin(), fs.end(), eq[0]) != fs.end()); + solvedf.addEquality(eq); + } + } + } + // add to unsolved functions + for (const Node& f : fs) + { + if (!solvedf.contains(f)) + { + unsf.push_back(f); + } + } +} + +Node SygusUtils::decomposeSygusBody(Node conj, std::vector& vs) +{ + if (conj.getKind() == NOT && conj[0].getKind() == FORALL) + { + vs.insert(vs.end(), conj[0][0].begin(), conj[0][0].end()); + return conj[0][1].negate(); + } + return conj; +} + +Node SygusUtils::getSygusArgumentListForSynthFun(Node f) +{ + Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute()); + if (sfvl.isNull() && f.getType().isFunction()) + { + NodeManager* nm = NodeManager::currentNM(); + std::vector argTypes = f.getType().getArgTypes(); + // make default variable list if none was specified by input + std::vector bvs; + for (unsigned j = 0, size = argTypes.size(); j < size; j++) + { + std::stringstream ss; + ss << "arg" << j; + bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j])); + } + sfvl = nm->mkNode(BOUND_VAR_LIST, bvs); + f.setAttribute(SygusSynthFunVarListAttribute(), sfvl); + } + return sfvl; +} + +void SygusUtils::getSygusArgumentListForSynthFun(Node f, + std::vector& formals) +{ + Node sfvl = getSygusArgumentListForSynthFun(f); + if (!sfvl.isNull()) + { + formals.insert(formals.end(), sfvl.begin(), sfvl.end()); + } +} + +Node SygusUtils::wrapSolutionForSynthFun(Node f, Node sol) +{ + Node al = getSygusArgumentListForSynthFun(f); + if (!al.isNull()) + { + sol = NodeManager::currentNM()->mkNode(LAMBDA, al, sol); + } + Assert(!expr::hasFreeVar(sol)); + return sol; +} + +TypeNode SygusUtils::getSygusTypeForSynthFun(Node f) +{ + Node gv = f.getAttribute(SygusSynthGrammarAttribute()); + if (!gv.isNull()) + { + return gv.getType(); + } + return TypeNode::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h new file mode 100644 index 000000000..c8b798097 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -0,0 +1,115 @@ +/********************* */ +/*! \file sygus_utils.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief generic sygus utilities + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H + +#include + +#include "expr/node.h" +#include "expr/subs.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class SygusUtils +{ + public: + /** + * Make (negated) sygus conjecture of the form + * forall fs. conj + * with instantiation attributes in iattrs. Notice that the marker for + * sygus conjecture is automatically prepended to this list. + * + * @param fs The functions + * @param conj The (negated) conjecture body + * @param iattrs The attributes of the conjecture. Notice this does not + * require the "sygus attribute" marker, which is automatically generated + * by this method. + */ + static Node mkSygusConjecture(const std::vector& fs, + Node conj, + const std::vector& iattrs); + /** Same as above, without auxiliary instantiation attributes */ + static Node mkSygusConjecture(const std::vector& fs, Node conj); + + /** + * Make conjecture, with a set of solved functions. In particular, + * solvedf is a substitution of the form { f1 -> t1, ... fn -> tn } where + * each f1 ... fn are in fs. + * + * In the implementation, solutions for solved functions are stored + * in the instantiation attribute list of the returned conjecture. + */ + static Node mkSygusConjecture(const std::vector& fs, + Node conj, + const Subs& solvedf); + /** + * Decompose (negated) sygus conjecture. + * + * @param q The (negated) sygus conjecture to decompose, of kind FORALL + * @param fs The functions-to-synthesize + * @param unsf The functions that have not been marked as solved. + * @param solvedf The substitution corresponding to the solved functions. + * + * The vector unsf and the domain of solved are a parition of fs. + */ + static void decomposeSygusConjecture(Node q, + std::vector& fs, + std::vector& unsf, + Subs& solvedf); + /** + * Decompose the negated body. This takes as input the body of the negated + * sygus conjecture, which is of the form (NOT (FORALL V G)) or + * quantifier-free formula G. It returns the conjecture without quantified + * variables (G), and adds the quantified variables (V) to vs. + */ + static Node decomposeSygusBody(Node conj, std::vector& vs); + + /** + * Get the formal argument list for a function-to-synthesize. This returns + * a node of kind BOUND_VAR_LIST that corresponds to the formal argument list + * of the function to synthesize. + * + * Note that if f is constant, then this returns null, since f has no + * arguments in this case. + */ + static Node getSygusArgumentListForSynthFun(Node f); + /** + * Same as above, but adds the variables to formals. + */ + static void getSygusArgumentListForSynthFun(Node f, + std::vector& formals); + /** + * Wrap a solution sol for f in the proper lambda, return the lambda + * expression. Notice the returned expression is sol itself if f has no + * formal arguments. + */ + static Node wrapSolutionForSynthFun(Node f, Node sol); + + /** + * Get the sygus datatype type that encodes the syntax restrictions for + * function-to-synthesize f. + */ + static TypeNode getSygusTypeForSynthFun(Node f); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */ diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 0ac984aa3..904bec78c 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" using namespace CVC4::kind; @@ -163,7 +164,7 @@ void SygusTemplateInfer::initialize(Node q) Assert(!templ.isNull()); // get the variables - Node sfvl = CegGrammarConstructor::getSygusVarList(prog); + Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(prog); if (!sfvl.isNull()) { std::vector prog_vars(sfvl.begin(), sfvl.end());