diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 12:41:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-20 12:41:49 -0500 |
commit | ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 (patch) | |
tree | e2195f62132de9dc009bc91a3a46380404fcfa3a /src/theory | |
parent | 696b9d7e06b132bd3cb2d343acecba775e141e24 (diff) |
Handle failures for sygus QE preprocess (#4072)
If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 42 |
1 files changed, 23 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 978e31545..0c8b8f734 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -15,6 +15,7 @@ **/ #include "theory/quantifiers/sygus/synth_engine.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -236,28 +237,31 @@ void SynthEngine::assignConjecture(Node q) conj_se_ngsi_subs.toExpr(), true, false); Trace("cegqi-qep") << "Result : " << qe_res << std::endl; - // create single invocation conjecture + // create single invocation conjecture, if QE was successful Node qe_res_n = Node::fromExpr(qe_res); - qe_res_n = qe_res_n.substitute( - subs.begin(), subs.end(), orig.begin(), orig.end()); - if (!nqe_vars.empty()) + if (!expr::hasBoundVar(qe_res_n)) { - qe_res_n = - nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); - } - Assert(q.getNumChildren() == 3); - qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]); - Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n - << std::endl; - qe_res_n = Rewriter::rewrite(qe_res_n); - Node nq = qe_res_n; - // must assert it is equivalent to the original - Node lem = q.eqNode(nq); - Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem + qe_res_n = qe_res_n.substitute( + subs.begin(), subs.end(), orig.begin(), orig.end()); + if (!nqe_vars.empty()) + { + qe_res_n = nm->mkNode( + EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); + } + Assert(q.getNumChildren() == 3); + qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n << std::endl; - d_quantEngine->getOutputChannel().lemma(lem); - // we've reduced the original to a preprocessed version, return - return; + qe_res_n = Rewriter::rewrite(qe_res_n); + Node nq = qe_res_n; + // must assert it is equivalent to the original + Node lem = q.eqNode(nq); + Trace("cegqi-lemma") + << "Cegqi::Lemma : qe-preprocess : " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma(lem); + // we've reduced the original to a preprocessed version, return + return; + } } } // allocate a new synthesis conjecture if not assigned |