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 d6a7cf47f5507a86906f1193aa80cd322f48810d..32da6002ea0f1e90d38b7374a48ad3eb9af0786e 100644 (file)
--- 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 (file)
index 0000000..dccddf7
--- /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 <sstream>
+
+#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<Node, Node>::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<std::string> 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<Node, Node>& 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 (file)
index 0000000..449bc0a
--- /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<Node, Node>& 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<Node, Node> d_cachedResults;
+};
+
+}  // namespace cvc5::internal
+
+#endif /*CVC5__UTIL__ORACLE_CALLER_H*/