From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 22 May 2022 00:02:54 +0000 (-0500)
Subject: Simplification of smt2 printer for type ascriptions (#8801)
X-Git-Tag: cvc5-1.0.1~107
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ec53e32461be0bff598a538633d120adb91862c;p=cvc5.git

Simplification of smt2 printer for type ascriptions (#8801)

Previously had code for dealing with subtypes
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 519d67fc1..ec29595e7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -488,52 +488,14 @@ void Smt2Printer::toStream(std::ostream& out,
     return;
   }
 
-  // determine if we are printing out a type ascription, store the argument of
-  // the type ascription into type_asc_arg.
-  Node type_asc_arg;
-  TypeNode force_nt;
+  // determine if we are printing out a type ascription
   if (k == kind::APPLY_TYPE_ASCRIPTION)
   {
-    force_nt = n.getOperator().getConst<AscriptionType>().getType();
-    type_asc_arg = n[0];
-  }
-  if (!type_asc_arg.isNull())
-  {
-    if (force_nt.isRealOrInt())
-    {
-      // we prefer using (/ x 1) instead of (to_real x) here.
-      // the reason is that (/ x 1) is SMT-LIB compliant when x is a constant
-      // or the logic is non-linear, whereas (to_real x) is compliant when
-      // the logic is mixed int/real. The former occurs more frequently.
-      bool is_int = force_nt.isInteger();
-      // If constant rational, print as special case
-      Kind ka = type_asc_arg.getKind();
-      if (ka == kind::CONST_RATIONAL || ka == kind::CONST_INTEGER)
-      {
-        const Rational& r = type_asc_arg.getConst<Rational>();
-        toStreamRational(out, r, !is_int, d_variant);
-      }
-      else
-      {
-        out << "("
-            << smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION,
-                             d_variant)
-            << " ";
-        toStream(out, type_asc_arg, toDepth, lbind);
-        if (!is_int)
-        {
-          out << " 1";
-        }
-        out << ")";
-      }
-    }
-    else if (k != kind::UNINTERPRETED_SORT_VALUE)
-    {
-      // use type ascription
-      out << "(as ";
-      toStream(out, type_asc_arg, toDepth < 0 ? toDepth : toDepth - 1, lbind);
-      out << " " << force_nt << ")";
-    }
+    TypeNode typeAsc = n.getOperator().getConst<AscriptionType>().getType();
+    // use type ascription
+    out << "(as ";
+    toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, lbind);
+    out << " " << typeAsc << ")";
     return;
   }