diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 |
1 files changed, 28 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 27105c3b4..d778ccc2b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -2,9 +2,9 @@ /*! \file cvc_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -955,6 +955,7 @@ void CvcPrinter::toStream(std::ostream& out, tryToStream<PushCommand>(out, c, d_cvc3Mode) || tryToStream<PopCommand>(out, c, d_cvc3Mode) || tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) || + tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) || tryToStream<QueryCommand>(out, c, d_cvc3Mode) || tryToStream<ResetCommand>(out, c, d_cvc3Mode) || tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) || @@ -1159,6 +1160,31 @@ static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) } } +static void toStream(std::ostream& out, + const CheckSatAssumingCommand* c, + bool cvc3Mode) +{ + const vector<Expr>& exprs = c->getTerms(); + if (cvc3Mode) + { + out << "PUSH; "; + } + out << "CHECKSAT"; + if (exprs.size() > 0) + { + out << " " << exprs[0]; + for (size_t i = 1, n = exprs.size(); i < n; ++i) + { + out << " AND " << exprs[i]; + } + } + out << ";"; + if (cvc3Mode) + { + out << " POP;"; + } +} + static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) { Expr e = c->getExpr(); |