From: Tim King <taking@cs.nyu.edu>
Date: Wed, 5 Mar 2014 17:04:03 +0000 (-0500)
Subject: Improving support for POW in arithmetic. Resolves bug 549.
X-Git-Tag: cvc5-1.0.0~7047
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df554608cc47684be08d8be7c427027b7c5e8eb2;p=cvc5.git

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 ca463d10b..4d784c383 100644
--- 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 dd6eac0ff..849d5c0a5 100644
--- 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 f72537965..e1cab0356 100644
--- 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
index 000000000..54df5e62c
--- /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