Simplify smt2 printer (#6954)

The common case of printing function applications is to print the kind in smt2 format, this makes this the default case and removes spurious cases. It also makes a few minor fixes.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bf26b80ee938a537e725cf8da1e24bfc114f6584..c51d00b5dea7efad965b87d002296635bdd7f466 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -566,194 +566,91 @@ void Smt2Printer::toStream(std::ostream& out,
   }
   switch(k) {
     // builtin theory
-  case kind::EQUAL:
-  case kind::DISTINCT:
-    out << smtKindString(k, d_variant) << " ";
-    break;
-  case kind::FUNCTION_TYPE:
-    out << "->";
-    for (Node nc : n)
-    {
-      out << " ";
-      toStream(out, nc, toDepth);
-    }
-    out << ")";
-    return;
-  case kind::SEXPR: break;
-
-    // bool theory
-  case kind::NOT:
-  case kind::AND:
-  case kind::IMPLIES:
-  case kind::OR:
-  case kind::XOR:
-  case kind::ITE:
-    out << smtKindString(k, d_variant) << " ";
-    break;
+    case kind::FUNCTION_TYPE:
+      out << "->";
+      for (Node nc : n)
+      {
+        out << " ";
+        toStream(out, nc, toDepth);
+      }
+      out << ")";
+      return;
+    case kind::SEXPR: break;
 
-  // uf theory
-  case kind::APPLY_UF: break;
-  // higher-order
-  case kind::HO_APPLY:
-    if (!options::flattenHOChains())
-    {
-      break;
-    }
-    // collapse "@" chains, i.e.
-    //
-    // ((a b) c) --> (a b c)
-    //
-    // (((a b) ((c d) e)) f) --> (a b (c d e) f)
-    {
-      Node head = n;
-      std::vector<Node> args;
-      while (head.getKind() == kind::HO_APPLY)
+    // uf theory
+    case kind::APPLY_UF: break;
+    // higher-order
+    case kind::HO_APPLY:
+      if (!options::flattenHOChains())
       {
-        args.insert(args.begin(), head[1]);
-        head = head[0];
+        break;
       }
-      toStream(out, head, toDepth, lbind);
-      for (unsigned i = 0, size = args.size(); i < size; ++i)
+      // collapse "@" chains, i.e.
+      //
+      // ((a b) c) --> (a b c)
+      //
+      // (((a b) ((c d) e)) f) --> (a b (c d e) f)
       {
-        out << " ";
-        toStream(out, args[i], toDepth, lbind);
+        Node head = n;
+        std::vector<Node> args;
+        while (head.getKind() == kind::HO_APPLY)
+        {
+          args.insert(args.begin(), head[1]);
+          head = head[0];
+        }
+        toStream(out, head, toDepth, lbind);
+        for (unsigned i = 0, size = args.size(); i < size; ++i)
+        {
+          out << " ";
+          toStream(out, args[i], toDepth, lbind);
+        }
+        out << ")";
       }
-      out << ")";
-    }
-    return;
+      return;
 
-  case kind::MATCH:
-    out << smtKindString(k, d_variant) << " ";
-    toStream(out, n[0], toDepth, lbind);
-    out << " (";
-    for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
-    {
-      if (i > 1)
+    case kind::MATCH:
+      out << smtKindString(k, d_variant) << " ";
+      toStream(out, n[0], toDepth, lbind);
+      out << " (";
+      for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
       {
-        out << " ";
+        if (i > 1)
+        {
+          out << " ";
+        }
+        toStream(out, n[i], toDepth, lbind);
       }
-      toStream(out, n[i], toDepth, lbind);
-    }
-    out << "))";
-    return;
-  case kind::MATCH_BIND_CASE:
-    // ignore the binder
-    toStream(out, n[1], toDepth, lbind);
-    out << " ";
-    toStream(out, n[2], toDepth, lbind);
-    out << ")";
-    return;
-  case kind::MATCH_CASE:
-    // do nothing
-    break;
+      out << "))";
+      return;
+    case kind::MATCH_BIND_CASE:
+      // ignore the binder
+      toStream(out, n[1], toDepth, lbind);
+      out << " ";
+      toStream(out, n[2], toDepth, lbind);
+      out << ")";
+      return;
+    case kind::MATCH_CASE:
+      // do nothing
+      break;
 
-  // arith theory
-  case kind::PLUS:
-  case kind::MULT:
-  case kind::NONLINEAR_MULT:
-  case kind::EXPONENTIAL:
-  case kind::SINE:
-  case kind::COSINE:
-  case kind::TANGENT:
-  case kind::COSECANT:
-  case kind::SECANT:
-  case kind::COTANGENT:
-  case kind::ARCSINE:
-  case kind::ARCCOSINE:
-  case kind::ARCTANGENT:
-  case kind::ARCCOSECANT:
-  case kind::ARCSECANT:
-  case kind::ARCCOTANGENT:
-  case kind::PI:
-  case kind::SQRT:
-  case kind::MINUS:
-  case kind::UMINUS:
-  case kind::LT:
-  case kind::LEQ:
-  case kind::GT:
-  case kind::GEQ:
-  case kind::DIVISION:
-  case kind::DIVISION_TOTAL:
-  case kind::INTS_DIVISION:
-  case kind::INTS_DIVISION_TOTAL:
-  case kind::INTS_MODULUS:
-  case kind::INTS_MODULUS_TOTAL:
-  case kind::ABS:
-  case kind::IS_INTEGER:
-  case kind::TO_INTEGER:
-  case kind::TO_REAL:
-  case kind::POW:
-  case kind::POW2: out << smtKindString(k, d_variant) << " "; break;
-  case kind::IAND:
-    out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
-    stillNeedToPrintParams = false;
-    break;
+    // arith theory
+    case kind::IAND:
+      out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
+      stillNeedToPrintParams = false;
+      break;
 
-  case kind::DIVISIBLE:
-    out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
-    stillNeedToPrintParams = false;
-    break;
-  case kind::INDEXED_ROOT_PREDICATE_OP:
-  {
-    const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
-    out << "(_ root_predicate " << irp.d_index << ")";
-    break;
+    case kind::DIVISIBLE:
+      out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
+      stillNeedToPrintParams = false;
+      break;
+    case kind::INDEXED_ROOT_PREDICATE_OP:
+    {
+      const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
+      out << "(_ root_predicate " << irp.d_index << ")";
+      break;
   }
 
-    // arrays theory
-  case kind::SELECT:
-  case kind::STORE:
-  case kind::PARTIAL_SELECT_0:
-  case kind::PARTIAL_SELECT_1:
-  case kind::ARRAY_TYPE:
-  case kind::EQ_RANGE: out << smtKindString(k, d_variant) << " "; break;
-
   // string theory
-  case kind::STRING_CONCAT:
-    out << "str.++ ";
-    break;
-  case kind::STRING_IN_REGEXP: {
-    stringstream ss;
-    out << smtKindString(k, d_variant) << " ";
-    break;
-  }
-  case kind::STRING_LENGTH:
-  case kind::STRING_SUBSTR:
-  case kind::STRING_UPDATE:
-  case kind::STRING_CHARAT:
-  case kind::STRING_CONTAINS:
-  case kind::STRING_INDEXOF:
-  case kind::STRING_INDEXOF_RE:
-  case kind::STRING_REPLACE:
-  case kind::STRING_REPLACE_ALL:
-  case kind::STRING_REPLACE_RE:
-  case kind::STRING_REPLACE_RE_ALL:
-  case kind::STRING_TOLOWER:
-  case kind::STRING_TOUPPER:
-  case kind::STRING_REV:
-  case kind::STRING_PREFIX:
-  case kind::STRING_SUFFIX:
-  case kind::STRING_LEQ:
-  case kind::STRING_LT:
-  case kind::STRING_ITOS:
-  case kind::STRING_STOI:
-  case kind::STRING_FROM_CODE:
-  case kind::STRING_TO_CODE:
-  case kind::STRING_TO_REGEXP:
-  case kind::REGEXP_CONCAT:
-  case kind::REGEXP_UNION:
-  case kind::REGEXP_INTER:
-  case kind::REGEXP_STAR:
-  case kind::REGEXP_PLUS:
-  case kind::REGEXP_OPT:
-  case kind::REGEXP_RANGE:
-  case kind::REGEXP_COMPLEMENT:
-  case kind::REGEXP_DIFF:
-  case kind::REGEXP_EMPTY:
-  case kind::REGEXP_SIGMA:
-  case kind::SEQ_UNIT:
-  case kind::SEQ_NTH:
-  case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break;
   case kind::REGEXP_REPEAT:
   case kind::REGEXP_LOOP:
   {
@@ -766,41 +663,17 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
 
     // bv theory
-  case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break;
-  case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break;
-  case kind::BITVECTOR_OR: out << "bvor "; forceBinary = true; break;
-  case kind::BITVECTOR_XOR: out << "bvxor "; forceBinary = true; break;
-  case kind::BITVECTOR_NOT: out << "bvnot "; break;
-  case kind::BITVECTOR_NAND: out << "bvnand "; break;
-  case kind::BITVECTOR_NOR: out << "bvnor "; break;
-  case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
-  case kind::BITVECTOR_COMP: out << "bvcomp "; break;
-  case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break;
+  case kind::BITVECTOR_CONCAT:
+  case kind::BITVECTOR_AND:
+  case kind::BITVECTOR_OR:
+  case kind::BITVECTOR_XOR:
+  case kind::BITVECTOR_MULT:
   case kind::BITVECTOR_ADD:
-    out << "bvadd ";
+  {
+    out << smtKindString(k, d_variant) << " ";
     forceBinary = true;
-    break;
-  case kind::BITVECTOR_SUB: out << "bvsub "; break;
-  case kind::BITVECTOR_NEG: out << "bvneg "; break;
-  case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
-  case kind::BITVECTOR_UREM: out << "bvurem "; break;
-  case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
-  case kind::BITVECTOR_SREM: out << "bvsrem "; break;
-  case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
-  case kind::BITVECTOR_SHL: out << "bvshl "; break;
-  case kind::BITVECTOR_LSHR: out << "bvlshr "; break;
-  case kind::BITVECTOR_ASHR: out << "bvashr "; break;
-  case kind::BITVECTOR_ULT: out << "bvult "; break;
-  case kind::BITVECTOR_ULE: out << "bvule "; break;
-  case kind::BITVECTOR_UGT: out << "bvugt "; break;
-  case kind::BITVECTOR_UGE: out << "bvuge "; break;
-  case kind::BITVECTOR_SLT: out << "bvslt "; break;
-  case kind::BITVECTOR_SLE: out << "bvsle "; break;
-  case kind::BITVECTOR_SGT: out << "bvsgt "; break;
-  case kind::BITVECTOR_SGE: out << "bvsge "; break;
-  case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
-  case kind::BITVECTOR_REDOR: out << "bvredor "; break;
-  case kind::BITVECTOR_REDAND: out << "bvredand "; break;
+  }
+  break;
 
   case kind::BITVECTOR_EXTRACT:
   case kind::BITVECTOR_REPEAT:
@@ -814,19 +687,7 @@ void Smt2Printer::toStream(std::ostream& out,
     stillNeedToPrintParams = false;
     break;
 
-    // sets
-  case kind::UNION:
-  case kind::INTERSECTION:
-  case kind::SETMINUS:
-  case kind::SUBSET:
-  case kind::CARD:
-  case kind::JOIN:
-  case kind::PRODUCT:
-  case kind::TRANSPOSE:
-  case kind::TCLOSURE:
-  case kind::IDEN:
-  case kind::JOIN_IMAGE: out << smtKindString(k, d_variant) << " "; break;
-  case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
+  // sets
   case kind::SINGLETON:
   {
     out << smtKindString(k, d_variant) << " ";
@@ -837,29 +698,9 @@ void Smt2Printer::toStream(std::ostream& out,
     return;
   }
   break;
-  case kind::MEMBER:
-  case kind::INSERT:
-  case kind::SET_TYPE:
-  case kind::COMPLEMENT:
-  case kind::CHOOSE:
-  case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
   // bags
-  case kind::BAG_TYPE:
-  case kind::UNION_MAX:
-  case kind::UNION_DISJOINT:
-  case kind::INTERSECTION_MIN:
-  case kind::DIFFERENCE_SUBTRACT:
-  case kind::DIFFERENCE_REMOVE:
-  case kind::SUBBAG:
-  case kind::BAG_COUNT:
-  case kind::DUPLICATE_REMOVAL:
-  case kind::BAG_CARD:
-  case kind::BAG_CHOOSE:
-  case kind::BAG_IS_SINGLETON:
-  case kind::BAG_FROM_SET:
-  case kind::BAG_TO_SET: out << smtKindString(k, d_variant) << " "; break;
   case kind::MK_BAG:
   {
     // print (bag (mkBag_op Real) 1 3) as (bag 1.0 3)
@@ -871,43 +712,7 @@ void Smt2Printer::toStream(std::ostream& out,
     return;
   }
 
-    // fp theory
-  case kind::FLOATINGPOINT_FP:
-  case kind::FLOATINGPOINT_EQ:
-  case kind::FLOATINGPOINT_ABS:
-  case kind::FLOATINGPOINT_NEG:
-  case kind::FLOATINGPOINT_ADD:
-  case kind::FLOATINGPOINT_SUB:
-  case kind::FLOATINGPOINT_MULT:
-  case kind::FLOATINGPOINT_DIV:
-  case kind::FLOATINGPOINT_FMA:
-  case kind::FLOATINGPOINT_SQRT:
-  case kind::FLOATINGPOINT_REM:
-  case kind::FLOATINGPOINT_RTI:
-  case kind::FLOATINGPOINT_MIN:
-  case kind::FLOATINGPOINT_MAX:
-  case kind::FLOATINGPOINT_LEQ:
-  case kind::FLOATINGPOINT_LT:
-  case kind::FLOATINGPOINT_GEQ:
-  case kind::FLOATINGPOINT_GT:
-  case kind::FLOATINGPOINT_ISN:
-  case kind::FLOATINGPOINT_ISSN:
-  case kind::FLOATINGPOINT_ISZ:
-  case kind::FLOATINGPOINT_ISINF:
-  case kind::FLOATINGPOINT_ISNAN:
-  case kind::FLOATINGPOINT_ISNEG:
-  case kind::FLOATINGPOINT_ISPOS:
-  case kind::FLOATINGPOINT_TO_REAL:
-  case kind::FLOATINGPOINT_COMPONENT_NAN:
-  case kind::FLOATINGPOINT_COMPONENT_INF:
-  case kind::FLOATINGPOINT_COMPONENT_ZERO:
-  case kind::FLOATINGPOINT_COMPONENT_SIGN:
-  case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
-  case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
-  case kind::ROUNDINGMODE_BITBLAST:
-    out << smtKindString(k, d_variant) << ' ';
-    break;
-
+  // fp theory
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
   case kind::FLOATINGPOINT_TO_FP_REAL:
@@ -991,11 +796,6 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::PARAMETRIC_DATATYPE: break;
 
   // separation logic
-  case kind::SEP_EMP:
-  case kind::SEP_PTO:
-  case kind::SEP_STAR:
-  case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
-
   case kind::SEP_NIL:
     out << "(as sep.nil " << n.getType() << ")";
     break;
@@ -1062,10 +862,9 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::INST_NO_PATTERN:
   case kind::INST_PATTERN_LIST: break;
   default:
-    // fall back on however the kind prints itself; this probably
-    // won't be SMT-LIB v2 compliant, but it will be clear from the
-    // output that support for the kind needs to be added here.
-    out << n.getKind() << ' ';
+    // by default, print the kind using the smtKindString utility
+    out << smtKindString(k, d_variant) << " ";
+    break;
   }
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
       stillNeedToPrintParams ) {
@@ -1236,6 +1035,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
   case kind::INT_TO_BITVECTOR: return "int2bv";
+  case kind::BITVECTOR_BB_TERM: return "bbT";
 
   // datatypes theory
   case kind::APPLY_TESTER: return "is";
@@ -1389,6 +1189,9 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
     ; /* fall through */
   }
 
+  // fall back on however the kind prints itself; this probably
+  // won't be SMT-LIB v2 compliant, but it will be clear from the
+  // output that support for the kind needs to be added here.
   // no SMT way to print these
   return kind::kindToString(k);
 }