Add support for check-sat-assuming. (#1637)

This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).

1 files changed, 10 insertions, 1 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index be95c947d..31f9b9c41 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -147,6 +147,7 @@ void AstPrinter::toStream(std::ostream& out,
      tryToStream<PushCommand>(out, c) ||
      tryToStream<PopCommand>(out, c) ||
      tryToStream<CheckSatCommand>(out, c) ||
+     tryToStream<CheckSatAssumingCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<ResetCommand>(out, c) ||
      tryToStream<ResetAssertionsCommand>(out, c) ||
@@ -237,6 +238,14 @@ static void toStream(std::ostream& out, const CheckSatCommand* c)
   }
 }
 
+static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+{
+  const vector<Expr>& terms = c->getTerms();
+  out << "CheckSatAssuming( << ";
+  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  out << ">> )";
+}
+
 static void toStream(std::ostream& out, const QueryCommand* c)
 {
   out << "Query(" << c->getExpr() << ')';
@@ -333,7 +342,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c)
   out << "GetValue( << ";
   const vector<Expr>& terms = c->getTerms();
   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
-  out << " >> )";
+  out << ">> )";
 }
 
 static void toStream(std::ostream& out, const GetModelCommand* c)