diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-05 20:55:00 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-05 13:55:00 -0500 |
commit | 47f003828a8ba0cd8edd362accaef8b2449b0c46 (patch) | |
tree | d67941c0c017262dc287fda36b1a9818302e4d30 /src/theory/arith/arith_rewriter.cpp | |
parent | d07c7796f75e32e46698f4f0af90a8b99577323f (diff) |
Improve error message for unsupported exponents (#4852)
We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 188ef47e6..f0e0487a0 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -229,8 +229,9 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if(exp.sgn() == 0){ return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1))); }else if(exp.sgn() > 0 && exp.isIntegral()){ - CVC4::Rational r(INT_MAX); - if( exp<r ){ + CVC4::Rational r(expr::NodeValue::MAX_CHILDREN); + if (exp <= r) + { unsigned num = exp.getNumerator().toUnsignedInt(); if( num==1 ){ return RewriteResponse(REWRITE_AGAIN, base); @@ -249,8 +250,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ // Todo improve the exception thrown std::stringstream ss; - ss << "The POW(^) operator can only be used with a natural number "; - ss << "in the exponent. Exception occurred in:" << std::endl; + ss << "The exponent of the POW(^) operator can only be a positive " + "integral constant below " + << (expr::NodeValue::MAX_CHILDREN + 1) << ". "; + ss << "Exception occurred in:" << std::endl; ss << " " << t; throw LogicException(ss.str()); } |