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, 2 insertions, 7 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3f24c8bab..672bec821 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -96,7 +96,7 @@ namespace smt {
   struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
-  class BooleanTermConverter;
+  class ProcessAssertions;
 
   ProofManager* currentProofManager();
 
@@ -130,7 +130,7 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::preprocessing::PreprocessingPassContext;
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
-  friend class ::CVC4::smt::BooleanTermConverter;
+  friend class ::CVC4::smt::ProcessAssertions;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::Model;  // to access d_modelCommands
@@ -1131,11 +1131,6 @@ class CVC4_PUBLIC SmtEngine
    */
   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.