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 | |
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
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 11 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/arith/bug716.1.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/arith/bug716.2.cvc | 6 |
4 files changed, 15 insertions, 5 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()); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f9840e552..0b0da8e93 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1247,6 +1247,7 @@ set(regress_1_tests regress1/arith/bug547.1.smt2 regress1/arith/bug716.0.smt2 regress1/arith/bug716.1.cvc + regress1/arith/bug716.2.cvc regress1/arith/div.03.smt2 regress1/arith/div.06.smt2 regress1/arith/div.08.smt2 diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc index d9330c727..854062beb 100644 --- a/test/regress/regress1/arith/bug716.1.cvc +++ b/test/regress/regress1/arith/bug716.1.cvc @@ -1,4 +1,4 @@ -% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occurred in: +% EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in: % EXPECT: 2 ^ x % EXIT: 1 x: INT; diff --git a/test/regress/regress1/arith/bug716.2.cvc b/test/regress/regress1/arith/bug716.2.cvc new file mode 100644 index 000000000..eb9b733fc --- /dev/null +++ b/test/regress/regress1/arith/bug716.2.cvc @@ -0,0 +1,6 @@ +% EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in: +% EXPECT: x ^ 67108864 +% EXIT: 1 +x: INT; +ASSERT x^67108864 = 8; +QUERY x=3; |