From: Andrew Reynolds Date: Wed, 20 Apr 2022 20:04:21 +0000 (-0500) Subject: Add declare-oracle-fun command (#8621) X-Git-Tag: cvc5-1.0.1~239 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e555b3cac196cb141a3a4dbf934f282bfbdd723;p=cvc5.git 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 a3211fed6..23864e71d 100644 --- 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 485ecf1de..e3e1eef91 100644 --- 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& 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 7d5dc1cc5..fe54a6b8d 100644 --- 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 ad417b256..72b6a0eb3 100644 --- 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 eebb5f471..a5956d63a 100644 --- 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 72a7edb24..ddc9ca82e 100644 --- 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: