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, 38 insertions, 7 deletions

diff --git a/src/smt/command.h b/src/smt/command.h
index 9573e1c22..19bf9fddd 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -2,9 +2,9 @@
 /*! \file command.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Andres Noetzli
+ **   Tim King, Morgan Deters, Andrew Reynolds
  ** 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
@@ -544,13 +544,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
   const std::string d_str_value;
 }; /* class SetUserAttributeCommand */
 
+/**
+ * The command when parsing check-sat.
+ * This command will check satisfiability of the input formula.
+ */
 class CVC4_PUBLIC CheckSatCommand : public Command
 {
- protected:
-  Expr d_expr;
-  Result d_result;
-  bool d_inUnsatCore;
-
  public:
   CheckSatCommand();
   CheckSatCommand(const Expr& expr, bool inUnsatCore = true);
@@ -563,8 +562,40 @@ class CVC4_PUBLIC CheckSatCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+
+ private:
+  Expr d_expr;
+  Result d_result;
+  bool d_inUnsatCore;
 }; /* class CheckSatCommand */
 
+/**
+ * The command when parsing check-sat-assuming.
+ * This command will assume a set of formulas and check satisfiability of the
+ * input formula under these assumptions.
+ */
+class CVC4_PUBLIC CheckSatAssumingCommand : public Command
+{
+ public:
+  CheckSatAssumingCommand(Expr term);
+  CheckSatAssumingCommand(const std::vector<Expr>& terms,
+                          bool inUnsatCore = true);
+
+  const std::vector<Expr>& getTerms() const;
+  Result getResult() const;
+  void invoke(SmtEngine* smtEngine) override;
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ private:
+  std::vector<Expr> d_terms;
+  Result d_result;
+  bool d_inUnsatCore;
+}; /* class CheckSatAssumingCommand */
+
 class CVC4_PUBLIC QueryCommand : public Command
 {
  protected: