From ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Mar 2020 12:41:49 -0500 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 4 +- src/theory/quantifiers/sygus/synth_engine.cpp | 42 ++++++++++--------- 2 files changed, 26 insertions(+), 20 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3ba34b6c..a367c8469 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5164,9 +5164,11 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) Trace("smt-qe") << "Query returned " << r << std::endl; if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) { if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){ - InternalError() + Notice() << "While performing quantifier elimination, unexpected result : " << r << " for query."; + // failed, return original + return e; } std::vector< Node > inst_qs; d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs ); 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 -- 2.30.2