From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 30 May 2019 18:05:42 +0000 (-0700)
Subject: Quote symbol when printing empty symbol name (#3025)
X-Git-Tag: cvc5-1.0.0~4136
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be2a85f84fec4e926704f4788c55ec2ba805de39;p=cvc5.git

Quote symbol when printing empty symbol name (#3025)

When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 380004d02..66d36fe4c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -91,7 +91,11 @@ void Smt2Printer::toStream(
 
 static std::string maybeQuoteSymbol(const std::string& s) {
   // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
-  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
+  if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
+                          "0123456789~!@$%^&*_-+=<>.?/")
+          != string::npos
+      || s.empty())
+  {
     // need to quote it
     stringstream ss;
     ss << '|' << s << '|';
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 261f8e19c..c39d96351 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -585,6 +585,7 @@ set(regress_0_tests
   regress0/print_lambda.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
+  regress0/printer/empty_symbol_name.smt2
   regress0/printer/tuples_and_records.cvc
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2
new file mode 100644
index 000000000..46652bc24
--- /dev/null
+++ b/test/regress/regress0/printer/empty_symbol_name.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; EXPECT: ((|| (_ bv1 4)))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const || (_ BitVec 4))
+(assert (= || #b0001))
+(check-sat)
+(get-value (||))