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.

9 files changed, 513 insertions, 296 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cd6f48178..92f197252 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -223,6 +223,8 @@ libcvc4_add_sources(
   smt/abduction_solver.h
   smt/abstract_values.cpp
   smt/abstract_values.h
+  smt/assertions.cpp
+  smt/assertions.h
   smt/command.cpp
   smt/command.h
   smt/defined_function.h
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index eef2b7052..0963c704b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4906,14 +4906,14 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
                  == SmtEngine::SmtMode::SMT_MODE_UNSAT)
       << "Cannot get unsat assumptions unless in unsat mode.";
 
-  std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions();
+  std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions();
   /* Can not use
    *   return std::vector<Term>(uassumptions.begin(), uassumptions.end());
    * here since constructor is private */
   std::vector<Term> res;
-  for (const Expr& e : uassumptions)
+  for (const Node& e : uassumptions)
   {
-    res.push_back(Term(this, e));
+    res.push_back(Term(this, e.toExpr()));
   }
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
new file mode 100644
index 000000000..ea3acf2d1
--- /dev/null
+++ b/src/smt/assertions.cpp
@@ -0,0 +1,234 @@
+/*********************                                                        */
+/*! \file assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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
+ **
+ ** \brief The module for storing assertions for an SMT engine.
+ **/
+
+#include "smt/assertions.h"
+
+#include "expr/node_algorithm.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/proof_options.h"
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
+    : d_userContext(u),
+      d_absValues(absv),
+      d_assertionList(nullptr),
+      d_globalNegation(false),
+      d_assertions()
+{
+}
+
+Assertions::~Assertions()
+{
+  if (d_assertionList != nullptr)
+  {
+    d_assertionList->deleteSelf();
+  }
+}
+
+void Assertions::finishInit()
+{
+  // [MGD 10/20/2011] keep around in incremental mode, due to a
+  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
+  // first, some user-context-dependent TNodes might still exist
+  // with rc == 0.
+  if (options::produceAssertions() || options::incrementalSolving())
+  {
+    // In the case of incremental solving, we appear to need these to
+    // ensure the relevant Nodes remain live.
+    d_assertionList = new (true) AssertionList(d_userContext);
+    d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
+  }
+}
+
+void Assertions::clearCurrent()
+{
+  d_assertions.clear();
+  d_assertions.getIteSkolemMap().clear();
+}
+
+void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
+                                    bool inUnsatCore,
+                                    bool isEntailmentCheck)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  // reset global negation
+  d_globalNegation = false;
+  // clear the assumptions
+  d_assumptions.clear();
+  if (isEntailmentCheck)
+  {
+    size_t size = assumptions.size();
+    if (size > 1)
+    {
+      /* Assume: not (BIGAND assumptions)  */
+      d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
+    }
+    else if (size == 1)
+    {
+      /* Assume: not expr  */
+      d_assumptions.push_back(assumptions[0].notNode());
+    }
+  }
+  else
+  {
+    /* Assume: BIGAND assumptions  */
+    d_assumptions = assumptions;
+  }
+
+  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+  for (const Node& e : d_assumptions)
+  {
+    // Substitute out any abstract values in ex.
+    Node n = d_absValues.substituteAbstractValues(e);
+    // Ensure expr is type-checked at this point.
+    ensureBoolean(n);
+
+    /* Add assumption  */
+    if (d_assertionList != nullptr)
+    {
+      d_assertionList->push_back(n);
+    }
+    addFormula(n, inUnsatCore, true, true, false);
+  }
+  if (d_globalDefineFunRecLemmas != nullptr)
+  {
+    // Global definitions are asserted at check-sat-time because we have to
+    // make sure that they are always present (they are essentially level
+    // zero assertions)
+    for (const Node& lemma : *d_globalDefineFunRecLemmas)
+    {
+      addFormula(lemma, false, true, false, false);
+    }
+  }
+}
+
+void Assertions::assertFormula(const Node& n, bool inUnsatCore)
+{
+  ensureBoolean(n);
+  if (d_assertionList != nullptr)
+  {
+    d_assertionList->push_back(n);
+  }
+  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+  addFormula(n, inUnsatCore, true, false, maybeHasFv);
+}
+
+std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
+bool Assertions::isGlobalNegated() const { return d_globalNegation; }
+void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
+
+preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
+{
+  return d_assertions;
+}
+
+context::CDList<Node>* Assertions::getAssertionList()
+{
+  return d_assertionList;
+}
+
+void Assertions::addFormula(
+    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
+{
+  if (n.isConst() && n.getConst<bool>())
+  {
+    // true, nothing to do
+    return;
+  }
+
+  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
+               << "), inUnsatCore = " << inUnsatCore
+               << ", inInput = " << inInput
+               << ", isAssumption = " << isAssumption << std::endl;
+
+  // Ensure that it does not contain free variables
+  if (maybeHasFv)
+  {
+    if (expr::hasFreeVar(n))
+    {
+      std::stringstream se;
+      se << "Cannot process assertion with free variable.";
+      if (language::isInputLangSygus(options::inputLanguage()))
+      {
+        // Common misuse of SyGuS is to use top-level assert instead of
+        // constraint when defining the synthesis conjecture.
+        se << " Perhaps you meant `constraint` instead of `assert`?";
+      }
+      throw ModalException(se.str().c_str());
+    }
+  }
+
+  // Give it to proof manager
+  PROOF(if (inInput) {
+    // n is an input assertion
+    if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
+        || options::checkUnsatCores() || options::fewerPreprocessingHoles())
+    {
+      ProofManager::currentPM()->addCoreAssertion(n.toExpr());
+    }
+  } else {
+    // n is the result of an unknown preprocessing step, add it to dependency
+    // map to null
+    ProofManager::currentPM()->addDependence(n, Node::null());
+  });
+
+  // Add the normalized formula to the queue
+  d_assertions.push_back(n, isAssumption);
+}
+
+void Assertions::addDefineFunRecDefinition(Node n, bool global)
+{
+  n = d_absValues.substituteAbstractValues(n);
+  if (d_assertionList != nullptr)
+  {
+    d_assertionList->push_back(n);
+  }
+  if (global && d_globalDefineFunRecLemmas != nullptr)
+  {
+    // Global definitions are asserted at check-sat-time because we have to
+    // make sure that they are always present
+    Assert(!language::isInputLangSygus(options::inputLanguage()));
+    d_globalDefineFunRecLemmas->emplace_back(n);
+  }
+  else
+  {
+    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+    addFormula(n, false, true, false, maybeHasFv);
+  }
+}
+
+void Assertions::ensureBoolean(const Node& n)
+{
+  TypeNode type = n.getType(options::typeChecking());
+  if (!type.isBoolean())
+  {
+    std::stringstream ss;
+    ss << "Expected Boolean type\n"
+       << "The assertion : " << n << "\n"
+       << "Its type      : " << type;
+    throw TypeCheckingException(n.toExpr(), ss.str());
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
new file mode 100644
index 000000000..c2a16db71
--- /dev/null
+++ b/src/smt/assertions.h
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/*! \file assertions.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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
+ **
+ ** \brief The module for storing assertions for an SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__ASSERTIONS_H
+#define CVC4__SMT__ASSERTIONS_H
+
+#include <vector>
+
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "smt/abstract_values.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * Contains all information pertaining to the assertions of an SMT engine.
+ *
+ * This class is responsible for setting up the assertions pipeline for
+ * check-sat calls. It is *not* responsible for the preprocessing itself, and
+ * instead is intended to be the input to a preprocessor utility.
+ */
+class Assertions
+{
+  /** The type of our internal assertion list */
+  typedef context::CDList<Node> AssertionList;
+
+ public:
+  Assertions(context::UserContext* u, AbstractValues& absv);
+  ~Assertions();
+  /**
+   * Finish initialization, called once after options are finalized. Sets up
+   * the required bookkeeping based on the options.
+   */
+  void finishInit();
+  /**
+   * Clears out the non-context-dependent data in this class.  Necessary to
+   * clear out our assertion vectors in case someone does a push-assert-pop
+   * without a check-sat.
+   */
+  void clearCurrent();
+  /*
+   * Initialize a call to check satisfiability. This adds assumptions to
+   * the list of assumptions maintained by this class, and finalizes the
+   * set of formulas (in the assertions pipeline) that will be used for the
+   * upcoming check-sat call.
+   *
+   * @param assumptions The assumptions of the upcoming check-sat call.
+   * @param inUnsatCore Whether assumptions are in the unsat core.
+   * @param isEntailmentCheck Whether we are checking entailment of assumptions
+   * in the upcoming check-sat call.
+   */
+  void initializeCheckSat(const std::vector<Node>& assumptions,
+                          bool inUnsatCore,
+                          bool isEntailmentCheck);
+  /**
+   * Add a formula to the current context: preprocess, do per-theory
+   * setup, use processAssertionList(), asserting to T-solver for
+   * literals and conjunction of literals.  Returns false if
+   * immediately determined to be inconsistent.  This version
+   * takes a Boolean flag to determine whether to include this asserted
+   * formula in an unsat core (if one is later requested).
+   *
+   * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+   */
+  void assertFormula(const Node& n, bool inUnsatCore = true);
+  /**
+   * Assert that n corresponds to an assertion from a define-fun-rec command.
+   * This assertion is added to the set of assertions maintained by this class.
+   * If this has a global definition, this assertion is persistent for any
+   * subsequent check-sat calls.
+   */
+  void addDefineFunRecDefinition(Node n, bool global);
+  /**
+   * Get the assertions pipeline, which contains the set of assertions we are
+   * currently processing.
+   */
+  preprocessing::AssertionPipeline& getAssertionPipeline();
+  /**
+   * Get assertions list corresponding to the original list of assertions,
+   * before preprocessing.
+   */
+  context::CDList<Node>* getAssertionList();
+  /**
+   * Get the list of assumptions, which are those registered to this class
+   * on initializeCheckSat.
+   */
+  std::vector<Node>& getAssumptions();
+  /**
+   * Is the set of assertions globally negated? When this flag is true, the
+   * overall result of check-sat should be inverted.
+   */
+  bool isGlobalNegated() const;
+  /** Flip the global negation flag. */
+  void flipGlobalNegated();
+
+ private:
+  /**
+   * Fully type-check the argument, and also type-check that it's
+   * actually Boolean.
+   * throw@ TypeCheckingException
+   */
+  void ensureBoolean(const Node& n);
+  /**
+   * Adds a formula to the current context.  Action here depends on
+   * the SimplificationMode (in the current Options scope); the
+   * formula might be pushed out to the propositional layer
+   * immediately, or it might be simplified and kept, or it might not
+   * even be simplified.
+   * The arguments isInput and isAssumption are used for bookkeeping for proofs.
+   * The argument maybeHasFv should be set to true if the assertion may have
+   * free variables. By construction, assertions from the smt2 parser are
+   * guaranteed not to have free variables. However, other cases such as
+   * assertions from the SyGuS parser may have free variables (say if the
+   * input contains an assert or define-fun-rec command).
+   *
+   * @param isAssumption If true, the formula is considered to be an assumption
+   * (this is used to distinguish assertions and assumptions)
+   */
+  void addFormula(TNode n,
+                  bool inUnsatCore,
+                  bool inInput,
+                  bool isAssumption,
+                  bool maybeHasFv);
+  /** pointer to the user context */
+  context::UserContext* d_userContext;
+  /** Reference to the abstract values utility */
+  AbstractValues& d_absValues;
+  /**
+   * 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<Node> d_assumptions;
+  /** Whether we did a global negation of the formula. */
+  bool d_globalNegation;
+  /** Assertions in the preprocessing pipeline */
+  preprocessing::AssertionPipeline d_assertions;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 97a51277b..52a9578dd 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2359,7 +2359,12 @@ void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    d_result = smtEngine->getUnsatAssumptions();
+    std::vector<Node> uassumps = smtEngine->getUnsatAssumptions();
+    d_result.clear();
+    for (const Node& n : uassumps)
+    {
+      d_result.push_back(n.toExpr());
+    }
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 4fed33f3c..d2bf3ba46 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -91,8 +91,9 @@ void ProcessAssertions::spendResource(ResourceManager::Resource r)
   d_resourceManager.spendResource(r);
 }
 
-bool ProcessAssertions::apply(AssertionPipeline& assertions)
+bool ProcessAssertions::apply(Assertions& as)
 {
+  AssertionPipeline& assertions = as.getAssertionPipeline();
   Assert(d_preprocessingPassContext != nullptr);
   // Dump the assertions
   dumpAssertions("pre-everything", assertions);
@@ -158,7 +159,7 @@ bool ProcessAssertions::apply(AssertionPipeline& assertions)
   {
     // global negation of the formula
     d_passes["global-negate"]->apply(&assertions);
-    d_smt.d_globalNegation = !d_smt.d_globalNegation;
+    as.flipGlobalNegated();
   }
 
   if (options::nlExtPurify())
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 4850d5589..2a7efe1c0 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -25,6 +25,7 @@
 #include "expr/type_node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "smt/assertions.h"
 #include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
 
@@ -69,10 +70,10 @@ class ProcessAssertions
    */
   void cleanup();
   /**
-   * Process the formulas in assertions. Returns true if there
-   * was no conflict when processing the assertions.
+   * Process the formulas in as. Returns true if there was no conflict when
+   * processing the assertions.
    */
-  bool apply(preprocessing::AssertionPipeline& assertions);
+  bool apply(Assertions& as);
   /**
    * Expand definitions in term n. Return the expanded form of n.
    *
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e5b95d656..43aa3b0c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -82,6 +82,7 @@
 #include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
+#include "smt/assertions.h"
 #include "smt/expr_names.h"
 #include "smt/command.h"
 #include "smt/defined_function.h"
@@ -162,9 +163,6 @@ class SmtEnginePrivate
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
 
-  /** Assertions in the preprocessing pipeline */
-  AssertionPipeline d_assertions;
-
   /** Whether any assertions have been processed */
   CDO<bool> d_assertionsProcessed;
 
@@ -178,7 +176,6 @@ class SmtEnginePrivate
   ProcessAssertions d_processor;
 
  public:
-  IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
 
   /** Instance of the ITE remover */
   RemoveTermFormulas d_iteRemover;
@@ -208,7 +205,6 @@ class SmtEnginePrivate
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
         d_propagator(true, true),
-        d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
         d_processor(smt, *smt.getResourceManager()),
         d_iteRemover(smt.getUserContext()),
@@ -241,12 +237,11 @@ class SmtEnginePrivate
   /**
    * Process the assertions that have been asserted.
    */
-  void processAssertions();
+  void processAssertions(Assertions& as);
 
   /** Process a user push.
   */
   void notifyPush() {
-
   }
 
   /**
@@ -256,32 +251,8 @@ class SmtEnginePrivate
    * last map of expression names from notifyPush.
    */
   void notifyPop() {
-    d_assertions.clear();
     d_propagator.getLearnedLiterals().clear();
-    getIteSkolemMap().clear();
   }
-
-  /**
-   * Adds a formula to the current context.  Action here depends on
-   * the SimplificationMode (in the current Options scope); the
-   * formula might be pushed out to the propositional layer
-   * immediately, or it might be simplified and kept, or it might not
-   * even be simplified.
-   * The arguments isInput and isAssumption are used for bookkeeping for proofs.
-   * The argument maybeHasFv should be set to true if the assertion may have
-   * free variables. By construction, assertions from the smt2 parser are
-   * guaranteed not to have free variables. However, other cases such as
-   * assertions from the SyGuS parser may have free variables (say if the
-   * input contains an assert or define-fun-rec command).
-   *
-   * @param isAssumption If true, the formula is considered to be an assumption
-   * (this is used to distinguish assertions and assumptions)
-   */
-  void addFormula(TNode n,
-                  bool inUnsatCore,
-                  bool inInput = true,
-                  bool isAssumption = false,
-                  bool maybeHasFv = false);
   /**
    * Simplify node "in" by expanding definitions and applying any
    * substitutions learned from preprocessing.
@@ -291,8 +262,6 @@ class SmtEnginePrivate
     // Expand definitions.
     NodeToNodeHashMap cache;
     Node n = d_processor.expandDefinitions(in, cache).toExpr();
-    // Make sure we've done all preprocessing, etc.
-    Assert(d_assertions.size() == 0);
     return applySubstitutions(n).toExpr();
   }
 };/* class SmtEnginePrivate */
@@ -306,6 +275,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
+      d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())),
       d_exprNames(new ExprNames(d_userContext.get())),
       d_dumpm(new DumpManager(d_userContext.get())),
       d_routListener(new ResourceOutListener(*this)),
@@ -316,7 +286,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_abductSolver(nullptr),
-      d_assertionList(nullptr),
       d_assignments(nullptr),
       d_defineCommands(),
       d_logic(),
@@ -326,7 +295,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_fullyInited(false),
       d_queryMade(false),
       d_needPostsolve(false),
-      d_globalNegation(false),
       d_status(),
       d_expectedStatus(),
       d_smtMode(SMT_MODE_START),
@@ -434,18 +402,8 @@ void SmtEngine::finishInit()
   d_userContext->push();
   d_context->push();
 
-  Trace("smt-debug") << "Set up assertion list..." << std::endl;
-  // [MGD 10/20/2011] keep around in incremental mode, due to a
-  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
-  // first, some user-context-dependent TNodes might still exist
-  // with rc == 0.
-  if(options::produceAssertions() ||
-     options::incrementalSolving()) {
-    // In the case of incremental solving, we appear to need these to
-    // ensure the relevant Nodes remain live.
-    d_assertionList = new (true) AssertionList(getUserContext());
-    d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
-  }
+  Trace("smt-debug") << "Set up assertions..." << std::endl;
+  d_asserts->finishInit();
 
   // dump out a set-logic command only when raw-benchmark is disabled to avoid
   // dumping the command twice.
@@ -534,12 +492,6 @@ SmtEngine::~SmtEngine()
       d_assignments->deleteSelf();
     }
 
-    d_globalDefineFunRecLemmas.reset();
-
-    if(d_assertionList != NULL) {
-      d_assertionList->deleteSelf();
-    }
-
     d_definedFunctions->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
@@ -557,6 +509,7 @@ SmtEngine::~SmtEngine()
 #endif
 
     d_absValues.reset(nullptr);
+    d_asserts.reset(nullptr);
     d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
@@ -647,12 +600,6 @@ void SmtEngine::setLogicInternal()
   d_userLogic.lock();
 }
 
-void SmtEngine::setProblemExtended()
-{
-  d_smtMode = SMT_MODE_ASSERT;
-  d_assumptions.clear();
-}
-
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
 {
   SmtScope smts(this);
@@ -983,7 +930,6 @@ void SmtEngine::defineFunctionsRec(
   }
 
   ExprManager* em = getExprManager();
-  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
   for (unsigned i = 0, size = funcs.size(); i < size; i++)
   {
     // we assert a quantified formula
@@ -1018,22 +964,9 @@ void SmtEngine::defineFunctionsRec(
     // assert the quantified formula
     //   notice we don't call assertFormula directly, since this would
     //   duplicate the output on raw-benchmark.
-    Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem));
-    if (d_assertionList != nullptr)
-    {
-      d_assertionList->push_back(n);
-    }
-    if (global && d_globalDefineFunRecLemmas != nullptr)
-    {
-      // Global definitions are asserted at check-sat-time because we have to
-      // make sure that they are always present
-      Assert(!language::isInputLangSygus(options::inputLanguage()));
-      d_globalDefineFunRecLemmas->emplace_back(n);
-    }
-    else
-    {
-      d_private->addFormula(n, false, true, false, maybeHasFv);
-    }
+    Node lemn = Node::fromExpr(lem);
+    // add define recursive definition to the assertions
+    d_asserts->addDefineFunRecDefinition(lemn, global);
   }
 }
 
@@ -1084,7 +1017,7 @@ Result SmtEngine::check() {
 
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
 
   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
@@ -1147,13 +1080,17 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   return m;
 }
 
-void SmtEnginePrivate::processAssertions() {
+void SmtEnginePrivate::processAssertions(Assertions& as)
+{
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
   spendResource(ResourceManager::Resource::PreprocessStep);
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
-  if (d_assertions.size() == 0) {
+  AssertionPipeline& ap = as.getAssertionPipeline();
+
+  if (ap.size() == 0)
+  {
     // nothing to do
     return;
   }
@@ -1161,24 +1098,24 @@ void SmtEnginePrivate::processAssertions() {
     // TODO(b/1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
 
-    d_assertions.enableStoreSubstsInAsserts();
+    ap.enableStoreSubstsInAsserts();
   }
   else
   {
-    d_assertions.disableStoreSubstsInAsserts();
+    ap.disableStoreSubstsInAsserts();
   }
 
   // process the assertions
-  bool noConflict = d_processor.apply(d_assertions);
+  bool noConflict = d_processor.apply(as);
 
   //notify theory engine new preprocessed assertions
-  d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
+  d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
 
   // Push the formula to decision engine
   if (noConflict)
   {
     Chat() << "pushing to decision engine..." << endl;
-    d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
+    d_smt.d_propEngine->addAssertionsToDecisionEngine(ap);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
@@ -1187,91 +1124,30 @@ void SmtEnginePrivate::processAssertions() {
   // if incremental, compute which variables are assigned
   if (options::incrementalSolving())
   {
-    d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref());
+    d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref());
   }
 
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Chat() << "+ " << d_assertions[i] << std::endl;
-      d_smt.d_propEngine->assertFormula(d_assertions[i]);
-    }
-  }
-
-  d_assertionsProcessed = true;
-
-  d_assertions.clear();
-  getIteSkolemMap().clear();
-}
-
-void SmtEnginePrivate::addFormula(
-    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
-{
-  if (n == d_true) {
-    // nothing to do
-    return;
-  }
-
-  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
-               << "), inUnsatCore = " << inUnsatCore
-               << ", inInput = " << inInput
-               << ", isAssumption = " << isAssumption << endl;
-
-  // Ensure that it does not contain free variables
-  if (maybeHasFv)
-  {
-    if (expr::hasFreeVar(n))
+    for (const Node& assertion : ap.ref())
     {
-      std::stringstream se;
-      se << "Cannot process assertion with free variable.";
-      if (language::isInputLangSygus(options::inputLanguage()))
-      {
-        // Common misuse of SyGuS is to use top-level assert instead of
-        // constraint when defining the synthesis conjecture.
-        se << " Perhaps you meant `constraint` instead of `assert`?";
-      }
-      throw ModalException(se.str().c_str());
+      Chat() << "+ " << assertion << std::endl;
+      d_smt.d_propEngine->assertFormula(assertion);
     }
   }
 
-  // Give it to proof manager
-  PROOF(
-    if( inInput ){
-      // n is an input assertion
-      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
-
-        ProofManager::currentPM()->addCoreAssertion(n.toExpr());
-      }
-    }else{
-      // n is the result of an unknown preprocessing step, add it to dependency map to null
-      ProofManager::currentPM()->addDependence(n, Node::null());
-    }
-  );
-
-  // Add the normalized formula to the queue
-  d_assertions.push_back(n, isAssumption);
-  //d_assertions.push_back(Rewriter::rewrite(n));
-}
+  d_assertionsProcessed = true;
 
-void SmtEngine::ensureBoolean(const Node& n)
-{
-  TypeNode type = n.getType(options::typeChecking());
-  TypeNode boolType = NodeManager::currentNM()->booleanType();
-  if(type != boolType) {
-    stringstream ss;
-    ss << "Expected " << boolType << "\n"
-       << "The assertion : " << n << "\n"
-       << "Its type      : " << type;
-    throw TypeCheckingException(n.toExpr(), ss.str());
-  }
+  // clear the current assertions
+  as.clearCurrent();
 }
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
   Dump("benchmark") << CheckSatCommand(assumption);
-  return checkSatisfiability(assumption, inUnsatCore, false);
+  return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false);
 }
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
@@ -1284,36 +1160,46 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
   {
     Dump("benchmark") << CheckSatAssumingCommand(assumptions);
   }
-
-  return checkSatisfiability(assumptions, inUnsatCore, false);
+  std::vector<Node> assumps;
+  for (const Expr& e : assumptions)
+  {
+    assumps.push_back(Node::fromExpr(e));
+  }
+  return checkSatisfiability(assumps, inUnsatCore, false);
 }
 
-Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
 {
-  Dump("benchmark") << QueryCommand(expr, inUnsatCore);
-  return checkSatisfiability(
-             expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
-             inUnsatCore,
-             true)
+  Dump("benchmark") << QueryCommand(node, inUnsatCore);
+  return checkSatisfiability(node.isNull()
+                                 ? std::vector<Node>()
+                                 : std::vector<Node>{Node::fromExpr(node)},
+                             inUnsatCore,
+                             true)
       .asEntailmentResult();
 }
 
-Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore)
 {
-  return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
+  std::vector<Node> ns;
+  for (const Expr& e : nodes)
+  {
+    ns.push_back(Node::fromExpr(e));
+  }
+  return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult();
 }
 
-Result SmtEngine::checkSatisfiability(const Expr& expr,
+Result SmtEngine::checkSatisfiability(const Node& node,
                                       bool inUnsatCore,
                                       bool isEntailmentCheck)
 {
   return checkSatisfiability(
-      expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
+      node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
       inUnsatCore,
       isEntailmentCheck);
 }
 
-Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
+Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
                                       bool inUnsatCore,
                                       bool isEntailmentCheck)
 {
@@ -1333,70 +1219,23 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
                            "(try --incremental)");
     }
 
-    // Note that a query has been made
+    // Note that a query has been made and we are in assert mode
     d_queryMade = true;
-    // reset global negation
-    d_globalNegation = false;
+    d_smtMode = SMT_MODE_ASSERT;
 
+    // push if there are assumptions
     bool didInternalPush = false;
-
-    setProblemExtended();
-
-    if (isEntailmentCheck)
-    {
-      size_t size = assumptions.size();
-      if (size > 1)
-      {
-        /* Assume: not (BIGAND assumptions)  */
-        d_assumptions.push_back(
-            d_exprManager->mkExpr(kind::AND, assumptions).notExpr());
-      }
-      else if (size == 1)
-      {
-        /* Assume: not expr  */
-        d_assumptions.push_back(assumptions[0].notExpr());
-      }
-    }
-    else
-    {
-      /* Assume: BIGAND assumptions  */
-      d_assumptions = assumptions;
-    }
-
-    if (!d_assumptions.empty())
+    if (!assumptions.empty())
     {
       internalPush();
       didInternalPush = true;
     }
 
-    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    for (Expr e : d_assumptions)
-    {
-      // Substitute out any abstract values in ex.
-      Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e));
-      // Ensure expr is type-checked at this point.
-      ensureBoolean(n);
+    // then, initialize the assertions
+    d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
 
-      /* Add assumption  */
-      if (d_assertionList != NULL)
-      {
-        d_assertionList->push_back(n);
-      }
-      d_private->addFormula(n, inUnsatCore, true, true);
-    }
-
-    if (d_globalDefineFunRecLemmas != nullptr)
-    {
-      // Global definitions are asserted at check-sat-time because we have to
-      // make sure that they are always present (they are essentially level
-      // zero assertions)
-      for (const Node& lemma : *d_globalDefineFunRecLemmas)
-      {
-        d_private->addFormula(lemma, false, true, false, false);
-      }
-    }
-
-    r = check();
+    // make the check
+    Result r = check();
 
     if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -1404,7 +1243,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     }
     // flipped if we did a global negation
-    if (d_globalNegation)
+    if (d_asserts->isGlobalNegated())
     {
       Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -1492,7 +1331,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
   }
 }
 
-vector<Expr> SmtEngine::getUnsatAssumptions(void)
+std::vector<Node> SmtEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
   SmtScope smts(this);
@@ -1514,10 +1353,14 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void)
     Dump("benchmark") << GetUnsatAssumptionsCommand();
   }
   UnsatCore core = getUnsatCoreInternal();
-  vector<Expr> res;
-  for (const Expr& e : d_assumptions)
+  std::vector<Node> res;
+  std::vector<Node>& assumps = d_asserts->getAssumptions();
+  for (const Node& e : assumps)
   {
-    if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); }
+    if (std::find(core.begin(), core.end(), e.toExpr()) != core.end())
+    {
+      res.push_back(e);
+    }
   }
   return res;
 }
@@ -1537,12 +1380,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
   // Substitute out any abstract values in ex
   Node n = d_absValues->substituteAbstractValues(formula);
 
-  ensureBoolean(n);
-  if(d_assertionList != NULL) {
-    d_assertionList->push_back(n);
-  }
-  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
-  d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv);
+  d_asserts->assertFormula(n, inUnsatCore);
   return quickCheck().asEntailmentResult();
 }/* SmtEngine::assertFormula() */
 
@@ -1801,7 +1639,7 @@ Expr SmtEngine::simplify(const Expr& ex)
   }
 
   // Make sure all preprocessing is done
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   Node n = d_private->simplify(Node::fromExpr(e));
   n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
@@ -2233,9 +2071,10 @@ void SmtEngine::checkUnsatCore() {
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
+  context::CDList<Node>* al = d_asserts->getAssertionList();
   // --check-model implies --produce-assertions, which enables the
   // assertion list, so we should be ok.
-  Assert(d_assertionList != NULL)
+  Assert(al != nullptr)
       << "don't have an assertion list to check in SmtEngine::checkModel()";
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
@@ -2354,7 +2193,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   }
 
   // Now go through all our user assertions checking if they're satisfied.
-  for (const Node& assertion : *d_assertionList)
+  for (const Node& assertion : *al)
   {
     Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
              << endl;
@@ -2507,7 +2346,8 @@ void SmtEngine::checkSynthSolution()
 
   Trace("check-synth-sol") << "Retrieving assertions\n";
   // Build conjecture from original assertions
-  if (d_assertionList == NULL)
+  context::CDList<Node>* al = d_asserts->getAssertionList();
+  if (al == nullptr)
   {
     Trace("check-synth-sol") << "No assertions to check\n";
     return;
@@ -2516,7 +2356,7 @@ void SmtEngine::checkSynthSolution()
   std::vector<Node> auxAssertions;
   // expand definitions cache
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  for (const Node& assertion : *d_assertionList)
+  for (const Node& assertion : *al)
   {
     Notice() << "SmtEngine::checkSynthSolution(): checking assertion "
              << assertion << endl;
@@ -2857,9 +2697,10 @@ vector<Expr> SmtEngine::getAssertions() {
       "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
   }
-  Assert(d_assertionList != NULL);
+  context::CDList<Node>* al = d_asserts->getAssertionList();
+  Assert(al != nullptr);
   std::vector<Expr> res;
-  for (const Node& n : *d_assertionList)
+  for (const Node& n : *al)
   {
     res.emplace_back(n.toExpr());
   }
@@ -2874,7 +2715,7 @@ void SmtEngine::push()
   doPendingPops();
   Trace("smt") << "SMT push()" << endl;
   d_private->notifyPush();
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand();
   }
@@ -2886,7 +2727,7 @@ void SmtEngine::push()
   // The problem isn't really "extended" yet, but this disallows
   // get-model after a push, simplifying our lives somewhat and
   // staying symmetric with pop.
-  setProblemExtended();
+  d_smtMode = SMT_MODE_ASSERT;
 
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
@@ -2914,7 +2755,7 @@ void SmtEngine::pop() {
   // but also it would be weird to have a legally-executed (get-model)
   // that only returns a subset of the assignment (because the rest
   // is no longer in scope!).
-  setProblemExtended();
+  d_smtMode = SMT_MODE_ASSERT;
 
   AlwaysAssert(d_userContext->getLevel() > 0);
   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
@@ -2924,6 +2765,7 @@ void SmtEngine::pop() {
   d_userLevels.pop_back();
 
   // Clear out assertion queues etc., in case anything is still in there
+  d_asserts->clearCurrent();
   d_private->notifyPop();
 
   Trace("userpushpop") << "SmtEngine: popped to level "
@@ -2937,7 +2779,7 @@ void SmtEngine::internalPush() {
   Trace("smt") << "SmtEngine::internalPush()" << endl;
   doPendingPops();
   if(options::incrementalSolving()) {
-    d_private->processAssertions();
+    d_private->processAssertions(*d_asserts);
     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
     d_userContext->push();
     // the d_context push is done inside of the SAT solver
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).