Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)

This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.

The changes that were required for this PR include:

The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.

1 files changed, 9 insertions, 37 deletions

diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index b606657bb..64646ac05 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -31,49 +31,18 @@ namespace CVC4 {
 namespace theory {
 
 /**
- * This function initializes the smt engine smte as a subsolver, e.g. it
- * creates a new SMT engine and sets the options of the current SMT engine.
- */
-void initializeSubsolver(SmtEngine* smte);
-
-/**
- * Initialize Smt subsolver with exporting
- *
  * This function initializes the smt engine smte to check the satisfiability
  * of the argument "query".
  *
- * The arguments em and varMap are used for supporting cases where we
- * want smte to use a different expression manager instead of the current
- * expression manager. The motivation for this so that different options can
- * be set for the subcall.
- *
- * Notice that subsequent expressions extracted from smte (for instance, model
- * values) must be exported to the current expression
- * manager.
- *
  * @param smte The smt engine pointer to initialize
- * @param em Reference to the expression manager used by smte
- * @param varMap Map used for exporting expressions
- * @param query The query to check
+ * @param query The query to check (if provided)
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
-void initializeSubsolverWithExport(SmtEngine* smte,
-                                   ExprManager* em,
-                                   ExprManagerMapCollection& varMap,
-                                   Node query,
-                                   bool needsTimeout = false,
-                                   unsigned long timeout = 0);
-
-/**
- * This function initializes the smt engine smte to check the satisfiability
- * of the argument "query", without exporting expressions.
- *
- * Notice that is not possible to set a timeout value currently without
- * exporting since the Options and ExprManager are tied together.
- * TODO: eliminate this dependency (cvc4-projects #120).
- */
-void initializeSubsolver(SmtEngine* smte, Node query);
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         Node query = Node::null(),
+                         bool needsTimeout = false,
+                         unsigned long timeout = 0);
 
 /**
  * This returns the result of checking the satisfiability of formula query.
@@ -81,7 +50,10 @@ void initializeSubsolver(SmtEngine* smte, Node query);
  * If necessary, smte is initialized to the SMT engine that checked its
  * satisfiability.
  */
-Result checkWithSubsolver(SmtEngine* smte, Node query);
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+                          Node query,
+                          bool needsTimeout = false,
+                          unsigned long timeout = 0);
 
 /**
  * This returns the result of checking the satisfiability of formula query.