diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-10 21:05:16 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-25 15:02:34 -0500 |
commit | f5f7ecf3ddd9ed23e5e44f2eefd41c1b11f2a70a (patch) | |
tree | ebf5304156cbc6242cf10329e658d95d810d3360 /src/printer | |
parent | 1b916866274cc238c708f25fbb8c17add33d3376 (diff) |
New translation work, support Z3-str-style string constraints.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 3 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 76 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 8 |
3 files changed, 80 insertions, 7 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 39d065065..a68c3ca7f 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -49,6 +49,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_CVC4: return new printer::cvc::CvcPrinter(); + case LANG_Z3STR: + return new printer::smt2::Smt2Printer(printer::smt2::z3str_variant); + case LANG_AST: return new printer::ast::AstPrinter(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fcb352ea7..80dcc8248 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -86,6 +86,21 @@ static std::string maybeQuoteSymbol(const std::string& s) { return s; } +static bool stringifyRegexp(Node n, stringstream& ss) { + if(n.getKind() == kind::STRING_TO_REGEXP) { + ss << n[0].getConst<String>().toString(); + } else if(n.getKind() == kind::REGEXP_CONCAT) { + for(unsigned i = 0; i < n.getNumChildren(); ++i) { + if(!stringifyRegexp(n[i], ss)) { + return false; + } + } + } else { + return false; + } + return true; +} + void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw() { // null @@ -279,9 +294,40 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; // string theory - case kind::STRING_CONCAT: out << "str.++ "; break; - case kind::STRING_IN_REGEXP: out << "str.in.re "; break; - case kind::STRING_LENGTH: out << "str.len "; break; + case kind::STRING_CONCAT: + if(d_variant == z3str_variant) { + out << "Concat "; + for(unsigned i = 0; i < n.getNumChildren(); ++i) { + toStream(out, n[i], -1, types); + if(i + 1 < n.getNumChildren()) { + out << ' '; + } + if(i + 2 < n.getNumChildren()) { + out << "(Concat "; + } + } + for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { + out << ")"; + } + return; + } + out << "str.++ "; + break; + case kind::STRING_IN_REGEXP: { + stringstream ss; + if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) { + out << "= "; + toStream(out, n[0], -1, types); + out << " "; + Node str = NodeManager::currentNM()->mkConst(String(ss.str())); + toStream(out, str, -1, types); + out << ")"; + return; + } + out << "str.in.re "; + break; + } + case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break; case kind::STRING_SUBSTR_TOTAL: case kind::STRING_SUBSTR: out << "str.substr "; break; case kind::STRING_CHARAT: out << "str.at "; break; @@ -597,6 +643,8 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { template <class T> static bool tryToStream(std::ostream& out, const Command* c) throw(); +template <class T> +static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw(); void Smt2Printer::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { @@ -624,7 +672,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetAssertionsCommand>(out, c) || tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || - tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) || tryToStream<SetInfoCommand>(out, c) || tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || @@ -773,7 +821,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() { static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { Expr e = c->getExpr(); - if(!e.isNull()) { + if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) { out << PushCommand() << endl << AssertCommand(e) << endl << CheckSatCommand() << endl @@ -912,8 +960,13 @@ static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) thro out << "(set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { - out << "(set-logic " << c->getLogic() << ")"; +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() { + // Z3-str doesn't have string-specific logic strings(?), so comment it + if(v == z3str_variant) { + out << "; (set-logic " << c->getLogic() << ")"; + } else { + out << "(set-logic " << c->getLogic() << ")"; + } } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { @@ -990,6 +1043,15 @@ static bool tryToStream(std::ostream& out, const Command* c) throw() { return false; } +template <class T> +static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw() { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c), v); + return true; + } + return false; +} + static void toStream(std::ostream& out, const CommandSuccess* s) throw() { if(Command::printsuccess::getPrintSuccess(out)) { out << "success" << endl; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 871b3823a..c70bb78c3 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -27,11 +27,19 @@ namespace CVC4 { namespace printer { namespace smt2 { +enum Variant { + no_variant, + z3str_variant +};/* enum Variant */ + class Smt2Printer : public CVC4::Printer { + Variant d_variant; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); void toStream(std::ostream& out, const Model& m) const throw(); public: + Smt2Printer(Variant variant = no_variant) : d_variant(variant) { } using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); |