diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 10:29:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-14 10:29:08 -0500 |
| commit | 33420e77e9f7ee7a429708db3a7f6c28aef7d0ec (patch) | |
| tree | de1d33cc21a9453caf0c0c1799b375d7ab53d5c9 /src/theory/quantifiers/sygus/cegis.cpp | |
| parent | 53c73505c5aed92401cfe02b669abaf8e6a30e32 (diff) | |
Flag to check invariance of entire values in sygus explain (#1908)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 92fea9586..e8d29835a 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -236,6 +236,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, std::vector<Node> msu; std::vector<Node> mexp; msu.insert(msu.end(), ms.begin(), ms.end()); + std::map<TypeNode, int> var_count; for (unsigned k = 0; k < vs.size(); k++) { vsit.setUpdatedTerm(msu[k]); @@ -249,8 +250,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Trace("sygus-cref-eval2-debug") << " compute min explain of : " << vs[k] << " = " << ut << std::endl; - tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit); - msu[k] = ut; + tds->getExplain()->getExplanationFor( + vs[k], ut, mexp, vsit, var_count, false); + Trace("sygus-cref-eval2-debug") + << "exp now: " << mexp << std::endl; + msu[k] = vsit.getUpdatedTerm(); + Trace("sygus-cref-eval2-debug") + << "updated term : " << msu[k] << std::endl; } if (!mexp.empty()) { |