diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-26 14:08:33 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-26 14:08:33 +0100 |
| commit | 365d6022b5742fc6910363e04e873b26e221bb05 (patch) | |
| tree | 0c4111ffbaa325646610bb598886216938ff10e4 /src/printer | |
| parent | 7f43bd304b3d6bede36a777ee85ab68fab35d742 (diff) | |
Front-end support for get-value of sort cardinality, minor fixes for sygus solution reconstruction.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b9b309d4a..56ad9c35a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -446,6 +446,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::REGEXP_EMPTY: out << "re.nostr "; break; case kind::REGEXP_SIGMA: out << "re.allchar "; break; + case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; + case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; + // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break; case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break; |