diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-04 12:54:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-04 17:54:58 +0000 |
| commit | 6f8200beec0c219d01ce57dab2ad8e3aa283e872 (patch) | |
| tree | e329627c98fcaa1779b7520424fcb484af8e7485 /src/theory/quantifiers/sygus/cegis.cpp | |
| parent | 763f292c2d36e54dcc5b334bba02bb211e79d200 (diff) | |
Eliminating static calls to rewriter in quantifiers (#7301)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index d9e4b61af..688d66cc3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -366,7 +366,7 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, std::vector<Node>& waiting) { Node lem = waiting[wcounter]; - lem = Rewriter::rewrite(lem); + lem = rewrite(lem); // apply substitution and rewrite if applicable if (lem.isConst()) { @@ -632,7 +632,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, candidates.begin(), candidates.end(), vals.begin(), vals.end()); Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl; // do eager rewriting - sbody = Rewriter::rewrite(sbody); + sbody = rewrite(sbody); Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -656,7 +656,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Assert(d_base_vars.size() == pt.size()); Node rlem = d_base_body.substitute( d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); - rlem = Rewriter::rewrite(rlem); + rlem = rewrite(rlem); if (std::find( d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem) == d_refinement_lemmas.end()) |