Add declare-oracle-fun command (#8621)

In preparation for adding declare-oracle-fun to the API/parser.

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a3211fed6f761619f556da5605b2a35748eb15fb..23864e71d8e7ca55bbfa7abeaebea54147ec13c9 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -214,6 +214,13 @@ void Printer::toStreamCmdDeclarePool(std::ostream& out,
   printUnknownCommand(out, "declare-pool");
 }
 
+void Printer::toStreamCmdDeclareOracleFun(std::ostream& out,
+                                          Node fun,
+                                          const std::string& binName) const
+{
+  printUnknownCommand(out, "declare-oracle-fun");
+}
+
 void Printer::toStreamCmdDeclareType(std::ostream& out,
                                      TypeNode type) const
 {

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 485ecf1de491499d0db84e203b3605e33f3798ed..e3e1eef91bc2b790744164a5d3753a48ea1e9804 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -97,6 +97,10 @@ class Printer
                                       const std::string& id,
                                       TypeNode type,
                                       const std::vector<Node>& initValue) const;
+  /** Print declare-oracle-fun command */
+  virtual void toStreamCmdDeclareOracleFun(std::ostream& out,
+                                           Node fun,
+                                           const std::string& binName) const;
 
   /** Print declare-sort command */
   virtual void toStreamCmdDeclareType(std::ostream& out,

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7d5dc1cc524594aec125dbdb18527539ae9d89e7..fe54a6b8dfa7658a0c2dcae51c81e8494068bade 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1579,6 +1579,15 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
   out << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdDeclareOracleFun(std::ostream& out,
+                                              Node fun,
+                                              const std::string& binName) const
+{
+  out << "(declare-oracle-fun " << fun << " ";
+  toStreamDeclareType(out, fun.getType());
+  out << " " << binName << ")" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdDeclarePool(
     std::ostream& out,
     const std::string& id,

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index ad417b2567b2a5e866c0aac8bbcfa5634788d727..72b6a0eb3f86a3d79c44efe4223f85cc11a814ab 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -73,6 +73,12 @@ class Smt2Printer : public cvc5::internal::Printer
   void toStreamCmdDeclareFunction(std::ostream& out,
                                   const std::string& id,
                                   TypeNode type) const override;
+
+  /** Print declare-oracle-fun command */
+  void toStreamCmdDeclareOracleFun(std::ostream& out,
+                                   Node fun,
+                                   const std::string& binName) const override;
+
   /** Print declare-pool command */
   void toStreamCmdDeclarePool(std::ostream& out,
                                       const std::string& id,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index eebb5f471f3800e622cccb9ba396179cd3de1fa1..a5956d63a26d1456e35c836cbab980acfe8887ae 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1116,7 +1116,7 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
-/* class DeclareFunctionCommand                                               */
+/* class DeclarePoolCommand                                               */
 /* -------------------------------------------------------------------------- */
 
 DeclarePoolCommand::DeclarePoolCommand(const std::string& id,
@@ -1169,6 +1169,55 @@ void DeclarePoolCommand::toStream(std::ostream& out,
       termVectorToNodes(d_initValue));
 }
 
+/* -------------------------------------------------------------------------- */
+/* class DeclareOracleFunCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareOracleFunCommand::DeclareOracleFunCommand(Term func)
+    : d_func(func), d_binName("")
+{
+}
+DeclareOracleFunCommand::DeclareOracleFunCommand(Term func,
+                                                 const std::string& binName)
+    : d_func(func), d_binName(binName)
+{
+}
+
+Term DeclareOracleFunCommand::getFunction() const { return d_func; }
+const std::string& DeclareOracleFunCommand::getBinaryName() const
+{
+  return d_binName;
+}
+
+void DeclareOracleFunCommand::invoke(Solver* solver, SymbolManager* sm)
+{
+  // Notice that the oracle function is already declared by the parser so that
+  // the symbol is bound eagerly.
+  // mark that it will be printed in the model
+  sm->addModelDeclarationTerm(d_func);
+  d_commandStatus = CommandSuccess::instance();
+}
+
+Command* DeclareOracleFunCommand::clone() const
+{
+  DeclareOracleFunCommand* dfc = new DeclareOracleFunCommand(d_func, d_binName);
+  return dfc;
+}
+
+std::string DeclareOracleFunCommand::getCommandName() const
+{
+  return "declare-oracle-fun";
+}
+
+void DeclareOracleFunCommand::toStream(std::ostream& out,
+                                       int toDepth,
+                                       size_t dag,
+                                       Language language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareOracleFun(
+      out, termToNode(d_func), d_binName);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DeclareSortCommand                                                   */
 /* -------------------------------------------------------------------------- */

diff --git a/src/smt/command.h b/src/smt/command.h
index 72a7edb241ae3f0239cdcd5db6e725d9551c376a..ddc9ca82e58eaaac83b9177e2c62799086d1e405 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -454,6 +454,30 @@ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
                     internal::Language::LANG_AUTO) const override;
 }; /* class DeclarePoolCommand */
 
+class CVC5_EXPORT DeclareOracleFunCommand : public Command
+{
+ public:
+  DeclareOracleFunCommand(Term func);
+  DeclareOracleFunCommand(Term func, const std::string& binName);
+  Term getFunction() const;
+  const std::string& getBinaryName() const;
+
+  void invoke(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,
+                internal::Language language =
+                    internal::Language::LANG_AUTO) const override;
+
+ protected:
+  /** The oracle function */
+  Term d_func;
+  /** The binary name, or "" if none is provided */
+  std::string d_binName;
+};
+
 class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
 {
  protected: