From: Andrew Reynolds Date: Tue, 12 Apr 2022 14:59:14 +0000 (-0500) Subject: Add oracle caller utility (#8599) X-Git-Tag: cvc5-1.0.1~271 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0dff5a6cbccb75c2ef1247243c30c0979d3d7617;p=cvc5.git Add oracle caller utility (#8599) The implementation of this class has a placeholder for calling external binaries, which will be filled in a later PR. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index d6a7cf47f..32da6002e 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -60,6 +60,8 @@ libcvc5_add_sources( node_traversal.h node_value.cpp node_value.h + oracle_caller.cpp + oracle_caller.h sequence.cpp sequence.h node_visitor.h diff --git a/src/expr/oracle_caller.cpp b/src/expr/oracle_caller.cpp new file mode 100644 index 000000000..dccddf7f0 --- /dev/null +++ b/src/expr/oracle_caller.cpp @@ -0,0 +1,102 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Elizabeth Polgreen + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Oracle caller + */ + +#include "expr/oracle_caller.h" + +#include + +#include "options/base_options.h" +#include "theory/quantifiers/quantifiers_attributes.h" + +namespace cvc5::internal { + +OracleCaller::OracleCaller(const Node& oracleInterfaceNode) + : d_binaryName(getBinaryNameFor(oracleInterfaceNode)) +{ +} + +bool OracleCaller::callOracle(const Node& fapp, Node& res, int& runResult) +{ + std::map::iterator it = d_cachedResults.find(fapp); + if (it != d_cachedResults.end()) + { + Trace("oracle-calls") << "Using cached oracle result for " << fapp + << std::endl; + res = it->second; + // don't bother setting runResult + return false; + } + Assert(fapp.getKind() == kind::APPLY_UF); + Assert(getBinaryNameFor(fapp.getOperator()) == d_binaryName); + std::vector sargs; + sargs.push_back(d_binaryName); + + Trace("oracle-calls") << "Call oracle " << fapp << std::endl; + for (const Node& arg : fapp) + { + std::ostringstream oss; + oss << arg; + sargs.push_back(oss.str()); + } + + // Run the oracle binary for `sargs`, which indicates a list of + // smt2 terms as strings. + + // Parse response from the binary into a Node. The response from the binary + // should be a string that can be parsed as a (tuple of) terms in the smt2 + // format. + Node response = Node::null(); + Trace("oracle-calls") << "response node " << response << std::endl; + d_cachedResults[fapp] = response; + res = response; + return true; +} + +bool OracleCaller::isOracleFunction(Node f) +{ + return f.hasAttribute(theory::OracleInterfaceAttribute()); +} + +std::string OracleCaller::getBinaryName() const { return d_binaryName; } + +std::string OracleCaller::getBinaryNameFor(const Node& n) +{ + // oracle functions have no children + if (n.isVar()) + { + Assert(isOracleFunction(n)); + return n.getAttribute(theory::OracleInterfaceAttribute()); + } + else if (n.getKind() == kind::FORALL) + { + // oracle interfaces have children, and the attribute is stored in 2nd child + for (const Node& v : n[2][0]) + { + if (v.getAttribute(theory::OracleInterfaceAttribute()) != "") + { + return v.getAttribute(theory::OracleInterfaceAttribute()); + } + } + } + Assert(false) << "Unexpected node for binary name " << n; + return ""; +} + +const std::map& OracleCaller::getCachedResults() const +{ + return d_cachedResults; +} + +} // namespace cvc5::internal diff --git a/src/expr/oracle_caller.h b/src/expr/oracle_caller.h new file mode 100644 index 000000000..449bc0a08 --- /dev/null +++ b/src/expr/oracle_caller.h @@ -0,0 +1,79 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Elizabeth Polgreen + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Oracle caller + */ + +#include "cvc5_private.h" + +#ifndef CVC5__EXPR__ORACLE_CALLER_H +#define CVC5__EXPR__ORACLE_CALLER_H + +#include "expr/node.h" +#include "expr/node_trie.h" + +namespace cvc5::internal { + +/** + * This class manages the calls to an (external) binary for a single oracle + * function symbol or oracle interface quantified formula. + */ +class OracleCaller +{ + public: + /** + * @param oracleInterfaceNode The oracle function symbol or oracle interface + * quantified formula. + */ + OracleCaller(const Node& oracleInterfaceNode); + + ~OracleCaller() {} + + /** + * Call an oracle with a set of arguments given as children of the application + * fapp. Store in result res. + * + * Return true if the call was made, and false if it was already cached. + * + * If this method returns true, then runResult is set to the result returned + * from executing the binary. + */ + bool callOracle(const Node& fapp, Node& res, int& runResult); + + /** Get the binary name for this oracle caller */ + std::string getBinaryName() const; + + /** Get cached results for this oracle caller */ + const std::map& getCachedResults() const; + + /** + * Get binary from an oracle function, or an oracle interface quantified + * formula. + */ + static std::string getBinaryNameFor(const Node& n); + + /** is f an oracle function? */ + static bool isOracleFunction(Node f); + + private: + /** name of binary */ + std::string d_binaryName; + /** + * The cached results, mapping (APPLY_UF) applications of the oracle + * function to the parsed output of the binary. + */ + std::map d_cachedResults; +}; + +} // namespace cvc5::internal + +#endif /*CVC5__UTIL__ORACLE_CALLER_H*/