Standardize the interface for SMT engine subsolvers (#3836)

This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.

This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).

Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).

1 files changed, 119 insertions, 0 deletions

diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
new file mode 100644
index 000000000..135175665
--- /dev/null
+++ b/src/theory/smt_engine_subsolver.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file smt_engine_subsolver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Utilities for initializing subsolvers (copies of SmtEngine) during
+ ** solving.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
+#define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
+
+#include <map>
+#include <memory>
+#include <vector>
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/variable_type_map.h"
+#include "smt/smt_engine.h"
+
+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(std::unique_ptr<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 to use
+ * @param varMap Map used for exporting expressions
+ * @param query The query to check
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+void initializeSubsolverWithExport(std::unique_ptr<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(std::unique_ptr<SmtEngine>& smte, Node query);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ *
+ * If necessary, smte is initialized to the SMT engine that checked its
+ * satisfiability.
+ */
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ *
+ * In contrast to above, this is used if the user of this method is not
+ * concerned with the state of the SMT engine after the check.
+ *
+ * @param query The query to check
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+Result checkWithSubsolver(Node query,
+                          bool needsTimeout = false,
+                          unsigned long timeout = 0);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ * Additionally, if the query is satisfiable, it adds the model values for vars
+ * into modelVars.
+ *
+ * @param query The query to check
+ * @param vars The variables we are interesting in getting a model for.
+ * @param modelVals A vector storing the model values of variables in vars.
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+Result checkWithSubsolver(Node query,
+                          const std::vector<Node>& vars,
+                          std::vector<Node>& modelVals,
+                          bool needsTimeout = false,
+                          unsigned long timeout = 0);
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */