Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)

1 files changed, 33 insertions, 6 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index bba6b1cef..377888a5a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -159,6 +159,14 @@ class CVC4_PUBLIC SmtEngine {
   AssertionList* d_assertionList;
 
   /**
+   * The list of assumptions from the previous call to checkSatisfiability.
+   * Note that if the last call to checkSatisfiability was a validity check,
+   * i.e., a call to query(a1, ..., an), then d_assumptions contains one single
+   * assumption ~(a1 AND ... AND an).
+   */
+  std::vector<Expr> d_assumptions;
+
+  /**
    * List of items for which to retrieve values using getAssignment().
    */
   AssignmentSet* d_assignments;
@@ -318,6 +326,13 @@ class CVC4_PUBLIC SmtEngine {
   void setDefaults();
 
   /**
+   * Sets d_problemExtended to the given value.
+   * If d_problemExtended is set to true, the list of assumptions from the
+   * previous call to checkSatisfiability is cleared.
+   */
+  void setProblemExtended(bool value);
+
+  /**
    * Create theory engine, prop engine, decision engine. Called by
    * finalOptionsAreSet()
    */
@@ -400,10 +415,10 @@ class CVC4_PUBLIC SmtEngine {
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
 
   //check satisfiability (for query and check-sat)
-  Result checkSatisfiability(const Expr& expr,
+  Result checkSatisfiability(const Expr& assumption,
                              bool inUnsatCore,
                              bool isQuery);
-  Result checkSatisfiability(const std::vector<Expr>& exprs,
+  Result checkSatisfiability(const std::vector<Expr>& assumptions,
                              bool inUnsatCore,
                              bool isQuery);
 
@@ -540,21 +555,33 @@ 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 = Expr(),
+  Result query(const Expr& assumption = Expr(),
                bool inUnsatCore = true) /* throw(Exception) */;
-  Result query(const std::vector<Expr>& exprs,
+  Result query(const std::vector<Expr>& assumptions,
                bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const Expr& e = Expr(),
+  Result checkSat(const Expr& assumption = Expr(),
                   bool inUnsatCore = true) /* throw(Exception) */;
-  Result checkSat(const std::vector<Expr>& exprs,
+  Result checkSat(const std::vector<Expr>& assumptions,
                   bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
+   * Returns a set of so-called "failed" assumptions.
+   *
+   * The returned set is a subset of the set of assumptions of a previous
+   * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability
+   * with this set of failed assumptions still produces an unsat answer.
+   *
+   * Note that the returned set of failed assumptions is not necessarily
+   * minimal.
+   */
+  std::vector<Expr> getUnsatAssumptions(void);
+
+  /**
    * Assert a synthesis conjecture to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */