Split Assertions from SmtEngine (#4788)

This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.

1 files changed, 6 insertions, 44 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5a8c41652..5dc0d74fa 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,7 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class Assertions;
 class ExprNames;
 class DumpManager;
 class ResourceOutListener;
@@ -409,7 +410,7 @@ class CVC4_PUBLIC SmtEngine
    * Note that the returned set of failed assumptions is not necessarily
    * minimal.
    */
-  std::vector<Expr> getUnsatAssumptions(void);
+  std::vector<Node> getUnsatAssumptions(void);
 
   /*---------------------------- sygus commands  ---------------------------*/
 
@@ -1001,13 +1002,6 @@ class CVC4_PUBLIC SmtEngine
   void finalOptionsAreSet();
 
   /**
-   * Sets that the problem has been extended. This sets the smt mode of the
-   * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the
-   * previous call to checkSatisfiability.
-   */
-  void setProblemExtended();
-
-  /**
    * Create theory engine, prop engine, decision engine. Called by
    * finalOptionsAreSet()
    */
@@ -1046,14 +1040,6 @@ class CVC4_PUBLIC SmtEngine
    */
   theory::TheoryModel* getAvailableModel(const char* c) const;
 
-  /**
-   * Fully type-check the argument, and also type-check that it's
-   * actually Boolean.
-   *
-   * throw@ TypeCheckingException
-   */
-  void ensureBoolean(const Node& n);
-
   void internalPush();
 
   void internalPop(bool immediate = false);
@@ -1076,10 +1062,10 @@ class CVC4_PUBLIC SmtEngine
                                 const char* dumpTag = "declarations");
 
   /* Check satisfiability (used to check satisfiability and entailment). */
-  Result checkSatisfiability(const Expr& assumption,
+  Result checkSatisfiability(const Node& assumption,
                              bool inUnsatCore,
                              bool isEntailmentCheck);
-  Result checkSatisfiability(const std::vector<Expr>& assumptions,
+  Result checkSatisfiability(const std::vector<Node>& assumptions,
                              bool inUnsatCore,
                              bool isEntailmentCheck);
 
@@ -1124,6 +1110,8 @@ class CVC4_PUBLIC SmtEngine
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
+  /** Assertions manager */
+  std::unique_ptr<smt::Assertions> d_asserts;
   /** Expression names */
   std::unique_ptr<smt::ExprNames> d_exprNames;
   /** The dump manager */
@@ -1154,27 +1142,6 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
-
-  /**
-   * The assertion list (before any conversion) for supporting
-   * getAssertions().  Only maintained if in incremental mode.
-   */
-  AssertionList* d_assertionList;
-
-  /**
-   * List of lemmas generated for global recursive function definitions. We
-   * assert this list of definitions in each check-sat call.
-   */
-  std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas;
-
-  /**
-   * The list of assumptions from the previous call to checkSatisfiability.
-   * Note that if the last call to checkSatisfiability was an entailment check,
-   * i.e., a call to checkEntailed(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().
    */
@@ -1236,11 +1203,6 @@ class CVC4_PUBLIC SmtEngine
    */
   bool d_earlyTheoryPP;
 
-  /*
-   * Whether we did a global negation of the formula.
-   */
-  bool d_globalNegation;
-
   /**
    * Most recent result of last checkSatisfiability/checkEntailed or
    * (set-info :status).