From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 26 Feb 2021 18:47:05 +0000 (-0600)
Subject: Minor improvement and fix to smt2 printer (#6009)
X-Git-Tag: cvc5-1.0.0~2204
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3453595e9f5d76a62b113b3a5d13a60dc09ce3ee;p=cvc5.git

Minor improvement and fix to smt2 printer (#6009)

This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bc4ea16de..c7962417a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -50,8 +50,6 @@ namespace smt2 {
 
 static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k, Variant v);
-
 /** returns whether the variant is smt-lib 2.6 or greater */
 bool isVariant_2_6(Variant v) { return v == smt2_6_variant; }
 
@@ -1066,7 +1064,7 @@ void Smt2Printer::toStreamCastToType(std::ostream& out,
   toStream(out, nasc, toDepth);
 }
 
-static string smtKindString(Kind k, Variant v)
+std::string Smt2Printer::smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
@@ -1292,7 +1290,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_STOI: return "str.to_int";
   case kind::STRING_IN_REGEXP: return "str.in_re";
   case kind::STRING_TO_REGEXP: return "str.to_re";
-  case kind::REGEXP_EMPTY: return "re.nostr";
+  case kind::REGEXP_EMPTY: return "re.none";
   case kind::REGEXP_SIGMA: return "re.allchar";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 6ed0938f8..8934967b9 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -223,6 +223,12 @@ class Smt2Printer : public CVC4::Printer
   void toStreamCmdDeclarationSequence(
       std::ostream& out, const std::vector<Command*>& sequence) const override;
 
+  /**
+   * Get the string for a kind k, which returns how the kind k is printed in
+   * the SMT-LIB format (with variant v).
+   */
+  static std::string smtKindString(Kind k, Variant v = smt2_6_variant);
+
  private:
   /**
    * The main printing method for nodes n.