Add rewrite for is_int pi (#7711)

Fixes cvc5/cvc5-projects#365.
Fixes cvc5/cvc5-projects#356.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 19b5c1204094bcdf899c61ac5332d06c51944b26..8408f15bb9f53271e0901c16b15ca9f578185f29 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -166,6 +166,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
   }else if(t.isVar()){
     return rewriteVariable(t);
   }else{
+    Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl;
     switch(t.getKind()){
     case kind::MINUS:
       return rewriteMinus(t, false);
@@ -213,29 +214,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
     case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
-    case kind::TO_INTEGER:
-      if(t[0].isConst()) {
-        return RewriteResponse(
-            REWRITE_DONE,
-            NodeManager::currentNM()->mkConst(
-                CONST_RATIONAL, Rational(t[0].getConst<Rational>().floor())));
-      }
-      if(t[0].getType().isInteger()) {
-        return RewriteResponse(REWRITE_DONE, t[0]);
-      }
-      //Unimplemented() << "TO_INTEGER, nonconstant";
-      //return rewriteToInteger(t);
-      return RewriteResponse(REWRITE_DONE, t);
-    case kind::IS_INTEGER:
-      if(t[0].isConst()) {
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst<Rational>().getDenominator() == 1));
-      }
-      if(t[0].getType().isInteger()) {
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-      }
-      //Unimplemented() << "IS_INTEGER, nonconstant";
-      //return rewriteIsInteger(t);
-      return RewriteResponse(REWRITE_DONE, t);
+    case kind::TO_INTEGER:return rewriteExtIntegerOp(t);
     case kind::POW:
       {
         if(t[1].getKind() == kind::CONST_RATIONAL){
@@ -668,14 +647,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
 
 RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   if(atom.getKind() == kind::IS_INTEGER) {
-    if(atom[0].isConst()) {
-      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst<Rational>().isIntegral()));
-    }
-    if(atom[0].getType().isInteger()) {
-      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-    }
-    // not supported, but this isn't the right place to complain
-    return RewriteResponse(REWRITE_DONE, atom);
+    return rewriteExtIntegerOp(atom);
   } else if(atom.getKind() == kind::DIVISIBLE) {
     if(atom[0].isConst()) {
       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst<Rational>() / atom.getOperator().getConst<Divisible>().k).isIntegral())));
@@ -847,6 +819,37 @@ RewriteResponse ArithRewriter::rewriteIntsDivMod(TNode t, bool pre)
   return RewriteResponse(REWRITE_DONE, t);
 }
 
+RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
+{
+  Assert(t.getKind() == kind::TO_INTEGER || t.getKind() == kind::IS_INTEGER);
+  bool isPred = t.getKind() == kind::IS_INTEGER;
+  NodeManager* nm = NodeManager::currentNM();
+  if (t[0].isConst())
+  {
+    Node ret;
+    if (isPred)
+    {
+      ret = nm->mkConst(t[0].getConst<Rational>().isIntegral());
+    }
+    else
+    {
+      ret = nm->mkConstInt(Rational(t[0].getConst<Rational>().floor()));
+    }
+    return returnRewrite(t, ret, Rewrite::INT_EXT_CONST);
+  }
+  if (t[0].getType().isInteger())
+  {
+    Node ret = isPred ? nm->mkConst(true) : Node(t[0]);
+    return returnRewrite(t, ret, Rewrite::INT_EXT_INT);
+  }
+  if (t[0].getKind() == kind::PI)
+  {
+    Node ret = isPred ? nm->mkConst(false) : nm->mkConstReal(Rational(3));
+    return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
+
 RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre)
 {
   if (pre)

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 813f2b1bb96f5e823148b1e01d967853878bce5e..1f861b08a8f26e47446552c93a8960e2d795787b 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -56,6 +56,8 @@ class ArithRewriter : public TheoryRewriter
   static RewriteResponse rewriteDiv(TNode t, bool pre);
   static RewriteResponse rewriteIntsDivMod(TNode t, bool pre);
   static RewriteResponse rewriteIntsDivModTotal(TNode t, bool pre);
+  /** Entry for applications of to_int and is_int */
+  static RewriteResponse rewriteExtIntegerOp(TNode t);
 
   static RewriteResponse preRewritePlus(TNode t);
   static RewriteResponse postRewritePlus(TNode t);

diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp
index a7013242238084afe1374e3a19f89a3a87f8ed98..2283cd73a81ccc5350c121e450493e67ab4a39c6 100644 (file)
--- a/src/theory/arith/rewrites.cpp
+++ b/src/theory/arith/rewrites.cpp
@@ -36,6 +36,9 @@ const char* toString(Rewrite r)
     case Rewrite::MOD_OVER_MOD: return "MOD_OVER_MOD";
     case Rewrite::MOD_CHILD_MOD: return "MOD_CHILD_MOD";
     case Rewrite::DIV_OVER_MOD: return "DIV_OVER_MOD";
+    case Rewrite::INT_EXT_CONST: return "INT_EXT_CONST";
+    case Rewrite::INT_EXT_INT: return "INT_EXT_INT";
+    case Rewrite::INT_EXT_PI: return "INT_EXT_PI";
     default: return "?";
   }
 }

diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h
index 24b6abdd5d551efb7bc27b06ed13b9e4796c139c..6053be916e06146cb4a17654dbfb0f333c126e29 100644 (file)
--- a/src/theory/arith/rewrites.h
+++ b/src/theory/arith/rewrites.h
@@ -53,7 +53,13 @@ enum class Rewrite : uint32_t
   // op is one of { NONLINEAR_MULT, MULT, PLUS }.
   MOD_CHILD_MOD,
   // (div (mod x c) c) --> 0
-  DIV_OVER_MOD
+  DIV_OVER_MOD,
+  // (to_int c) --> floor(c), (is_int c) --> true iff c is int
+  INT_EXT_CONST,
+  // (to_int t) --> t, (is_int t) ---> true if t is int
+  INT_EXT_INT,
+  // (to_int real.pi) --> 3, (is_int real.pi) ---> false
+  INT_EXT_PI
 };
 
 /**

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 686c0ff6ee8d4ae8f0e1ce4e4b6636f2a55adf8d..e52f2ac63ab3e6b4d84fca5f1a08ed02cb6d99af 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1814,6 +1814,7 @@ set(regress_1_tests
   regress1/nl/ones.smt2
   regress1/nl/pinto-model-core-ni.smt2
   regress1/nl/poly-1025.smt2
+  regress1/nl/proj-365-is-int-pi.smt2
   regress1/nl/quant-nl.smt2
   regress1/nl/red-exp.smt2
   regress1/nl/rewriting-sums.smt2

diff --git a/test/regress/regress1/nl/proj-365-is-int-pi.smt2 b/test/regress/regress1/nl/proj-365-is-int-pi.smt2
new file mode 100644 (file)
index 0000000..dab3dcf
--- /dev/null
+++ b/test/regress/regress1/nl/proj-365-is-int-pi.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :nl-ext light)
+(assert (is_int real.pi))
+(check-sat)