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, 12 insertions, 2 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 16cf90de1..bba6b1cef 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -400,7 +400,12 @@ class CVC4_PUBLIC SmtEngine {
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
 
   //check satisfiability (for query and check-sat)
-  Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
+  Result checkSatisfiability(const Expr& expr,
+                             bool inUnsatCore,
+                             bool isQuery);
+  Result checkSatisfiability(const std::vector<Expr>& exprs,
+                             bool inUnsatCore,
+                             bool isQuery);
 
   /**
    * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
@@ -535,7 +540,10 @@ class CVC4_PUBLIC SmtEngine {
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const Expr& e, bool inUnsatCore = true) /* throw(Exception) */;
+  Result query(const Expr& e = Expr(),
+               bool inUnsatCore = true) /* throw(Exception) */;
+  Result query(const std::vector<Expr>& exprs,
+               bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
    * Assert a formula (if provided) to the current context and call
@@ -543,6 +551,8 @@ class CVC4_PUBLIC SmtEngine {
    */
   Result checkSat(const Expr& e = Expr(),
                   bool inUnsatCore = true) /* throw(Exception) */;
+  Result checkSat(const std::vector<Expr>& exprs,
+                  bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
    * Assert a synthesis conjecture to the current context and call