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)).

3 files changed, 62 insertions, 11 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)
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();
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e06f8c062..e025c64f1 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2_printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Martin Brain
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** 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
@@ -1191,7 +1191,8 @@ void Smt2Printer::toStream(std::ostream& out,
   if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
       || tryToStream<PopCommand>(out, c)
       || tryToStream<CheckSatCommand>(out, c)
-      || tryToStream<QueryCommand>(out, c)
+      || tryToStream<CheckSatAssumingCommand>(out, c)
+      || tryToStream<QueryCommand>(out, c, d_variant)
       || tryToStream<ResetCommand>(out, c)
       || tryToStream<ResetAssertionsCommand>(out, c)
       || tryToStream<QuitCommand>(out, c)
@@ -1511,14 +1512,29 @@ static void toStream(std::ostream& out, const CheckSatCommand* c)
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c)
+static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+{
+  out << "(check-sat-assuming ( ";
+  const vector<Expr>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  out << "))";
+}
+
+static void toStream(std::ostream& out, const QueryCommand* c, Variant v)
 {
   Expr e = c->getExpr();
   if(!e.isNull()) {
-    out << PushCommand() << endl
-        << AssertCommand(BooleanSimplification::negate(e)) << endl
-        << CheckSatCommand() << endl
-        << PopCommand();
+    if (v == smt2_0_variant)
+    {
+      out << PushCommand() << endl
+          << AssertCommand(BooleanSimplification::negate(e)) << endl
+          << CheckSatCommand() << endl
+          << PopCommand();
+    }
+    else
+    {
+      out << CheckSatAssumingCommand(e.notExpr()) << endl;
+    }
   } else {
     out << "(check-sat)";
   }