SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)

2 files changed, 574 insertions, 546 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 762b21fd8..27ee446fe 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -849,8 +849,8 @@ class SmtEnginePrivate : public NodeManagerListener {
 
 SmtEngine::SmtEngine(ExprManager* em)
     : d_context(new Context()),
-      d_userLevels(),
       d_userContext(new UserContext()),
+      d_userLevels(),
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_decisionEngine(NULL),
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f032d202a..eba73c380 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -65,19 +65,27 @@ class Model;
 class LogicRequest;
 class StatisticsRegistry;
 
+/* -------------------------------------------------------------------------- */
+
 namespace context {
   class Context;
   class UserContext;
 }/* CVC4::context namespace */
 
+/* -------------------------------------------------------------------------- */
+
 namespace preprocessing {
 class PreprocessingPassContext;
 }
 
+/* -------------------------------------------------------------------------- */
+
 namespace prop {
   class PropEngine;
 }/* CVC4::prop namespace */
 
+/* -------------------------------------------------------------------------- */
+
 namespace smt {
   /**
    * Representation of a defined function.  We keep these around in
@@ -98,6 +106,8 @@ namespace smt {
   typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
+/* -------------------------------------------------------------------------- */
+
 namespace theory {
   class TheoryModel;
 }/* CVC4::theory namespace */
@@ -113,345 +123,10 @@ namespace theory {
 //
 // The CNF conversion can go on in PropEngine.
 
-class CVC4_PUBLIC SmtEngine {
-
-  /** The type of our internal map of defined functions */
-  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
-    DefinedFunctionMap;
-  /** The type of our internal assertion list */
-  typedef context::CDList<Expr> AssertionList;
-  /** The type of our internal assignment set */
-  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
-  /** The types for the recursive function definitions */
-  typedef context::CDList<Node> NodeList;
-
-  /** Expr manager context */
-  context::Context* d_context;
-
-  /** The context levels of user pushes */
-  std::vector<int> d_userLevels;
-  /** User level context */
-  context::UserContext* d_userContext;
-
-  /** Our expression manager */
-  ExprManager* d_exprManager;
-  /** Our internal expression/node manager */
-  NodeManager* d_nodeManager;
-  /** The decision engine */
-  DecisionEngine* d_decisionEngine;
-  /** The theory engine */
-  TheoryEngine* d_theoryEngine;
-  /** The propositional engine */
-  prop::PropEngine* d_propEngine;
-  /** The proof manager */
-  ProofManager* d_proofManager;
-  /** An index of our defined functions */
-  DefinedFunctionMap* d_definedFunctions;
-  /** The SMT engine subsolver
-   *
-   * This is a separate copy of the SMT engine which is used for making
-   * calls that cannot be answered by this copy of the SMT engine. An example
-   * of invoking this subsolver is the get-abduct command, where we wish to
-   * solve a sygus conjecture based on the current assertions. In particular,
-   * consider the input:
-   *   (assert A)
-   *   (get-abduct B)
-   * In the copy of the SMT engine where these commands are issued, we maintain
-   * A in the assertion stack. To solve the abduction problem, instead of
-   * modifying the assertion stack to remove A and add the sygus conjecture
-   * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
-   * assertion stack unchaged. This copy of the SMT engine can be further
-   * queried for information regarding further solutions.
-   */
-  std::unique_ptr<SmtEngine> d_subsolver;
-  /**
-   * If applicable, the function-to-synthesize that the subsolver is solving
-   * for. This is used for the get-abduct command.
-   */
-  Expr d_sssf;
-  /**
-   * The conjecture of the current abduction problem. This expression is only
-   * valid while we are in mode SMT_MODE_ABDUCT.
-   */
-  Expr d_abdConj;
-  /** recursive function definition abstractions for --fmf-fun */
-  std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
-  std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
-  NodeList* d_fmfRecFunctionsDefined;
-
-  /**
-   * The assertion list (before any conversion) for supporting
-   * getAssertions().  Only maintained if in interactive mode.
-   */
-  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;
-
-  /**
-   * A list of commands that should be in the Model globally (i.e.,
-   * regardless of push/pop).  Only maintained if produce-models option
-   * is on.
-   */
-  std::vector<Command*> d_modelGlobalCommands;
-
-  /**
-   * A list of commands that should be in the Model locally (i.e.,
-   * it is context-dependent on push/pop).  Only maintained if
-   * produce-models option is on.
-   */
-  smt::CommandList* d_modelCommands;
-
-  /**
-   * A vector of declaration commands waiting to be dumped out.
-   * Once the SmtEngine is fully initialized, we'll dump them.
-   * This ensures the declarations come after the set-logic and
-   * any necessary set-option commands are dumped.
-   */
-  std::vector<Command*> d_dumpCommands;
-
-  /**
-   * A vector of command definitions to be imported in the new
-   * SmtEngine when checking unsat-cores.
-   */
-  std::vector<Command*> d_defineCommands;
-
-  /**
-   * The logic we're in.
-   */
-  LogicInfo d_logic;
-
-  /**
-   * Keep a copy of the original option settings (for reset()).
-   */
-  Options d_originalOptions;
-
-  /** whether this is an internal subsolver */
-  bool d_isInternalSubsolver;
-
-  /**
-   * Number of internal pops that have been deferred.
-   */
-  unsigned d_pendingPops;
-
-  /**
-   * Whether or not this SmtEngine is fully initialized (post-construction).
-   * This post-construction initialization is automatically triggered by the
-   * use of the SmtEngine; e.g. when the first formula is asserted, a call
-   * to simplify() is issued, a scope is pushed, etc.
-   */
-  bool d_fullyInited;
-
-  /**
-   * Whether or not a query() or checkSat() has already been made through
-   * this SmtEngine.  If true, and incrementalSolving is false, then
-   * attempting an additional query() or checkSat() will fail with a
-   * ModalException.
-   */
-  bool d_queryMade;
-
-  /**
-   * Internal status flag to indicate whether we've sent a theory
-   * presolve() notification and need to match it with a postsolve().
-   */
-  bool d_needPostsolve;
-
-  /*
-   * Whether to call theory preprocessing during simplification - on
-   * by default* but gets turned off if arithRewriteEq is on
-   */
-  bool d_earlyTheoryPP;
-
-  /*
-   * Whether we did a global negation of the formula.
-   */
-  bool d_globalNegation;
-
-  /**
-   * Most recent result of last checkSat/query or (set-info :status).
-   */
-  Result d_status;
-
-  /**
-   * The expected status of the next satisfiability check.
-   */
-  Result d_expectedStatus;
-
-  /**
-   * The current mode of the solver, see Figure 4.1 on page 52 of the
-   * SMT-LIB version 2.6 standard
-   * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
-   */
-  enum SmtMode
-  {
-    // the initial state of the solver
-    SMT_MODE_START,
-    // normal state of the solver, after assert/push/pop/declare/define
-    SMT_MODE_ASSERT,
-    // immediately after a check-sat returning "sat" or "unknown"
-    SMT_MODE_SAT,
-    // immediately after a check-sat returning "unsat"
-    SMT_MODE_UNSAT,
-    // immediately after a successful call to get-abduct
-    SMT_MODE_ABDUCT
-  };
-  SmtMode d_smtMode;
-
-  /**
-   * The input file name (if any) or the name set through setInfo (if any)
-   */
-  std::string d_filename;
-
-  /**
-   * Verbosity of various commands.
-   */
-  std::map<std::string, Integer> d_commandVerbosity;
-  
-
-  /** ReplayStream for the solver. */
-  ExprStream* d_replayStream;
-
-  /**
-   * A private utility class to SmtEngine.
-   */
-  smt::SmtEnginePrivate* d_private;
-
-  /**
-   * Check that a generated proof (via getProof()) checks.
-   */
-  void checkProof();
-
-  /**
-   * Internal method to get an unsatisfiable core (only if immediately preceded
-   * by an UNSAT or VALID query). Only permitted if CVC4 was built with
-   * unsat-core support and produce-unsat-cores is on. Does not dump the
-   * command.
-   */
-  UnsatCore getUnsatCoreInternal();
-
-  /**
-   * Check that an unsatisfiable core is indeed unsatisfiable.
-   */
-  void checkUnsatCore();
-
-  /**
-   * Check that a generated Model (via getModel()) actually satisfies
-   * all user assertions.
-   */
-  void checkModel(bool hardFailure = true);
-
-  /**
-   * Check that a solution to a synthesis conjecture is indeed a solution.
-   *
-   * The check is made by determining if the negation of the synthesis
-   * conjecture in which the functions-to-synthesize have been replaced by the
-   * synthesized solutions, which is a quantifier-free formula, is
-   * unsatisfiable. If not, then the found solutions are wrong.
-   */
-  void checkSynthSolution();
-  /**
-   * Check that a solution to an abduction conjecture is indeed a solution.
-   *
-   * The check is made by determining that the assertions conjoined with the
-   * solution to the abduction problem (a) is SAT, and the assertions conjoined
-   * with the abduct and the goal is UNSAT. If these criteria are not met, an
-   * internal error is thrown.
-   */
-  void checkAbduct(Expr a);
-
-  /**
-   * Postprocess a value for output to the user.  Involves doing things
-   * like turning datatypes back into tuples, length-1-bitvectors back
-   * into booleans, etc.
-   */
-  Node postprocess(TNode n, TypeNode expectedType) const;
-
-  /**
-   * This is something of an "init" procedure, but is idempotent; call
-   * as often as you like.  Should be called whenever the final options
-   * and logic for the problem are set (at least, those options that are
-   * not permitted to change after assertions and queries are made).
-   */
-  void finalOptionsAreSet();
-
-  /**
-   * Apply heuristics settings and other defaults.  Done once, at
-   * finishInit() time.
-   */
-  void setDefaults();
-
-  /**
-   * 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()
-   */
-  void finishInit();
-
-  /**
-   * This is called by the destructor, just before destroying the
-   * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
-   * is important because there are destruction ordering issues
-   * between PropEngine and Theory.
-   */
-  void shutdown();
-
-  /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
-
-  /**
-   * Quick check of consistency in current context: calls
-   * processAssertionList() then look for inconsistency (based only on
-   * that).
-   */
-  Result quickCheck();
-  /** get the model, if it is available and return a pointer to it
-   *
-   * This ensures that the model is currently available, which means that
-   * CVC4 is producing models, and is in "SAT mode", otherwise an exception
-   * is thrown.
-   *
-   * The flag c is used for giving an error message to indicate the context
-   * this method was called.
-   */
-  theory::TheoryModel* getAvailableModel(const char* c) const;
-
-  /**
-   * Fully type-check the argument, and also type-check that it's
-   * actually Boolean.
-   */
-  void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */;
-
-  void internalPush();
-
-  void internalPop(bool immediate = false);
-
-  void doPendingPops();
-
-  /**
-   * Internally handle the setting of a logic.  This function should always
-   * be called when d_logic is updated.
-   */
-  void setLogicInternal() /* throw() */;
+/* -------------------------------------------------------------------------- */
 
+class CVC4_PUBLIC SmtEngine
+{
   // TODO (Issue #1096): Remove this friend relationship.
   friend class ::CVC4::preprocessing::PreprocessingPassContext;
   friend class ::CVC4::smt::SmtEnginePrivate;
@@ -459,83 +134,16 @@ class CVC4_PUBLIC SmtEngine {
   friend class ::CVC4::smt::BooleanTermConverter;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
-  // to access d_modelCommands
-  friend class ::CVC4::Model;
+  friend class ::CVC4::Model;  // to access d_modelCommands
   friend class ::CVC4::theory::TheoryModel;
 
-  StatisticsRegistry* d_statisticsRegistry;
-
-  smt::SmtEngineStatistics* d_stats;
-
-  /** Container for the lemma input and output channels for this SmtEngine.*/
-  LemmaChannels* d_channels;
-
-  /**
-   * Add to Model command.  This is used for recording a command
-   * that should be reported during a get-model call.
-   */
-  void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
-
-  // disallow copy/assignment
-  SmtEngine(const SmtEngine&) = delete;
-  SmtEngine& operator=(const SmtEngine&) = delete;
-
-  //check satisfiability (for query and check-sat)
-  Result checkSatisfiability(const Expr& assumption,
-                             bool inUnsatCore,
-                             bool isQuery);
-  Result checkSatisfiability(const std::vector<Expr>& assumptions,
-                             bool inUnsatCore,
-                             bool isQuery);
-
-  /**
-   * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
-   * the function that the formal argument list is for. This method is used
-   * as a helper function when defining (recursive) functions.
-   */
-  void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
-
-  /**
-   * Checks whether formula is a valid function body for func whose formal
-   * argument list is stored in formals. This method is
-   * used as a helper function when defining (recursive) functions.
-   */
-  void debugCheckFunctionBody(Expr formula,
-                              const std::vector<Expr>& formals,
-                              Expr func);
-  /** get abduct internal
-   *
-   * Gets the next abduct from the internal subsolver d_subsolver. If
-   * successful, this method returns true and sets abd to that abduct.
-   *
-   * This method assumes d_subsolver has been initialized to do abduction
-   * problems.
-   */
-  bool getAbductInternal(Expr& abd);
-
-  /**
-   * Helper method to obtain both the heap and nil from the solver. Returns a
-   * std::pair where the first element is the heap expression and the second
-   * element is the nil expression.
-   */
-  std::pair<Expr, Expr> getSepHeapAndNilExpr();
-
-  /** get expanded assertions
-   *
-   * Returns the set of assertions, after expanding definitions.
-   */
-  std::vector<Expr> getExpandedAssertions();
-
+  /* .......................................................................  */
  public:
+  /* .......................................................................  */
 
-  /**
-   * Construct an SmtEngine with the given expression manager.
-   */
-  SmtEngine(ExprManager* em) /* throw() */;
-
-  /**
-   * Destruct the SMT engine.
-   */
+  /** Construct an SmtEngine with the given expression manager.  */
+  SmtEngine(ExprManager* em);
+  /** Destruct the SMT engine.  */
   ~SmtEngine();
 
   /**
@@ -546,48 +154,44 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool isFullyInited() { return d_fullyInited; }
 
-  /**
-   * Return the user context level.
-   */
+  /** Return the user context level.  */
   size_t getNumUserLevels() { return d_userLevels.size(); }
 
   /**
    * Set the logic of the script.
+   * @throw ModalException, LogicException
    */
-  void setLogic(
-      const std::string& logic) /* throw(ModalException, LogicException) */;
+  void setLogic(const std::string& logic);
 
   /**
    * Set the logic of the script.
+   * @throw ModalException, LogicException
    */
-  void setLogic(const char* logic) /* throw(ModalException, LogicException) */;
+  void setLogic(const char* logic);
 
   /**
    * Set the logic of the script.
+   * @throw ModalException
    */
-  void setLogic(const LogicInfo& logic) /* throw(ModalException) */;
+  void setLogic(const LogicInfo& logic);
 
-  /**
-   * Get the logic information currently set
-   */
+  /** Get the logic information currently set. */
   LogicInfo getLogicInfo() const;
 
   /**
    * Set information about the script executing.
+   * @throw OptionException, ModalException
    */
-  void setInfo(const std::string& key, const CVC4::SExpr& value)
-      /* throw(OptionException, ModalException) */;
+  void setInfo(const std::string& key, const CVC4::SExpr& value);
 
-  /**
-   * Query information about the SMT environment.
-   */
+  /** Query information about the SMT environment.  */
   CVC4::SExpr getInfo(const std::string& key) const;
 
   /**
    * Set an aspect of the current SMT execution environment.
+   * @throw OptionException, ModalException
    */
-  void setOption(const std::string& key, const CVC4::SExpr& value)
-      /* throw(OptionException, ModalException) */;
+  void setOption(const std::string& key, const CVC4::SExpr& value);
 
   /** Set is internal subsolver.
    *
@@ -598,10 +202,11 @@ class CVC4_PUBLIC SmtEngine {
    */
   void setIsInternalSubsolver();
 
-  /** sets the input name */
+  /** set the input name */
   void setFilename(std::string filename);
   /** return the input name (if any) */
   std::string getFilename() const;
+
   /**
    * Get the model (only if immediately preceded by a SAT
    * or INVALID query).  Only permitted if produce-models is on.
@@ -634,21 +239,17 @@ class CVC4_PUBLIC SmtEngine {
    */
   Result blockModelValues(const std::vector<Expr>& exprs);
 
-  /**
-   * When using separation logic, obtain the expression for the heap.
-   */
+  /** When using separation logic, obtain the expression for the heap.  */
   Expr getSepHeapExpr();
 
-  /**
-   * When using separation logic, obtain the expression for nil.
-   */
+  /** When using separation logic, obtain the expression for nil.  */
   Expr getSepNilExpr();
 
   /**
    * Get an aspect of the current SMT execution environment.
+   * @throw OptionException
    */
-  CVC4::SExpr getOption(const std::string& key) const
-      /* throw(OptionException) */;
+  CVC4::SExpr getOption(const std::string& key) const;
 
   /**
    * Define function func in the current context to be:
@@ -665,10 +266,11 @@ class CVC4_PUBLIC SmtEngine {
                       const std::vector<Expr>& formals,
                       Expr formula);
 
-  /** is defined function */
+  /** Return true if given expression is a defined function. */
   bool isDefinedFunction(Expr func);
 
-  /** Define functions recursive
+  /**
+   * Define functions recursive
    *
    * For each i, this constrains funcs[i] in the current context to be:
    *   (lambda (formals[i]) formulas[i])
@@ -685,15 +287,13 @@ class CVC4_PUBLIC SmtEngine {
   void defineFunctionsRec(const std::vector<Expr>& funcs,
                           const std::vector<std::vector<Expr> >& formals,
                           const std::vector<Expr>& formulas);
-
-  /** Define function recursive
-   *
+  /**
+   * Define function recursive
    * Same as above, but for a single function.
    */
   void defineFunctionRec(Expr func,
                          const std::vector<Expr>& formals,
                          Expr formula);
-
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
@@ -701,29 +301,30 @@ class CVC4_PUBLIC SmtEngine {
    * 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
    */
-  Result assertFormula(const Expr& e, bool inUnsatCore = true)
-      /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
-      ;
+  Result assertFormula(const Expr& e, bool inUnsatCore = true);
 
   /**
    * Check validity of an expression with respect to the current set
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
+   *
+   * @throw Exception
    */
-  Result query(const Expr& assumption = Expr(),
-               bool inUnsatCore = true) /* throw(Exception) */;
-  Result query(const std::vector<Expr>& assumptions,
-               bool inUnsatCore = true) /* throw(Exception) */;
+  Result query(const Expr& assumption = Expr(), bool inUnsatCore = true);
+  Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
+   *
+   * @throw Exception
    */
-  Result checkSat(const Expr& assumption = Expr(),
-                  bool inUnsatCore = true) /* throw(Exception) */;
+  Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true);
   Result checkSat(const std::vector<Expr>& assumptions,
-                  bool inUnsatCore = true) /* throw(Exception) */;
+                  bool inUnsatCore = true);
 
   /**
    * Returns a set of so-called "failed" assumptions.
@@ -737,15 +338,18 @@ class CVC4_PUBLIC SmtEngine {
    */
   std::vector<Expr> getUnsatAssumptions(void);
 
-  /*------------------- sygus commands  ------------------*/
+  /*---------------------------- sygus commands  ---------------------------*/
 
-  /** adds a variable declaration
+  /**
+   * Add variable declaration.
    *
    * Declared SyGuS variables may be used in SyGuS constraints, in which they
    * are assumed to be universally quantified.
    */
   void declareSygusVar(const std::string& id, Expr var, Type type);
-  /** stores information for debugging sygus invariants setup
+
+  /**
+   * Store information for debugging sygus invariants setup.
    *
    * Since in SyGuS the commands "declare-primed-var" are not necessary for
    * building invariant constraints, we only use them to check that the number
@@ -753,7 +357,9 @@ class CVC4_PUBLIC SmtEngine {
    * invariant-to-synthesize.
    */
   void declareSygusPrimedVar(const std::string& id, Type type);
-  /** adds a function variable declaration
+
+  /**
+   * Add a function variable declaration.
    *
    * Is SyGuS semantics declared functions are treated in the same manner as
    * declared variables, i.e. as universally quantified (function) variables
@@ -761,7 +367,9 @@ class CVC4_PUBLIC SmtEngine {
    * which a function is being synthesized.
    */
   void declareSygusFunctionVar(const std::string& id, Expr var, Type type);
-  /** adds a function-to-synthesize declaration
+
+  /**
+   * Add a function-to-synthesize declaration.
    *
    * The given type may not correspond to the actual function type but to a
    * datatype encoding the syntax restrictions for the
@@ -780,9 +388,12 @@ class CVC4_PUBLIC SmtEngine {
                        Type type,
                        bool isInv,
                        const std::vector<Expr>& vars);
-  /** adds a regular sygus constraint */
+
+  /** Add a regular sygus constraint.*/
   void assertSygusConstraint(Expr constraint);
-  /** adds an invariant constraint
+
+  /**
+   * Add an invariant constraint.
    *
    * Invariant constraints are not explicitly declared: they are given in terms
    * of the invariant-to-synthesize, the pre condition, transition relation and
@@ -813,10 +424,12 @@ class CVC4_PUBLIC SmtEngine {
    *
    * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
    * universal variables and F is the set of declared constraints.
+   *
+   * @throw Exception
    */
-  Result checkSynth() /* throw(Exception) */;
+  Result checkSynth();
 
-  /*------------------- end of sygus commands-------------*/
+  /*------------------------- end of sygus commands ------------------------*/
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -824,31 +437,30 @@ class CVC4_PUBLIC SmtEngine {
    * definitions, assertions, and the current partial model, if one
    * has been constructed.  It also involves theory normalization.
    *
+   * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+   *
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(
-      const Expr&
-          e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
-      ;
+  Expr simplify(const Expr& e);
 
   /**
    * Expand the definitions in a term or formula.  No other
    * simplification or normalization is done.
+   *
+   * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  Expr expandDefinitions(
-      const Expr&
-          e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
-      ;
+  Expr expandDefinitions(const Expr& e);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
+   *
+   * @throw ModalException, TypeCheckingException, LogicException,
+   *        UnsafeInterruptException
    */
-  Expr getValue(const Expr& e) const
-      /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */
-      ;
+  Expr getValue(const Expr& e) const;
 
   /**
    * Same as getValue but for a vector of expressions
@@ -883,18 +495,17 @@ class CVC4_PUBLIC SmtEngine {
    */
   const Proof& getProof();
 
-  /**
-   * Print all instantiations made by the quantifiers module.
-   */
-  void printInstantiations( std::ostream& out );
+  /** Print all instantiations made by the quantifiers module.  */
+  void printInstantiations(std::ostream& out);
 
   /**
-   * Print solution for synthesis conjectures found by ce_guided_instantiation module
+   * Print solution for synthesis conjectures found by counter-example guided
+   * instantiation module.
    */
-  void printSynthSolution( std::ostream& out );
+  void printSynthSolution(std::ostream& out);
 
   /**
-   * Get synth solution
+   * Get synth solution.
    *
    * This function adds entries to sol_map that map functions-to-synthesize with
    * their solutions, for all active conjectures. This should be called
@@ -951,13 +562,14 @@ class CVC4_PUBLIC SmtEngine {
    * extended command get-qe-disjunct, which can be used
    * for incrementally computing the result of a
    * quantifier elimination.
-   * 
+   *
    * The argument strict is whether to output
    * warnings, such as when an unexpected logic is used.
+   *
+   * throw@ Exception
    */
-  Expr doQuantifierElimination(const Expr& e,
-                               bool doFull,
-                               bool strict = true) /* throw(Exception) */;
+  Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true);
+
   /**
    * This method asks this SMT engine to find an abduct with respect to the
    * current assertion stack (call it A) and the conjecture (call it B).
@@ -971,19 +583,17 @@ class CVC4_PUBLIC SmtEngine {
    * corresponding sygus problem for generating such a solution.
    */
   bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd);
+
   /** Same as above, but without user-provided grammar restrictions */
   bool getAbduct(const Expr& conj, Expr& abd);
 
-  /**
-   * Get list of quantified formulas that were instantiated
-   */
-  void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs );
-   
-  /**
-   * Get instantiations
-   */
-  void getInstantiations( Expr q, std::vector< Expr >& insts );
-  void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs );
+  /** Get list of quantified formulas that were instantiated. */
+  void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs);
+
+  /** Get instantiations. */
+  void getInstantiations(Expr q, std::vector<Expr>& insts);
+  void getInstantiationTermVectors(Expr q,
+                                   std::vector<std::vector<Expr> >& tvecs);
 
   /**
    * Get an unsatisfiable core (only if immediately preceded by an
@@ -1000,12 +610,13 @@ class CVC4_PUBLIC SmtEngine {
 
   /**
    * Push a user-level context.
+   * throw@ ModalException, LogicException, UnsafeInterruptException
    */
-  void
-  push() /* throw(ModalException, LogicException, UnsafeInterruptException) */;
+  void push();
 
   /**
    * Pop a user-level context.  Throws an exception if nothing to pop.
+   * @throw ModalException
    */
   void pop();
 
@@ -1014,19 +625,19 @@ class CVC4_PUBLIC SmtEngine {
    * recreated.  The result is as if newly constructed (so it still
    * retains the same options structure and ExprManager).
    */
-  void reset() /* throw() */;
+  void reset();
 
-  /**
-   * Reset all assertions, global declarations, etc.
-   */
-  void resetAssertions() /* throw() */;
+  /** Reset all assertions, global declarations, etc.  */
+  void resetAssertions();
 
   /**
    * Interrupt a running query.  This can be called from another thread
    * or from a signal handler.  Throws a ModalException if the SmtEngine
    * isn't currently in a query.
+   *
+   * @throw ModalException
    */
-  void interrupt() /* throw(ModalException) */;
+  void interrupt();
 
   /**
    * Set a resource limit for SmtEngine operations.  This is like a time
@@ -1100,9 +711,7 @@ class CVC4_PUBLIC SmtEngine {
    */
   unsigned long getResourceUsage() const;
 
-  /**
-   * Get the current millisecond count for this SmtEngine.
-   */
+  /** Get the current millisecond count for this SmtEngine.  */
   unsigned long getTimeUsage() const;
 
   /**
@@ -1110,43 +719,36 @@ class CVC4_PUBLIC SmtEngine {
    * according to the currently-set cumulative resource limit.  If there
    * is not a cumulative resource limit set, this function throws a
    * ModalException.
+   *
+   * @throw ModalException
    */
-  unsigned long getResourceRemaining() const /* throw(ModalException) */;
+  unsigned long getResourceRemaining() const;
 
   /**
    * Get the remaining number of milliseconds that can be consumed by
    * this SmtEngine according to the currently-set cumulative time limit.
    * If there is not a cumulative resource limit set, this function
    * throws a ModalException.
+   *
+   * @throw ModalException
    */
-  unsigned long getTimeRemaining() const /* throw(ModalException) */;
+  unsigned long getTimeRemaining() const;
 
-  /**
-   * Permit access to the underlying ExprManager.
-   */
-  ExprManager* getExprManager() const {
-    return d_exprManager;
-  }
+  /** Permit access to the underlying ExprManager. */
+  ExprManager* getExprManager() const { return d_exprManager; }
 
-  /**
-   * Export statistics from this SmtEngine.
-   */
-  Statistics getStatistics() const /* throw() */;
+  /** Export statistics from this SmtEngine. */
+  Statistics getStatistics() const;
 
-  /**
-   * Get the value of one named statistic from this SmtEngine.
-   */
-  SExpr getStatistic(std::string name) const /* throw() */;
+  /** Get the value of one named statistic from this SmtEngine. */
+  SExpr getStatistic(std::string name) const;
 
-  /**
-   * Flush statistic from this SmtEngine. Safe to use in a signal handler.
-   */
+  /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */
   void safeFlushStatistics(int fd) const;
 
-  /**
-   * Returns the most recent result of checkSat/query or (set-info :status).
-   */
-  Result getStatusOfLastCommand() const /* throw() */ { return d_status; }
+  /** Returns the most recent result of checkSat/query or (set-info :status). */
+  Result getStatusOfLastCommand() const { return d_status; }
+
   /**
    * Set user attribute.
    * This function is called when an attribute is set by a user.
@@ -1157,18 +759,19 @@ class CVC4_PUBLIC SmtEngine {
                         const std::vector<Expr>& expr_values,
                         const std::string& str_value);
 
-  /**
-   * Set print function in model
-   */
+  /** Set print function in model. */
   void setPrintFuncInModel(Expr f, bool p);
 
-
-  /** Throws a ModalException if the SmtEngine has been fully initialized. */
-  void beforeSearch() /* throw(ModalException) */;
+  /**
+   * Check and throw a ModalException if the SmtEngine has been fully
+   * initialized.
+   *
+   * throw@ ModalException
+   */
+  void beforeSearch();
 
   LemmaChannels* channels() { return d_channels; }
 
-
   /**
    * Expermintal feature: Sets the sequence of decisions.
    * This currently requires very fine grained knowledge about literal
@@ -1176,20 +779,445 @@ class CVC4_PUBLIC SmtEngine {
    */
   void setReplayStream(ExprStream* exprStream);
 
-  /** get expression name
-  * Returns true if e has an expression name in the current context.
-  * If it returns true, the name of e is stored in name.
-  */
+  /**
+   * Get expression name.
+   *
+   * Return true if given expressoion has a name in the current context.
+   * If it returns true, the name of expression 'e' is stored in 'name'.
+   */
   bool getExpressionName(Expr e, std::string& name) const;
 
-  /** set expression name 
-  * Sets the expression name of e to name.
-  * This information is user-context-dependent.
-  * If e already has a name, it is overwritten.
-  */
+  /**
+   * Set name of given expression 'e' to 'name'.
+   *
+   * This information is user-context-dependent.
+   * If 'e' already has a name, it is overwritten.
+   */
   void setExpressionName(Expr e, const std::string& name);
 
-};/* class SmtEngine */
+  /* .......................................................................  */
+ private:
+  /* .......................................................................  */
+
+  /** The type of our internal map of defined functions */
+  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
+      DefinedFunctionMap;
+  /** The type of our internal assertion list */
+  typedef context::CDList<Expr> AssertionList;
+  /** The type of our internal assignment set */
+  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
+  /** The types for the recursive function definitions */
+  typedef context::CDList<Node> NodeList;
+
+  /**
+   * The current mode of the solver, see Figure 4.1 on page 52 of the
+   * SMT-LIB version 2.6 standard
+   * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
+   */
+  enum SmtMode
+  {
+    // the initial state of the solver
+    SMT_MODE_START,
+    // normal state of the solver, after assert/push/pop/declare/define
+    SMT_MODE_ASSERT,
+    // immediately after a check-sat returning "sat" or "unknown"
+    SMT_MODE_SAT,
+    // immediately after a check-sat returning "unsat"
+    SMT_MODE_UNSAT,
+    // immediately after a successful call to get-abduct
+    SMT_MODE_ABDUCT
+  };
+
+  // disallow copy/assignment
+  SmtEngine(const SmtEngine&) = delete;
+  SmtEngine& operator=(const SmtEngine&) = delete;
+
+  /**
+   * Check that a generated proof (via getProof()) checks.
+   */
+  void checkProof();
+
+  /**
+   * Internal method to get an unsatisfiable core (only if immediately preceded
+   * by an UNSAT or VALID query). Only permitted if CVC4 was built with
+   * unsat-core support and produce-unsat-cores is on. Does not dump the
+   * command.
+   */
+  UnsatCore getUnsatCoreInternal();
+
+  /**
+   * Check that an unsatisfiable core is indeed unsatisfiable.
+   */
+  void checkUnsatCore();
+
+  /**
+   * Check that a generated Model (via getModel()) actually satisfies
+   * all user assertions.
+   */
+  void checkModel(bool hardFailure = true);
+
+  /**
+   * Check that a solution to a synthesis conjecture is indeed a solution.
+   *
+   * The check is made by determining if the negation of the synthesis
+   * conjecture in which the functions-to-synthesize have been replaced by the
+   * synthesized solutions, which is a quantifier-free formula, is
+   * unsatisfiable. If not, then the found solutions are wrong.
+   */
+  void checkSynthSolution();
+  /**
+   * Check that a solution to an abduction conjecture is indeed a solution.
+   *
+   * The check is made by determining that the assertions conjoined with the
+   * solution to the abduction problem (a) is SAT, and the assertions conjoined
+   * with the abduct and the goal is UNSAT. If these criteria are not met, an
+   * internal error is thrown.
+   */
+  void checkAbduct(Expr a);
+
+  /**
+   * Postprocess a value for output to the user.  Involves doing things
+   * like turning datatypes back into tuples, length-1-bitvectors back
+   * into booleans, etc.
+   */
+  Node postprocess(TNode n, TypeNode expectedType) const;
+
+  /**
+   * This is something of an "init" procedure, but is idempotent; call
+   * as often as you like.  Should be called whenever the final options
+   * and logic for the problem are set (at least, those options that are
+   * not permitted to change after assertions and queries are made).
+   */
+  void finalOptionsAreSet();
+
+  /**
+   * Apply heuristics settings and other defaults.  Done once, at
+   * finishInit() time.
+   */
+  void setDefaults();
+
+  /**
+   * 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()
+   */
+  void finishInit();
+
+  /**
+   * This is called by the destructor, just before destroying the
+   * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
+   * is important because there are destruction ordering issues
+   * between PropEngine and Theory.
+   */
+  void shutdown();
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Get the model, if it is available and return a pointer to it
+   *
+   * This ensures that the model is currently available, which means that
+   * CVC4 is producing models, and is in "SAT mode", otherwise an exception
+   * is thrown.
+   *
+   * The flag c is used for giving an error message to indicate the context
+   * this method was called.
+   */
+  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 Expr& e);
+
+  void internalPush();
+
+  void internalPop(bool immediate = false);
+
+  void doPendingPops();
+
+  /**
+   * Internally handle the setting of a logic.  This function should always
+   * be called when d_logic is updated.
+   */
+  void setLogicInternal();
+
+  /**
+   * Add to Model command.  This is used for recording a command
+   * that should be reported during a get-model call.
+   */
+  void addToModelCommandAndDump(const Command& c,
+                                uint32_t flags = 0,
+                                bool userVisible = true,
+                                const char* dumpTag = "declarations");
+
+  /* Check satisfiability (used for query and check-sat). */
+  Result checkSatisfiability(const Expr& assumption,
+                             bool inUnsatCore,
+                             bool isQuery);
+  Result checkSatisfiability(const std::vector<Expr>& assumptions,
+                             bool inUnsatCore,
+                             bool isQuery);
+
+  /**
+   * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
+   * the function that the formal argument list is for. This method is used
+   * as a helper function when defining (recursive) functions.
+   */
+  void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
+
+  /**
+   * Checks whether formula is a valid function body for func whose formal
+   * argument list is stored in formals. This method is
+   * used as a helper function when defining (recursive) functions.
+   */
+  void debugCheckFunctionBody(Expr formula,
+                              const std::vector<Expr>& formals,
+                              Expr func);
+  /**
+   * Get abduct internal.
+   *
+   * Get the next abduct from the internal subsolver d_subsolver. If
+   * successful, this method returns true and sets abd to that abduct.
+   *
+   * This method assumes d_subsolver has been initialized to do abduction
+   * problems.
+   */
+  bool getAbductInternal(Expr& abd);
+
+  /**
+   * Helper method to obtain both the heap and nil from the solver. Returns a
+   * std::pair where the first element is the heap expression and the second
+   * element is the nil expression.
+   */
+  std::pair<Expr, Expr> getSepHeapAndNilExpr();
+
+  /**
+   * Get expanded assertions.
+   *
+   * Return the set of assertions, after expanding definitions.
+   */
+  std::vector<Expr> getExpandedAssertions();
+
+  /* Members -------------------------------------------------------------- */
+
+  /** Expr manager context */
+  context::Context* d_context;
+  /** User level context */
+  context::UserContext* d_userContext;
+  /** The context levels of user pushes */
+  std::vector<int> d_userLevels;
+
+  /** Our expression manager */
+  ExprManager* d_exprManager;
+  /** Our internal expression/node manager */
+  NodeManager* d_nodeManager;
+  /** The decision engine */
+
+  DecisionEngine* d_decisionEngine;
+  /** The theory engine */
+  TheoryEngine* d_theoryEngine;
+  /** The propositional engine */
+  prop::PropEngine* d_propEngine;
+
+  /** The proof manager */
+  ProofManager* d_proofManager;
+
+  /** An index of our defined functions */
+  DefinedFunctionMap* d_definedFunctions;
+
+  /** The SMT engine subsolver
+   *
+   * This is a separate copy of the SMT engine which is used for making
+   * calls that cannot be answered by this copy of the SMT engine. An example
+   * of invoking this subsolver is the get-abduct command, where we wish to
+   * solve a sygus conjecture based on the current assertions. In particular,
+   * consider the input:
+   *   (assert A)
+   *   (get-abduct B)
+   * In the copy of the SMT engine where these commands are issued, we maintain
+   * A in the assertion stack. To solve the abduction problem, instead of
+   * modifying the assertion stack to remove A and add the sygus conjecture
+   * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
+   * assertion stack unchaged. This copy of the SMT engine can be further
+   * queried for information regarding further solutions.
+   */
+  std::unique_ptr<SmtEngine> d_subsolver;
+
+  /**
+   * If applicable, the function-to-synthesize that the subsolver is solving
+   * for. This is used for the get-abduct command.
+   */
+  Expr d_sssf;
+
+  /**
+   * The conjecture of the current abduction problem. This expression is only
+   * valid while we are in mode SMT_MODE_ABDUCT.
+   */
+  Expr d_abdConj;
+
+  /** recursive function definition abstractions for --fmf-fun */
+  std::map<Node, TypeNode> d_fmfRecFunctionsAbs;
+  std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete;
+  NodeList* d_fmfRecFunctionsDefined;
+
+  /**
+   * The assertion list (before any conversion) for supporting
+   * getAssertions().  Only maintained if in interactive mode.
+   */
+  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;
+
+  /**
+   * A list of commands that should be in the Model globally (i.e.,
+   * regardless of push/pop).  Only maintained if produce-models option
+   * is on.
+   */
+  std::vector<Command*> d_modelGlobalCommands;
+
+  /**
+   * A list of commands that should be in the Model locally (i.e.,
+   * it is context-dependent on push/pop).  Only maintained if
+   * produce-models option is on.
+   */
+  smt::CommandList* d_modelCommands;
+
+  /**
+   * A vector of declaration commands waiting to be dumped out.
+   * Once the SmtEngine is fully initialized, we'll dump them.
+   * This ensures the declarations come after the set-logic and
+   * any necessary set-option commands are dumped.
+   */
+  std::vector<Command*> d_dumpCommands;
+
+  /**
+   * A vector of command definitions to be imported in the new
+   * SmtEngine when checking unsat-cores.
+   */
+  std::vector<Command*> d_defineCommands;
+
+  /**
+   * The logic we're in.
+   */
+  LogicInfo d_logic;
+
+  /**
+   * Keep a copy of the original option settings (for reset()).
+   */
+  Options d_originalOptions;
+
+  /** Whether this is an internal subsolver. */
+  bool d_isInternalSubsolver;
+
+  /**
+   * Number of internal pops that have been deferred.
+   */
+  unsigned d_pendingPops;
+
+  /**
+   * Whether or not this SmtEngine is fully initialized (post-construction).
+   * This post-construction initialization is automatically triggered by the
+   * use of the SmtEngine; e.g. when the first formula is asserted, a call
+   * to simplify() is issued, a scope is pushed, etc.
+   */
+  bool d_fullyInited;
+
+  /**
+   * Whether or not a query() or checkSat() has already been made through
+   * this SmtEngine.  If true, and incrementalSolving is false, then
+   * attempting an additional query() or checkSat() will fail with a
+   * ModalException.
+   */
+  bool d_queryMade;
+
+  /**
+   * Internal status flag to indicate whether we've sent a theory
+   * presolve() notification and need to match it with a postsolve().
+   */
+  bool d_needPostsolve;
+
+  /*
+   * Whether to call theory preprocessing during simplification - on
+   * by default* but gets turned off if arithRewriteEq is on
+   */
+  bool d_earlyTheoryPP;
+
+  /*
+   * Whether we did a global negation of the formula.
+   */
+  bool d_globalNegation;
+
+  /**
+   * Most recent result of last checkSat/query or (set-info :status).
+   */
+  Result d_status;
+
+  /**
+   * The expected status of the next satisfiability check.
+   */
+  Result d_expectedStatus;
+
+  SmtMode d_smtMode;
+
+  /**
+   * The input file name (if any) or the name set through setInfo (if any)
+   */
+  std::string d_filename;
+
+  /**
+   * Verbosity of various commands.
+   */
+  std::map<std::string, Integer> d_commandVerbosity;
+
+  /** ReplayStream for the solver. */
+  ExprStream* d_replayStream;
+
+  /**
+   * A private utility class to SmtEngine.
+   */
+  smt::SmtEnginePrivate* d_private;
+
+  StatisticsRegistry* d_statisticsRegistry;
+
+  smt::SmtEngineStatistics* d_stats;
+
+  /** Container for the lemma input and output channels for this SmtEngine.*/
+  LemmaChannels* d_channels;
+}; /* class SmtEngine */
+
+/* -------------------------------------------------------------------------- */
 
 }/* CVC4 namespace */