diff options
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 6 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/nl/pow2-pow.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/arith/bug716.1.cvc | 4 |
4 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 6eda6283c..5baaaf317 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -255,6 +255,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ } } } + else if (t[0].getKind() == kind::CONST_RATIONAL + && t[0].getConst<Rational>().getNumerator().toUnsignedInt() == 2) + { + return RewriteResponse( + REWRITE_DONE, NodeManager::currentNM()->mkNode(kind::POW2, t[1])); + } // Todo improve the exception thrown std::stringstream ss; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d2d6f0855..abd21e222 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -737,6 +737,7 @@ set(regress_0_tests regress0/nl/pow2-native-1.smt2 regress0/nl/pow2-native-2.smt2 regress0/nl/pow2-native-3.smt2 + regress0/nl/pow2-pow.smt2 regress0/nl/real-as-int.smt2 regress0/nl/real-div-ufnra.smt2 regress0/nl/sin-cos-346-b-chunk-0169.smt2 diff --git a/test/regress/regress0/nl/pow2-pow.smt2 b/test/regress/regress0/nl/pow2-pow.smt2 new file mode 100644 index 000000000..8fdbfa659 --- /dev/null +++ b/test/regress/regress0/nl/pow2-pow.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic QF_NIA) +(declare-fun x () Int) +(assert (< x 0)) +(assert (distinct (^ 2 x) 0)) +(check-sat) diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc index 854062beb..50be132af 100644 --- a/test/regress/regress1/arith/bug716.1.cvc +++ b/test/regress/regress1/arith/bug716.1.cvc @@ -1,6 +1,6 @@ % EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in: -% EXPECT: 2 ^ x +% EXPECT: 3 ^ x % EXIT: 1 x: INT; -ASSERT 2^x = 8; +ASSERT 3^x = 27; QUERY x=3; |