From 3453595e9f5d76a62b113b3a5d13a60dc09ce3ee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 26 Feb 2021 12:47:05 -0600 Subject: [PATCH] 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. --- src/printer/smt2/smt2_printer.cpp | 6 ++---- src/printer/smt2/smt2_printer.h | 6 ++++++ 2 files changed, 8 insertions(+), 4 deletions(-) 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& 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. -- 2.30.2