Split ProcessAssertions module from SmtEngine (#4210)

This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.

The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:

A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.

1 files changed, 60 insertions, 0 deletions

diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
new file mode 100644
index 000000000..b141ef9cb
--- /dev/null
+++ b/src/smt/defined_function.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file defined_function.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 Defined function data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__DEFINED_FUNCTION_H
+#define CVC4__SMT__DEFINED_FUNCTION_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * Representation of a defined function.  We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction
+{
+ public:
+  DefinedFunction() {}
+  DefinedFunction(Node func, std::vector<Node>& formals, Node formula)
+      : d_func(func), d_formals(formals), d_formula(formula)
+  {
+  }
+  /** get the function */
+  Node getFunction() const { return d_func; }
+  /** get the formal argument list of the function */
+  const std::vector<Node>& getFormals() const { return d_formals; }
+  /** get the formula that defines it */
+  Node getFormula() const { return d_formula; }
+
+ private:
+  /** the function */
+  Node d_func;
+  /** the formal argument list */
+  std::vector<Node> d_formals;
+  /** the formula */
+  Node d_formula;
+}; /* class DefinedFunction */
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__DEFINED_FUNCTION_H */