diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-26 12:47:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-26 12:47:05 -0600 |
| commit | 3453595e9f5d76a62b113b3a5d13a60dc09ce3ee (patch) | |
| tree | e78403fbf68c4887a95cf66b7edafc84116a31ca /src/printer | |
| parent | cc052e096323a193b52a05c2400c0c4639ada5de (diff) | |
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.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 | ||||
| -rw-r--r-- | 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<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. |