diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-27 21:01:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-27 21:01:54 -0500 |
commit | e25f99329c9905c67a565481dcb0d6a4499a7557 (patch) | |
tree | a85e7f998c4d4e722c80c8bcdedbc6292432bdb2 /src/printer | |
parent | b2447df23d473184a7881ead02aa0b1e8f547d53 (diff) |
Support smt2 language "match" term (#3258)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index df9bee981..013288880 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -540,7 +540,31 @@ void Smt2Printer::toStream(std::ostream& out, } return; - case kind::LAMBDA: + case kind::LAMBDA: out << smtKindString(k, d_variant) << " "; break; + case kind::MATCH: + out << smtKindString(k, d_variant) << " "; + toStream(out, n[0], toDepth, types, TypeNode::null()); + out << " ("; + for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++) + { + if (i > 1) + { + out << " "; + } + toStream(out, n[i], toDepth, types, TypeNode::null()); + } + out << "))"; + return; + case kind::MATCH_BIND_CASE: + // ignore the binder + toStream(out, n[1], toDepth, types, TypeNode::null()); + out << " "; + toStream(out, n[2], toDepth, types, TypeNode::null()); + out << ")"; + return; + case kind::MATCH_CASE: + // do nothing + break; case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break; // arith theory @@ -1030,6 +1054,7 @@ static string smtKindString(Kind k, Variant v) case kind::LAMBDA: return "lambda"; + case kind::MATCH: return "match"; case kind::CHOICE: return "choice"; // arith theory |