Add instantiation pool feature to the API (#6358)

This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.

2 files changed, 80 insertions, 0 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f27ed6e1f..b2a1590b0 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1168,6 +1168,60 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
+/* class DeclareFunctionCommand                                               */
+/* -------------------------------------------------------------------------- */
+
+DeclarePoolCommand::DeclarePoolCommand(const std::string& id,
+                                       api::Term func,
+                                       api::Sort sort,
+                                       const std::vector<api::Term>& initValue)
+    : DeclarationDefinitionCommand(id),
+      d_func(func),
+      d_sort(sort),
+      d_initValue(initValue)
+{
+}
+
+api::Term DeclarePoolCommand::getFunction() const { return d_func; }
+api::Sort DeclarePoolCommand::getSort() const { return d_sort; }
+const std::vector<api::Term>& DeclarePoolCommand::getInitialValue() const
+{
+  return d_initValue;
+}
+
+void DeclarePoolCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+  // Notice that the pool is already declared by the parser so that it the
+  // symbol is bound eagerly. This is analogous to DeclareSygusVarCommand.
+  // Hence, we do nothing here.
+  d_commandStatus = CommandSuccess::instance();
+}
+
+Command* DeclarePoolCommand::clone() const
+{
+  DeclarePoolCommand* dfc =
+      new DeclarePoolCommand(d_symbol, d_func, d_sort, d_initValue);
+  return dfc;
+}
+
+std::string DeclarePoolCommand::getCommandName() const
+{
+  return "declare-pool";
+}
+
+void DeclarePoolCommand::toStream(std::ostream& out,
+                                  int toDepth,
+                                  size_t dag,
+                                  OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclarePool(
+      out,
+      d_func.toString(),
+      sortToTypeNode(d_sort),
+      termVectorToNodes(d_initValue));
+}
+
+/* -------------------------------------------------------------------------- */
 /* class DeclareSortCommand                                                   */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index f14d52e94..07dfa2b30 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -425,6 +425,32 @@ class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DeclareFunctionCommand */
 
+class CVC4_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
+{
+ protected:
+  api::Term d_func;
+  api::Sort d_sort;
+  std::vector<api::Term> d_initValue;
+
+ public:
+  DeclarePoolCommand(const std::string& id,
+                     api::Term func,
+                     api::Sort sort,
+                     const std::vector<api::Term>& initValue);
+  api::Term getFunction() const;
+  api::Sort getSort() const;
+  const std::vector<api::Term>& getInitialValue() const;
+
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+}; /* class DeclarePoolCommand */
+
 class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
 {
  protected: