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.
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
#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;
// 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;
#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;
// 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<Node> synthConj;
unsigned fCounter = 1;
// 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);
#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"
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<Node> iplc;
- iplc.push_back(instAttr);
Node aconj = axioms.size() == 0
? nm->mkConst(true)
: (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms));
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);
#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"
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;
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<unsigned> arg_irrelevant;
d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
{
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<Node, Node>::const_iterator itt = templates.find(sf);
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<TypeNode> argTypes = f.getType().getArgTypes();
- // make default variable list if none was specified by input
- std::vector<Node> 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)
* 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.
--- /dev/null
+/********************* */
+/*! \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<SygusSolutionAttributeId, Node> SygusSolutionAttribute;
+
+Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
+ Node conj,
+ const std::vector<Node>& iattrs)
+{
+ Assert(!fs.empty());
+ NodeManager* nm = NodeManager::currentNM();
+ SygusAttribute ca;
+ Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+ sygusVar.setAttribute(ca, true);
+ std::vector<Node> 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<Node>& fs, Node conj)
+{
+ std::vector<Node> iattrs;
+ return mkSygusConjecture(fs, conj, iattrs);
+}
+
+Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
+ Node conj,
+ const Subs& solvedf)
+{
+ Assert(!fs.empty());
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> 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<Node>& fs,
+ std::vector<Node>& 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<Node>& 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<TypeNode> argTypes = f.getType().getArgTypes();
+ // make default variable list if none was specified by input
+ std::vector<Node> 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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& fs,
+ Node conj,
+ const std::vector<Node>& iattrs);
+ /** Same as above, without auxiliary instantiation attributes */
+ static Node mkSygusConjecture(const std::vector<Node>& 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<Node>& 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<Node>& fs,
+ std::vector<Node>& 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<Node>& 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<Node>& 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 */
#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;
Assert(!templ.isNull());
// get the variables
- Node sfvl = CegGrammarConstructor::getSygusVarList(prog);
+ Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(prog);
if (!sfvl.isNull())
{
std::vector<Node> prog_vars(sfvl.begin(), sfvl.end());
projects / cvc5.git / commitdiff