diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 15:08:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 15:08:00 -0500 |
commit | 72281a35622ae4656d3a2e4cd29e42cb96eba205 (patch) | |
tree | 1182a067911c1d7c2314fce70b76f0171c57ee3c /src/theory | |
parent | 9e654bc0105b04d08e8c0fb555a212228cab2c9d (diff) |
Track sygus variable to term relationship via attribute (#3182)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 27 |
4 files changed, 52 insertions, 14 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 329f9d08a..827c5e7f4 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -84,6 +84,18 @@ struct SygusSideConditionAttributeId typedef expr::Attribute<SygusSideConditionAttributeId, Node> SygusSideConditionAttribute; +/** Attribute for indicating that a sygus variable encodes a term + * + * This is used, e.g., for abduction where the formal argument list of the + * abduct-to-synthesize corresponds to the free variables of the sygus + * problem. + */ +struct SygusVarToTermAttributeId +{ +}; +typedef expr::Attribute<SygusVarToTermAttributeId, Node> + SygusVarToTermAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 52fb60c06..4f6219343 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -35,9 +35,7 @@ SygusAbduct::SygusAbduct() {} Node SygusAbduct::mkAbductionConjecture(const std::string& name, const std::vector<Node>& asserts, const std::vector<Node>& axioms, - TypeNode abdGType, - std::vector<Node>& varlist, - std::vector<Node>& syms) + TypeNode abdGType) { NodeManager* nm = NodeManager::currentNM(); std::unordered_set<Node, NodeHashFunction> symset; @@ -49,7 +47,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, << "...finish, got " << symset.size() << " symbols." << std::endl; Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector<Node> syms; std::vector<Node> vars; + std::vector<Node> varlist; std::vector<TypeNode> varlistTypes; for (const Node& s : symset) { @@ -64,6 +64,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, Node vlv = nm->mkBoundVar(ss.str(), tn); varlist.push_back(vlv); varlistTypes.push_back(tn); + // set that this variable encodes the term s + SygusVarToTermAttribute sta; + vlv.setAttribute(sta, s); } } // make the sygus variable list diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index d6bbd0e3f..2fdce542a 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -68,19 +68,19 @@ class SygusAbduct * The type abdGType (if non-null) is a sygus datatype type that encodes the * grammar that should be used for solutions of the abduction conjecture. * - * The arguments varlist and syms specify the relationship between the free - * variables of asserts and the formal argument list of the - * abduct-to-synthesize. In particular, solutions to the synthesis conjecture - * will be in the form of a closed term (lambda varlist. t). The intended - * solution, which is a term whose free variables are a subset of asserts, - * is the term t { varlist -> syms }. + * The relationship between the free variables of asserts and the formal + * rgument list of the abduct-to-synthesize are tracked by the attribute + * SygusVarToTermAttribute. + * + * In particular, solutions to the synthesis conjecture will be in the form + * of a closed term (lambda varlist. t). The intended solution, which is a + * term whose free variables are a subset of asserts, is the term + * t * { varlist -> SygusVarToTermAttribute(varlist) }. */ static Node mkAbductionConjecture(const std::string& name, const std::vector<Node>& asserts, const std::vector<Node>& axioms, - TypeNode abdGType, - std::vector<Node>& varlist, - std::vector<Node>& syms); + TypeNode abdGType); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 41caf8c6c..b302c4657 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1017,6 +1017,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { return; } + NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -1081,13 +1082,35 @@ void SynthConjecture::printSynthSolution(std::ostream& out) if (is_unique_term) { out << "(define-fun " << f << " "; - if (dt.getSygusVarList().isNull()) + // Only include variables that are truly bound variables of the + // function-to-synthesize. This means we exclude variables that encode + // external terms. This ensures that --sygus-stream prints + // solutions with no arguments on the predicate for responses to + // the get-abduct command. + // pvs stores the variables that will be printed in the argument list + // below. + std::vector<Node> pvs; + Node vl = Node::fromExpr(dt.getSygusVarList()); + if (!vl.isNull()) + { + Assert(vl.getKind() == BOUND_VAR_LIST); + SygusVarToTermAttribute sta; + for (const Node& v : vl) + { + if (!v.hasAttribute(sta)) + { + pvs.push_back(v); + } + } + } + if (pvs.empty()) { out << "() "; } else { - out << dt.getSygusVarList() << " "; + vl = nm->mkNode(BOUND_VAR_LIST, pvs); + out << vl << " "; } out << dt.getSygusType() << " "; if (status == 0) |