From d07ce1107a4431e4d3e584ae731fe19b51c19631 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Mar 2022 12:16:20 -0600 Subject: [PATCH] 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. --- src/printer/smt2/smt2_printer.cpp | 31 ++++++++++++++++++- src/printer/smt2/smt2_printer.h | 5 +++ src/theory/strings/term_registry.cpp | 3 +- test/regress/CMakeLists.txt | 1 + .../seq/issue6005-no-strings-exp.smt2 | 6 ++++ 5 files changed, 44 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/seq/issue6005-no-strings-exp.smt2 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) -- 2.30.2