diff options
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 9 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 | ||||
| -rw-r--r-- | test/unit/parser/parser_builder_black.h | 12 |
3 files changed, 12 insertions, 14 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b7e1520b7..4f0d4b664 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -398,8 +398,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } } break; - case kind::APPLY_TESTER: - toStream(op, n.getOperator(), depth, types, false); + case kind::APPLY_TESTER: { + Assert( !n.getType().isTuple() && !n.getType().isRecord() ); + op << "is_"; + unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false); + } break; case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index be550474c..aa5849960 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -668,6 +668,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, tmp.replace(pos, 8, "::"); } out << tmp; + }else if( n.getKind()==kind::APPLY_TESTER ){ + unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + out << "is-"; + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); }else{ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); } diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index f65dadf1b..c2f8317b1 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -16,7 +16,6 @@ #include <cxxtest/TestSuite.h> -#include <ext/stdio_filebuf.h> #include <stdio.h> #include <string.h> #include <sys/stat.h> @@ -30,9 +29,6 @@ #include "parser/parser_builder.h" #include "smt/command.h" - -typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu; - using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::language::input; @@ -85,20 +81,12 @@ public: void testEmptyFileInput() { char *filename = mkTemp(); - /* FILE *fp = tmpfile(); */ - /* filebuf_gnu fs( fd, ios_base::out ); */ - - /* ptr = tmpnam(filename); */ - /* std::fstream fs( ptr, fstream::out ); */ - /* fs.close(); */ - checkEmptyInput( ParserBuilder(d_exprManager,filename) .withInputLanguage(LANG_CVC4) ); remove(filename); - // mkfifo(ptr, S_IWUSR | s_IRUSR); free(filename); } |