Towards proper usage of TO_REAL (#8680)

This is work towards making the rewriter preserve types, which is work towards eliminating subtyping.

This makes it so that the arithmetic rewriter does not simply drop TO_REAL from all terms, as this may change the type of the Node. Instead, TO_REAL is pulled upwards, and can be removed beneath arithmetic relations. TO_REAL is not eliminated if it occurs as a child of an operator not belonging to arithmetic. For example if x,y : Int:

(= (+ (to_real x) y) 0.0) ---> (= (to_real (+ x y)) 0.0) ---> (= (+ x y) 0.0) ; note this is the same rewritten form as before
(P (+ (to_real x) y)) ---> (P (to_real (+ x y))).

The one exception is that to_real applied to constants is simply dropped (for now), for example:

(to_real 5) ---> 5

where above, a Real term is rewritten to an Int term. (Fixing this will require further PRs that make integer constants of kind CONST_INTEGER and integral CONST_RATIONAL have Real type, thus we can have the above rewrite return 5 that is constant and has type Real).

Several quantifiers utilities are patched to preserve their behavior wrt handling TO_REAL.

Finally, a few fixes for subtypes are made to the regressions that we were not catching as errors before, and adds one regression.

The net effect of this PR is that the rewritten form of terms may have to_real applications that occur as direct children of symbols from other theories. Special care is required for preregistration, shared terms, and getting model values in the linear solver to strip off TO_REAL if necessary before using the (unmodified) interface to the linear solver.

FYI @barrettcw

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index b32d488a29fcaae2f7f2925c4a7043c18e8ba4e2..128b2e84cf5476e39a8e3bdfc76ad92767f654fb 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -81,12 +81,18 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom)
 {
   Assert(rewriter::isAtom(atom));
 
-  if (auto response = rewriter::tryEvaluateRelationReflexive(atom); response)
+  Kind kind = atom.getKind();
+  if (atom.getNumChildren() == 2)
   {
-    return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response));
+    if (auto response =
+            rewriter::tryEvaluateRelationReflexive(kind, atom[0], atom[1]);
+        response)
+    {
+      return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response));
+    }
   }
 
-  switch (atom.getKind())
+  switch (kind)
   {
     case Kind::GT:
       return RewriteResponse(
@@ -144,16 +150,17 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom)
             nm->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], rewriter::mkConst(k)),
             rewriter::mkConst(Integer(0))));
   }
+  // left |><| right
+  Kind kind = atom.getKind();
+  Node left = removeToReal(atom[0]);
+  Node right = removeToReal(atom[1]);
 
-  if (auto response = rewriter::tryEvaluateRelationReflexive(atom); response)
+  if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right);
+      response)
   {
     return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response));
   }
 
-  // left |><| right
-  Kind kind = atom.getKind();
-  TNode left = atom[0];
-  TNode right = atom[1];
   Assert(isRelationOperator(kind));
 
   if (auto response = rewriter::tryEvaluateRelation(kind, left, right);
@@ -241,10 +248,10 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true);
       case kind::ABS: return rewriteAbs(t);
       case kind::IS_INTEGER:
-      case kind::TO_INTEGER: return RewriteResponse(REWRITE_DONE, t);
+      case kind::TO_INTEGER:
       case kind::TO_REAL:
-      case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
-      case kind::POW: return RewriteResponse(REWRITE_DONE, t);
+      case kind::CAST_TO_REAL:
+      case kind::POW:
       case kind::PI: return RewriteResponse(REWRITE_DONE, t);
       default: Unhandled() << k;
     }
@@ -291,7 +298,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false);
       case kind::ABS: return rewriteAbs(t);
       case kind::TO_REAL:
-      case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
+      case kind::CAST_TO_REAL: return rewriteToReal(t);
       case kind::TO_INTEGER: return rewriteExtIntegerOp(t);
       case kind::POW:
       {
@@ -350,6 +357,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
 RewriteResponse ArithRewriter::rewriteRAN(TNode t)
 {
   Assert(rewriter::isRAN(t));
+  Assert(t.getType().isReal());
   const RealAlgebraicNumber& r = rewriter::getRAN(t);
   if (r.isRational())
   {
@@ -369,10 +377,12 @@ RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
 {
   Assert(t.getKind() == kind::NEG);
 
+  NodeManager* nm = NodeManager::currentNM();
   if (t[0].isConst())
   {
     Rational neg = -(t[0].getConst<Rational>());
-    return RewriteResponse(REWRITE_DONE, rewriter::mkConst(neg));
+    return RewriteResponse(REWRITE_DONE,
+                           nm->mkConstRealOrInt(t.getType(), neg));
   }
   if (rewriter::isRAN(t[0]))
   {
@@ -380,8 +390,7 @@ RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
                            rewriter::mkConst(-rewriter::getRAN(t[0])));
   }
 
-  auto* nm = NodeManager::currentNM();
-  Node noUminus = nm->mkNode(kind::MULT, rewriter::mkConst(Integer(-1)), t[0]);
+  Node noUminus = nm->mkNode(kind::MULT, rewriter::mkConst(Rational(-1)), t[0]);
   if (pre)
   {
     return RewriteResponse(REWRITE_DONE, noUminus);
@@ -397,16 +406,19 @@ RewriteResponse ArithRewriter::rewriteSub(TNode t)
   Assert(t.getKind() == kind::SUB);
   Assert(t.getNumChildren() == 2);
 
+  NodeManager* nm = NodeManager::currentNM();
   if (t[0] == t[1])
   {
-    return RewriteResponse(REWRITE_DONE, rewriter::mkConst(Integer(0)));
+    return RewriteResponse(REWRITE_DONE,
+                           nm->mkConstRealOrInt(t.getType(), Rational(0)));
   }
-  auto* nm = NodeManager::currentNM();
   return RewriteResponse(
       REWRITE_AGAIN_FULL,
       nm->mkNode(Kind::ADD,
                  t[0],
-                 nm->mkNode(kind::MULT, rewriter::mkConst(Integer(-1)), t[1])));
+                 nm->mkNode(kind::MULT,
+                            nm->mkConstRealOrInt(t[1].getType(), Rational(-1)),
+                            t[1])));
 }
 
 RewriteResponse ArithRewriter::preRewritePlus(TNode t)
@@ -426,9 +438,11 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t)
   rewriter::Sum sum;
   for (const auto& child : children)
   {
-    rewriter::addToSum(sum, child);
+    rewriter::addToSum(sum, removeToReal(child));
   }
-  return RewriteResponse(REWRITE_DONE, rewriter::collectSum(sum));
+  Node retSum = rewriter::collectSum(sum);
+  retSum = maybeEnsureReal(t.getType(), retSum);
+  return RewriteResponse(REWRITE_DONE, retSum);
 }
 
 RewriteResponse ArithRewriter::preRewriteMult(TNode node)
@@ -438,7 +452,7 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode node)
 
   if (auto res = rewriter::getZeroChild(node); res)
   {
-    return RewriteResponse(REWRITE_DONE, *res);
+    return RewriteResponse(REWRITE_DONE, maybeEnsureReal(node.getType(), *res));
   }
   return RewriteResponse(REWRITE_DONE, node);
 }
@@ -452,43 +466,52 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
 
   if (auto res = rewriter::getZeroChild(children); res)
   {
-    return RewriteResponse(REWRITE_DONE, *res);
+    return RewriteResponse(REWRITE_DONE, maybeEnsureReal(t.getType(), *res));
   }
 
+  // remove TO_REAL
+  for (TNode& tc : children)
+  {
+    tc = removeToReal(tc);
+  }
+
+  Node ret;
   // Distribute over addition
   if (std::any_of(children.begin(), children.end(), [](TNode child) {
         return child.getKind() == Kind::ADD;
       }))
   {
-    return RewriteResponse(REWRITE_DONE,
-                           rewriter::distributeMultiplication(children));
+    ret = rewriter::distributeMultiplication(children);
   }
-
-  RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1));
-  std::vector<Node> leafs;
-
-  for (const auto& child : children)
+  else
   {
-    if (child.isConst())
+    RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1));
+    std::vector<Node> leafs;
+
+    for (const auto& child : children)
     {
-      if (child.getConst<Rational>().isZero())
+      if (child.isConst())
       {
-        return RewriteResponse(REWRITE_DONE, child);
+        if (child.getConst<Rational>().isZero())
+        {
+          return RewriteResponse(REWRITE_DONE,
+                                 maybeEnsureReal(t.getType(), child));
+        }
+        ran *= child.getConst<Rational>();
+      }
+      else if (rewriter::isRAN(child))
+      {
+        ran *= rewriter::getRAN(child);
+      }
+      else
+      {
+        leafs.emplace_back(child);
       }
-      ran *= child.getConst<Rational>();
-    }
-    else if (rewriter::isRAN(child))
-    {
-      ran *= rewriter::getRAN(child);
-    }
-    else
-    {
-      leafs.emplace_back(child);
     }
+    ret = rewriter::mkMultTerm(ran, std::move(leafs));
   }
-
-  return RewriteResponse(REWRITE_DONE,
-                         rewriter::mkMultTerm(ran, std::move(leafs)));
+  ret = maybeEnsureReal(t.getType(), ret);
+  return RewriteResponse(REWRITE_DONE, ret);
 }
 
 RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
@@ -496,22 +519,22 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
   Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION);
   Assert(t.getNumChildren() == 2);
 
-  Node left = t[0];
-  Node right = t[1];
+  Node left = removeToReal(t[0]);
+  Node right = removeToReal(t[1]);
+  NodeManager* nm = NodeManager::currentNM();
   if (right.isConst())
   {
-    NodeManager* nm = NodeManager::currentNM();
     const Rational& den = right.getConst<Rational>();
 
     if (den.isZero())
     {
       if (t.getKind() == kind::DIVISION_TOTAL)
       {
-        return RewriteResponse(REWRITE_DONE, nm->mkConstReal(0));
+        Node ret = nm->mkConstReal(0);
+        return RewriteResponse(REWRITE_DONE, ret);
       }
       else
       {
-        // This is unsupported, but this is not a good place to complain
         return RewriteResponse(REWRITE_DONE, t);
       }
     }
@@ -530,42 +553,68 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
     }
 
     Node result = nm->mkConstReal(den.inverse());
-    Node mult = NodeManager::currentNM()->mkNode(kind::MULT, left, result);
+    Node mult =
+        ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result));
     if (pre)
     {
       return RewriteResponse(REWRITE_DONE, mult);
     }
-    else
-    {
-      return RewriteResponse(REWRITE_AGAIN, mult);
-    }
+    // requires again full since ensureReal may have added a to_real
+    return RewriteResponse(REWRITE_AGAIN_FULL, mult);
   }
   if (rewriter::isRAN(right))
   {
     const RealAlgebraicNumber& den = rewriter::getRAN(right);
-
+    // mkConst is applied to RAN in this block, which are always Real
     if (left.isConst())
     {
       return RewriteResponse(
-          REWRITE_DONE, rewriter::mkConst(left.getConst<Rational>() / den));
+          REWRITE_DONE,
+          ensureReal(rewriter::mkConst(left.getConst<Rational>() / den)));
     }
     if (rewriter::isRAN(left))
     {
-      return RewriteResponse(REWRITE_DONE,
-                             rewriter::mkConst(rewriter::getRAN(left) / den));
+      return RewriteResponse(
+          REWRITE_DONE,
+          ensureReal(rewriter::mkConst(rewriter::getRAN(left) / den)));
     }
 
     Node result = rewriter::mkConst(inverse(den));
-    Node mult = NodeManager::currentNM()->mkNode(kind::MULT, left, result);
+    Node mult =
+        ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result));
     if (pre)
     {
       return RewriteResponse(REWRITE_DONE, mult);
     }
-    else
-    {
-      return RewriteResponse(REWRITE_AGAIN, mult);
-    }
+    // requires again full since ensureReal may have added a to_real
+    return RewriteResponse(REWRITE_AGAIN_FULL, mult);
+  }
+  Node ret = nm->mkNode(t.getKind(), left, right);
+  return RewriteResponse(REWRITE_DONE, ret);
+}
+
+RewriteResponse ArithRewriter::rewriteToReal(TNode t)
+{
+  Assert(t.getKind() == kind::CAST_TO_REAL || t.getKind() == kind::TO_REAL);
+  if (!t[0].getType().isInteger())
+  {
+    // if it is already real type, then just return the argument
+    return RewriteResponse(REWRITE_DONE, t[0]);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  if (t[0].isConst())
+  {
+    // If the argument is constant, return a real constant.
+    // !!!! Note that this does not preserve the type of t, since rat is
+    // an integral rational. This will be corrected when the type rule for
+    // CONST_RATIONAL is changed to always return Real.
+    const Rational& rat = t[0].getConst<Rational>();
+    return RewriteResponse(REWRITE_DONE, nm->mkConstReal(rat));
   }
+  // CAST_TO_REAL is our way of marking integral constants coming from the
+  // user as Real. It should only be applied to constants, which is handled
+  // above.
+  Assert(t.getKind() != kind::CAST_TO_REAL);
   return RewriteResponse(REWRITE_DONE, t);
 }
 
@@ -759,6 +808,11 @@ RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
     Node ret = isPred ? nm->mkConst(false) : nm->mkConstReal(Rational(3));
     return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
   }
+  else if (t[0].getKind() == kind::TO_REAL)
+  {
+    Node ret = nm->mkNode(t.getKind(), t[0][0]);
+    return returnRewrite(t, ret, Rewrite::INT_EXT_TO_REAL);
+  }
   return RewriteResponse(REWRITE_DONE, t);
 }
 
@@ -884,12 +938,12 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
         const Rational& rat = t[0].getConst<Rational>();
         if (rat.sgn() == 0)
         {
-          return RewriteResponse(REWRITE_DONE, rewriter::mkConst(Integer(0)));
+          return RewriteResponse(REWRITE_DONE, nm->mkConstReal(Rational(0)));
         }
         else if (rat.sgn() == -1)
         {
-          Node ret = nm->mkNode(
-              kind::NEG, nm->mkNode(kind::SINE, rewriter::mkConst(-rat)));
+          Node ret = nm->mkNode(kind::NEG,
+                                nm->mkNode(kind::SINE, nm->mkConstReal(-rat)));
           return RewriteResponse(REWRITE_AGAIN_FULL, ret);
         }
       }
@@ -965,6 +1019,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
             {
               new_arg = nm->mkNode(kind::ADD, new_arg, rem);
             }
+            new_arg = ensureReal(new_arg);
             // sin( 2*n*PI + x ) = sin( x )
             return RewriteResponse(REWRITE_AGAIN_FULL,
                                    nm->mkNode(kind::SINE, new_arg));
@@ -994,8 +1049,8 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
             if (r_abs.getDenominator() == two)
             {
               Assert(r_abs.getNumerator() == one);
-              return RewriteResponse(REWRITE_DONE,
-                                     nm->mkConstReal(Rational(r.sgn())));
+              return RewriteResponse(
+                  REWRITE_DONE, ensureReal(nm->mkConstReal(Rational(r.sgn()))));
             }
             else if (r_abs.getDenominator() == six)
             {
@@ -1070,6 +1125,40 @@ TrustNode ArithRewriter::expandDefinition(Node node)
   return ret;
 }
 
+TNode ArithRewriter::removeToReal(TNode t)
+{
+  return t.getKind() == kind::TO_REAL ? t[0] : t;
+}
+
+Node ArithRewriter::maybeEnsureReal(TypeNode tn, TNode t)
+{
+  // if we require being a real
+  if (!tn.isInteger())
+  {
+    // ensure that t has type real
+    Assert(tn.isReal());
+    return ensureReal(t);
+  }
+  return t;
+}
+
+Node ArithRewriter::ensureReal(TNode t)
+{
+  if (t.getType().isInteger())
+  {
+    if (t.isConst())
+    {
+      // short-circuit
+      Node ret = NodeManager::currentNM()->mkConstReal(t.getConst<Rational>());
+      Assert(ret.getType().isReal());
+      return ret;
+    }
+    Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl;
+    return NodeManager::currentNM()->mkNode(kind::TO_REAL, t);
+  }
+  return t;
+}
+
 RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
 {
   Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by "

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 0f2a55f842e016d14464d1281fc90aad9f1e6fa2..3da45fead96001649dead5c5f04cc5592ac013b6 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -40,7 +40,6 @@ class ArithRewriter : public TheoryRewriter
    * the given node.
    */
   TrustNode expandDefinition(Node node) override;
-
  private:
   /** preRewrite for atoms */
   static RewriteResponse preRewriteAtom(TNode t);
@@ -72,6 +71,8 @@ class ArithRewriter : public TheoryRewriter
 
   /** rewrite division */
   static RewriteResponse rewriteDiv(TNode t, bool pre);
+  /** rewrite to_real */
+  static RewriteResponse rewriteToReal(TNode t);
   /** rewrite absolute */
   static RewriteResponse rewriteAbs(TNode t);
   /** rewrite integer division and modulus */
@@ -93,6 +94,17 @@ class ArithRewriter : public TheoryRewriter
 
   /** return rewrite */
   static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r);
+  /**
+   * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL.
+   */
+  static TNode removeToReal(TNode t);
+  /**
+   * Ensure that t has real type if tn is the real type. Do so by applying
+   * TO_REAL to t.
+   */
+  static Node maybeEnsureReal(TypeNode tn, TNode t);
+  /** Same as above, without a check for the type of tn. */
+  static Node ensureReal(TNode t);
   /** The operator elimination utility */
   OperatorElim& d_opElim;
 }; /* class ArithRewriter */

diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp
index 0d31d734fb6b645fd60eb2d35744fda0b6e05cce..8a6d535c98ded3589612fe1e4c1bc7131dbfe2a3 100644 (file)
--- a/src/theory/arith/linear/theory_arith_private.cpp
+++ b/src/theory/arith/linear/theory_arith_private.cpp
@@ -3823,6 +3823,8 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
   Theory::shared_terms_iterator shared_end = d_containing.shared_terms_end();
   for(; shared_iter != shared_end; ++shared_iter){
     Node sharedCurr = *shared_iter;
+    sharedCurr =
+        sharedCurr.getKind() == kind::TO_REAL ? sharedCurr[0] : sharedCurr;
 
     // ModelException is fatal as this point. Don't catch!
     // DeltaRationalException is fatal as this point. Don't catch!

diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp
index cd6510a6b46970cad0af6ae9c95fdde12ac9a191..f12124a4e52016e931d6156b0ef9abf701d019bf 100644 (file)
--- a/src/theory/arith/rewriter/rewrite_atom.cpp
+++ b/src/theory/arith/rewriter/rewrite_atom.cpp
@@ -226,11 +226,13 @@ std::optional<bool> tryEvaluateRelation(Kind rel, TNode left, TNode right)
   return {};
 }
 
-std::optional<bool> tryEvaluateRelationReflexive(TNode atom)
+std::optional<bool> tryEvaluateRelationReflexive(Kind rel,
+                                                 TNode left,
+                                                 TNode right)
 {
-  if (atom.getNumChildren() == 2 && atom[0] == atom[1])
+  if (left == right)
   {
-    switch (atom.getKind())
+    switch (rel)
     {
       case Kind::LT: return false;
       case Kind::LEQ: return true;
@@ -352,4 +354,4 @@ Node buildRealInequality(Sum&& sum, Kind k)
 }  // namespace rewriter
 }  // namespace arith
 }  // namespace theory
-}  // namespace cvc5::internal
\ No newline at end of file
+}  // namespace cvc5::internal

diff --git a/src/theory/arith/rewriter/rewrite_atom.h b/src/theory/arith/rewriter/rewrite_atom.h
index 68c8cd564938d3584a3327a7dcfd5d0a5ede38c3..e5ffdba93fd6716f03a0462c601dd6f237371004 100644 (file)
--- a/src/theory/arith/rewriter/rewrite_atom.h
+++ b/src/theory/arith/rewriter/rewrite_atom.h
@@ -41,7 +41,9 @@ std::optional<bool> tryEvaluateRelation(Kind rel, TNode left, TNode right);
  * not identical).
  * Assumes atom to be a relational operator, i.e. one of <,<=,=,!=,>=,>.
  */
-std::optional<bool> tryEvaluateRelationReflexive(TNode atom);
+std::optional<bool> tryEvaluateRelationReflexive(Kind rel,
+                                                 TNode left,
+                                                 TNode right);
 
 /**
  * Build a node `(kind left right)`. If negate is true, it returns the negation

diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp
index 51a50fbdc4a144628000f5047471e419bfe2aa27..4e2d6fb3318fa2dbfeeedc3d352effaabc7f3ed7 100644 (file)
--- a/src/theory/arith/rewrites.cpp
+++ b/src/theory/arith/rewrites.cpp
@@ -39,6 +39,7 @@ const char* toString(Rewrite r)
     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";
+    case Rewrite::INT_EXT_TO_REAL: return "INT_EXT_TO_REAL";
     default: return "?";
   }
 }

diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h
index 8e198c53da0bd7c8abdc5c574704864649d230c0..be90f24177ead4a393c75895e509bf090689ecde 100644 (file)
--- a/src/theory/arith/rewrites.h
+++ b/src/theory/arith/rewrites.h
@@ -59,7 +59,9 @@ enum class Rewrite : uint32_t
   // (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
+  INT_EXT_PI,
+  // (to_int (to_real x)) --> (to_int x), (is_int (to_real x)) --> (is_int x)
+  INT_EXT_TO_REAL
 };
 
 /**

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index fe04a9c2632644b0d47990e97d6ba3233c3370bb..c1cdef9f14bb34deaed867919ce1249f6e8c34b3 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -121,7 +121,11 @@ void TheoryArith::preRegisterTerm(TNode n)
   d_internal->preRegisterTerm(n);
 }
 
-void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
+void TheoryArith::notifySharedTerm(TNode n)
+{
+  n = n.getKind() == kind::TO_REAL ? n[0] : n;
+  d_internal->notifySharedTerm(n);
+}
 
 TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 {
@@ -352,6 +356,7 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheoryArith::getModelValue(TNode var) {
+  var = var.getKind() == kind::TO_REAL ? var[0] : var;
   std::map<Node, Node>::iterator it = d_arithModelCache.find(var);
   if (it != d_arithModelCache.end())
   {

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 3acc0b76a4f0864123ad3163d8c8f80424ea8224..ab03ba3953731fce8a0180d00708ad3f91546933 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -520,6 +520,7 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(x.abs());
           break;
         }
+        case kind::TO_REAL:
         case kind::CAST_TO_REAL:
         {
           // casting to real is a no-op
@@ -527,6 +528,19 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(x);
           break;
         }
+        case kind::TO_INTEGER:
+        {
+          // casting to int takes the floor
+          const Rational& x = results[currNode[0]].d_rat.floor();
+          results[currNode] = EvalResult(x);
+          break;
+        }
+        case kind::IS_INTEGER:
+        {
+          const Rational& x = results[currNode[0]].d_rat;
+          results[currNode] = EvalResult(x.isIntegral());
+          break;
+        }
         case kind::CONST_STRING:
           results[currNode] = EvalResult(currNodeVal.getConst<String>());
           break;

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index d8119e45f90bca70595cb6ca209774b05f4f3868..40e07fb55590dd9550a6ec1dd2976b925b0254e1 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -904,10 +904,13 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
       int ires_use =
           (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
                                                                           : -1;
-      val = rewrite(
-          nm->mkNode(ires_use == -1 ? ADD : SUB,
-                     nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart),
-                     nm->mkNode(TO_INTEGER, realPart)));
+      val = nm->mkNode(ires_use == -1 ? ADD : SUB,
+                       nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart),
+                       nm->mkNode(TO_INTEGER, realPart));
+      Trace("cegqi-arith-debug")
+          << "result (pre-rewrite) : " << val << std::endl;
+      val = rewrite(val);
+      val = val.getKind() == TO_REAL ? val[0] : val;
       // could round up for upper bounds here
       Trace("cegqi-arith-debug") << "result : " << val << std::endl;
       Assert(val.getType().isInteger());

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index dbb6c6acc850d2f92aeecd6a0a020817c45044ef..5320638bed9850ecca7471bbc7f81f490ac9ca5c 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -266,7 +266,7 @@ CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
       || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION
       || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
       || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER
-      || k == IS_INTEGER)
+      || k == IS_INTEGER || k == TO_REAL)
   {
     return CEG_HANDLED;
   }

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 4c6eac6eb3f0eaf563c89f350f17e12dc2680bf9..503ee4c2c4b275f69faaa5effe92e613093fff5c 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -954,6 +954,11 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     doCheck( fm, f, d, n[0] );
     doNegate( d );
   }
+  else if (n.getKind() == kind::TO_REAL)
+  {
+    // no-op
+    doCheck(fm, f, d, n[0]);
+  }
   else if( n.getKind() == kind::FORALL ){
     d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4177631234a1abcf630dde9c7f3857864b852fd7..174d448eed1d3529d9e374e1665a16bb155c19c0 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -778,6 +778,7 @@ set(regress_0_tests
   regress0/nl/all-logic.smt2
   regress0/nl/coeff-sat.smt2
   regress0/nl/combined-uf.smt2
+  regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2
   regress0/nl/iand-no-init.smt2
   regress0/nl/issue3003.smt2
   regress0/nl/issue3407.smt2

diff --git a/test/regress/cli/regress0/arith/bug549.cvc.smt2 b/test/regress/cli/regress0/arith/bug549.cvc.smt2
index 8a62b70647c657346ee3cf8cfbf64bc6a9884035..74bdc88781ca6e5b96d5151e991de57f6555201f 100644 (file)
--- a/test/regress/cli/regress0/arith/bug549.cvc.smt2
+++ b/test/regress/cli/regress0/arith/bug549.cvc.smt2
@@ -3,4 +3,4 @@
 (set-option :incremental false)
 (declare-fun a () Real)
 (declare-fun b () Real)
-(check-sat-assuming ( (not (= (^ (* a b) 5.0) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) ))
+(check-sat-assuming ( (not (= (^ (* a b) 5) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) ))

diff --git a/test/regress/cli/regress0/bug339.smt2 b/test/regress/cli/regress0/bug339.smt2
index bb03cf9b17044ce8d53444296a115b426422e191..6252aa322aab7fbb8f4d0bff3c45a3309e494709 100644 (file)
--- a/test/regress/cli/regress0/bug339.smt2
+++ b/test/regress/cli/regress0/bug339.smt2
@@ -5,7 +5,7 @@
 (declare-fun P () Bool)
 
 (assert
- (let ((y (ite P 1 x)))
+ (let ((y (ite P 1.0 x)))
    (and (not (= y 1))
         (> y 0)
         (<= y 1))))

diff --git a/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2 b/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2
new file mode 100644 (file)
index 0000000..abc6941
--- /dev/null
+++ b/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_UFNRA)
+(set-info :status sat)
+(declare-fun f (Real) Real)
+(declare-fun p (Real Real Real) Bool)
+(check-sat-assuming ((= 0.0 (/ 1 (ite (p 0.0 0.0 (/ (ite (p 0.0 0.0 (f 0.0)) 1 0) 1)) 1 0)))))

diff --git a/test/regress/cli/regress0/quantifiers/mix-match.smt2 b/test/regress/cli/regress0/quantifiers/mix-match.smt2
index d123bf9c4751765ed7f180238f36e5a7921b5ea6..a7fc077ded0c0621537f9ff50392840f92ec054a 100644 (file)
--- a/test/regress/cli/regress0/quantifiers/mix-match.smt2
+++ b/test/regress/cli/regress0/quantifiers/mix-match.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --enum-inst
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)