diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c38d0aa91..c53809d6e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -443,7 +443,7 @@ Node QuantifiersRewriter::computeProcessTerms(Node body, { Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds); Assert(new_vars.size() == h.getNumChildren()); - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r)); + return NodeManager::currentNM()->mkNode(EQUAL, h, r); } // It can happen that we can't infer the shape of the function definition, // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to @@ -906,9 +906,9 @@ bool QuantifiersRewriter::getVarElimLit(Node body, // take into account if parametric if (dt.isParametric()) { - tspec = c.getSpecializedConstructorType(lit[0].getType()); - cons = nm->mkNode( - APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons); + TypeNode ltn = lit[0].getType(); + tspec = c.getInstantiatedConstructorType(ltn); + cons = c.getInstantiatedConstructor(ltn); } else { @@ -920,7 +920,7 @@ bool QuantifiersRewriter::getVarElimLit(Node body, for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { TypeNode tn = tspec[j]; - Node rn = nm->mkConst(CONST_RATIONAL, Rational(j)); + Node rn = nm->mkConstInt(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn); newChildren.push_back(v); @@ -1028,12 +1028,11 @@ bool QuantifiersRewriter::getVarElimInternal(Node body, std::vector<Node>& subs) const { Kind nk = n.getKind(); - if (nk == NOT) + while (nk == NOT) { n = n[0]; pol = !pol; nk = n.getKind(); - Assert(nk != NOT); } if ((nk == AND && pol) || (nk == OR && !pol)) { @@ -1326,7 +1325,6 @@ Node QuantifiersRewriter::computeVarElimination(Node body, // remake with eliminated nodes body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - body = Rewriter::rewrite(body); if (!qa.d_ipl.isNull()) { qa.d_ipl = qa.d_ipl.substitute( |