Improving support for POW in arithmetic. Resolves bug 549.

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index ca463d10b82041a15e90a017b0316ffa043122db..4d784c383c07d3860146415c669d43eea8a88a13 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -478,6 +478,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << ">=";
       opType = INFIX;
       break;
+    case kind::POW:
+      op << '^';
+      opType = INFIX;
+      break;
 
     // BITVECTORS
     case kind::BITVECTOR_XOR:

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index dd6eac0ff6c485a7be284ff51b72bf2c6d571aa9..849d5c0a5fc74e391fee0fb5dd3ac71bbe079053 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,7 +281,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::ABS:
   case kind::IS_INTEGER:
   case kind::TO_INTEGER:
-  case kind::TO_REAL: out << smtKindString(k) << " "; break;
+  case kind::TO_REAL:
+  case kind::POW: out << smtKindString(k) << " "; break;
 
   case kind::DIVISIBLE:
     out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
@@ -545,6 +546,7 @@ static string smtKindString(Kind k) throw() {
   case kind::IS_INTEGER: return "is_int";
   case kind::TO_INTEGER: return "to_int";
   case kind::TO_REAL: return "to_real";
+  case kind::POW: return "^";
 
     // arrays theory
   case kind::SELECT: return "select";

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index f725379657e57be18d81c224cc00db2c8214d7a2..e1cab03568df672cf9248823c512a9b7a5b57ca7 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -121,11 +121,14 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
       return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::POW:
+      return RewriteResponse(REWRITE_DONE, t);
     default:
       Unhandled(k);
     }
   }
 }
+
 RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
   if(t.isConst()){
     return rewriteConstant(t);
@@ -182,6 +185,33 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       //Unimplemented("IS_INTEGER, nonconstant");
       //return rewriteIsInteger(t);
       return RewriteResponse(REWRITE_DONE, t);
+    case kind::POW:
+      {
+        if(t[1].getKind() == kind::CONST_RATIONAL){
+          const Rational& exp = t[1].getConst<Rational>();
+          TNode base = t[0];
+          if(exp.sgn() == 0){
+            return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1)));
+          }else if(exp.sgn() > 0 && exp.isIntegral()){
+            Integer num = exp.getNumerator();
+            NodeBuilder<> nb(kind::MULT);
+            Integer one(1);
+            for(Integer i(0); i < num; i = i + one){
+              nb << base;
+            }
+            Assert(nb.getNumChildren() > 0);
+            Node mult = nb;
+            return RewriteResponse(REWRITE_AGAIN, mult);
+          }
+        }
+
+        // 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 occured in:" << std::endl;
+        ss << "  " << t;
+        throw Exception(ss.str());
+      }
     default:
       Unreachable();
     }

diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc
new file mode 100644 (file)
index 0000000..54df5e6
--- /dev/null
+++ b/test/regress/regress0/arith/bug549.cvc
@@ -0,0 +1,3 @@
+% EXPECT: valid
+a, b : REAL;
+QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
\ No newline at end of file