diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-20 06:04:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-20 06:04:43 -0500 |
| commit | c110363ccf39c9415c1a32bda6273fe8221db182 (patch) | |
| tree | 0d0ec2edc846b5c9a495ed29e077472ab74b0d40 /src/theory/quantifiers/sygus/synth_engine.cpp | |
| parent | eee14382af077bd043d53b75c038050b325dd04a (diff) | |
Split QuantElimSolver from SmtEngine (#4919)
Towards refactoring SmtEngine / converting Expr -> Node.
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f8349c834..3e47c1155 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -233,27 +233,26 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe->doQuantifierElimination( - conj_se_ngsi_subs.toExpr(), true, false); - Trace("cegqi-qep") << "Result : " << qe_res << std::endl; + Node qeRes = + smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false); + Trace("cegqi-qep") << "Result : " << qeRes << std::endl; // create single invocation conjecture, if QE was successful - Node qe_res_n = Node::fromExpr(qe_res); - if (!expr::hasBoundVar(qe_res_n)) + if (!expr::hasBoundVar(qeRes)) { - qe_res_n = qe_res_n.substitute( + qeRes = qeRes.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); + qeRes = + nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qeRes); } 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 + qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes << std::endl; - qe_res_n = Rewriter::rewrite(qe_res_n); - Node nq = qe_res_n; + qeRes = Rewriter::rewrite(qeRes); + Node nq = qeRes; // must assert it is equivalent to the original Node lem = q.eqNode(nq); Trace("cegqi-lemma") |