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/quantifiers/sygus/sygus_abduct.cpp | |
| parent | 9e654bc0105b04d08e8c0fb555a212228cab2c9d (diff) | |
Track sygus variable to term relationship via attribute (#3182)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_abduct.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
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 |