From 52b3385489537ba4b5577e1596b74ba0eb0aed21 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 May 2022 09:58:22 -0500 Subject: [PATCH] Relax an assertion in the evaluator (#8751) In a rare case this can throw after https://github.com/cvc5/cvc5/pull/8740, complaining that `(/ 0.0 0)` and `(/ 0.0 0.0)` are not the same. --- src/theory/evaluator.cpp | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index ab03ba395..51e0357e6 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -169,19 +169,24 @@ Node Evaluator::eval(TNode n, Node ret = evalInternal(n, args, vals, evalAsNode, results).toNode(n.getType()); // if we failed to evaluate - if (ret.isNull() && d_rr != nullptr) + if (d_rr != nullptr) { - // should be stored in the evaluation-as-node map - std::unordered_map::iterator itn = evalAsNode.find(n); - Assert(itn != evalAsNode.end()); - ret = d_rr->rewrite(itn->second); + if (ret.isNull()) + { + // should be stored in the evaluation-as-node map + std::unordered_map::iterator itn = evalAsNode.find(n); + Assert(itn != evalAsNode.end()); + ret = itn->second; + } + // always rewrite, which can change if the evaluation was not a constant + ret = d_rr->rewrite(ret); } // should be the same as substitution + rewriting, or possibly null if - // d_rr is nullptr - Assert((ret.isNull() && d_rr == nullptr) + // d_rr is nullptr or non-constant + Assert(((ret.isNull() || !ret.isConst()) && d_rr == nullptr) || ret == d_rr->rewrite(n.substitute( - args.begin(), args.end(), vals.begin(), vals.end()))); + args.begin(), args.end(), vals.begin(), vals.end()))); return ret; } -- 2.30.2