From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 18:16:20 +0000 (-0600)
Subject: Improve error message when not using strings-exp (#8203)
X-Git-Tag: cvc5-1.0.0~344
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d07ce1107a4431e4d3e584ae731fe19b51c19631;p=cvc5.git

Improve error message when not using strings-exp (#8203)

Fixes #6005.

Also improves smt2 printing of sequences so that we print the compliant kinds, which is work towards cvc5/cvc5-wishues#106.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f3078a450..773d5fd4b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -953,7 +953,7 @@ void Smt2Printer::toStream(std::ostream& out,
       if(forceBinary && i < n.getNumChildren() - 1) {
         // not going to work properly for parameterized kinds!
         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
+        out << " (" << smtKindStringOf(n, d_variant) << ' ';
         parens << ')';
         ++c;
       } else {
@@ -1269,6 +1269,35 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   return kind::kindToString(k);
 }
 
+std::string Smt2Printer::smtKindStringOf(const Node& n, Variant v)
+{
+  Kind k = n.getKind();
+  if (n.getNumChildren() > 0 && n[0].getType().isSequence())
+  {
+    // this method parallels api::Term::getKind
+    switch (k)
+    {
+      case kind::STRING_CONCAT: return "seq.concat";
+      case kind::STRING_LENGTH: return "seq.len";
+      case kind::STRING_SUBSTR: return "seq.extract";
+      case kind::STRING_UPDATE: return "seq.update";
+      case kind::STRING_CHARAT: return "seq.at";
+      case kind::STRING_CONTAINS: return "seq.contains";
+      case kind::STRING_INDEXOF: return "seq.indexof";
+      case kind::STRING_REPLACE: return "seq.replace";
+      case kind::STRING_REPLACE_ALL: return "seq.replace_all";
+      case kind::STRING_REV: return "seq.rev";
+      case kind::STRING_PREFIX: return "seq.prefixof";
+      case kind::STRING_SUFFIX: return "seq.suffixof";
+      default:
+        // fall through to conversion below
+        break;
+    }
+  }
+  // by default
+  return smtKindString(k, v);
+}
+
 void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const
 {
   // we currently must call TypeNode::toStream here.
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index bf6c20d40..4170fe88f 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -256,6 +256,11 @@ class Smt2Printer : public cvc5::Printer
    * the SMT-LIB format (with variant v).
    */
   static std::string smtKindString(Kind k, Variant v = smt2_6_variant);
+  /**
+   * Same as above, but also takes into account the type of the node, which
+   * makes a difference for printing sequences.
+   */
+  static std::string smtKindStringOf(const Node& n, Variant v = smt2_6_variant);
   /**
    * Get the string corresponding to the sygus datatype t printed as a grammar.
    */
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index fff869c7d..84a290f3c 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -18,6 +18,7 @@
 #include "expr/attribute.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
+#include "printer/smt2/smt2_printer.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
 #include "theory/strings/inference_manager.h"
@@ -162,7 +163,7 @@ void TermRegistry::preRegisterTerm(TNode n)
         || k == STRING_UPDATE)
     {
       std::stringstream ss;
-      ss << "Term of kind " << k
+      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindStringOf(n)
          << " not supported in default mode, try --strings-exp";
       throw LogicException(ss.str());
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 043994368..a4921e5c9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1170,6 +1170,7 @@ set(regress_0_tests
   regress0/seq/array/nth-concat.smt2
   regress0/seq/array/update-fallback.smt2
   regress0/seq/array/update-word-eq.smt2
+  regress0/seq/issue6005-no-strings-exp.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2
diff --git a/test/regress/regress0/seq/issue6005-no-strings-exp.smt2 b/test/regress/regress0/seq/issue6005-no-strings-exp.smt2
new file mode 100644
index 000000000..54f552095
--- /dev/null
+++ b/test/regress/regress0/seq/issue6005-no-strings-exp.smt2
@@ -0,0 +1,6 @@
+; EXPECT: (error "Term of kind seq.extract not supported in default mode, try --strings-exp")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun x () (Seq Int))
+(assert (not (= x (seq.extract x 4 7))))
+(check-sat)