Make more utilities distinguish Int and Real (#8626)

Towards eliminating arithmetic subtyping.

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 626e7a483e4f7916d49809509865d50f7a44c880..44bb709db6f6ca8a0aa3cf967308a86985cd82fc 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -106,8 +106,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
               {
                 if (!cc.isNull())
                 {
-                  c = rewrite(
-                      NodeManager::currentNM()->mkNode(kind::MULT, c, cc));
+                  c = nm->mkConstInt(c.getConst<Rational>()
+                                     * cc.getConst<Rational>());
                 }
               }
               Assert(c.getType().isInteger());

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9b5667c563ca743682091e8a886258560f524f6a..f45f5977acb59d2ad27cdc5735959948a3e05462 100644 (file)
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -122,6 +122,7 @@ void ArithStaticLearner::process(TNode n,
     break;
 
   case CONST_RATIONAL:
+  case CONST_INTEGER:
     // Mark constants as minmax
     d_minMap.insert(n, n.getConst<Rational>());
     d_maxMap.insert(n, n.getConst<Rational>());

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 6dac1305c3bd0b4cbb8bb142777a10e63945aa31..3acc0b76a4f0864123ad3163d8c8f80424ea8224 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -104,14 +104,16 @@ EvalResult::~EvalResult()
   }
 }
 
-Node EvalResult::toNode() const
+Node EvalResult::toNode(const TypeNode& tn) const
 {
   NodeManager* nm = NodeManager::currentNM();
   switch (d_tag)
   {
     case EvalResult::BOOL: return nm->mkConst(d_bool);
     case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
-    case EvalResult::RATIONAL: return nm->mkConst(CONST_RATIONAL, d_rat);
+    case EvalResult::RATIONAL:
+      Assert(!tn.isNull());
+      return nm->mkConstRealOrInt(tn, d_rat);
     case EvalResult::STRING: return nm->mkConst(d_str);
     case EvalResult::UVALUE: return nm->mkConst(d_av);
     default:
@@ -164,7 +166,8 @@ Node Evaluator::eval(TNode n,
     }
   }
   Trace("evaluator") << "Run eval internal..." << std::endl;
-  Node ret = evalInternal(n, args, vals, evalAsNode, results).toNode();
+  Node ret =
+      evalInternal(n, args, vals, evalAsNode, results).toNode(n.getType());
   // if we failed to evaluate
   if (ret.isNull() && d_rr != nullptr)
   {
@@ -348,7 +351,8 @@ EvalResult Evaluator::evalInternal(
 
           for (const auto& lambdaVal : currNode)
           {
-            lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode());
+            lambdaVals.insert(lambdaVals.begin(),
+                              results[lambdaVal].toNode(lambdaVal.getType()));
           }
 
           // Lambdas are evaluated in a recursive fashion because each
@@ -404,6 +408,7 @@ EvalResult Evaluator::evalInternal(
         }
 
         case kind::CONST_RATIONAL:
+        case kind::CONST_INTEGER:
         {
           const Rational& r = currNodeVal.getConst<Rational>();
           results[currNode] = EvalResult(r);
@@ -943,7 +948,7 @@ Node Evaluator::reconstruct(TNode n,
       else
       {
         // otherwise, use the evaluation of the operator
-        echildren.push_back(itr->second.toNode());
+        echildren.push_back(itr->second.toNode(op.getType()));
       }
     }
   }
@@ -961,7 +966,7 @@ Node Evaluator::reconstruct(TNode n,
     else
     {
       // otherwise, use the evaluation
-      echildren.push_back(itr->second.toNode());
+      echildren.push_back(itr->second.toNode(currNodeChild.getType()));
     }
   }
   // The value is the result of our (partially) successful evaluation

diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 45d598020dcad8c5f0926568aa782d4a1f60decb..31dc43e8bf18ddc15fd9215cd10f5fb67ae394e4 100644 (file)
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -75,9 +75,10 @@ struct EvalResult
 
   /**
    * Converts the result to a Node. If the result is not valid, this function
-   * returns the null node.
+   * returns the null node. This method takes a type to distinguish integer
+   * and real constants, which are both represented as RATIONAL results.
    */
-  Node toNode() const;
+  Node toNode(const TypeNode& tn) const;
 };
 
 class Rewriter;