diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-27 17:29:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-27 17:29:02 -0500 |
commit | 98cdd72fca04e76eb1057d694e1dad9717351f7f (patch) | |
tree | 5f3c93c3d046f9264b9abac11260699ca8f87387 /src/theory/quantifiers/sygus/synth_engine.cpp | |
parent | b52dc978f2445c6765b806119d238ca81cb8fe90 (diff) |
Fix sygus quantifier elimination preprocess for multiple functions (#5130)
The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 95f1acb25..5358a0aff 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -184,13 +184,19 @@ void SynthEngine::assignConjecture(Node q) for (unsigned i = 0, size = all_vars.size(); i < size; i++) { Node v = all_vars[i]; - if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) + if (std::find(funcs0.begin(), funcs0.end(), v) != funcs0.end()) + { + Trace("cegqi-qep") << "- fun var: " << v << std::endl; + } + else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) { qe_vars.push_back(v); + Trace("cegqi-qep") << "- qe var: " << v << std::endl; } else { nqe_vars.push_back(v); + Trace("cegqi-qep") << "- non qe var: " << v << std::endl; } } std::vector<Node> orig; |