Add support for oracle constant nodes (#8707)

This is the beginning of a refactoring to make std::function the basis for oracles internally, not binary names.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index f485365377561ff8ad8a9f9dc9cbca7f2ff1817e..a72a4998ae4390483974302f66b7adf76e9adc8f 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -60,6 +60,7 @@ libcvc5_add_sources(
   node_traversal.h
   node_value.cpp
   node_value.h
+  oracle.h
   oracle_caller.cpp
   oracle_caller.h
   sequence.cpp

diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index 25043f146953ff4e101189d635363d632b2101ea..af3d3e18105b8465acca9b683df5e4db5dc352ab 100644 (file)
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -39,6 +39,9 @@ namespace attr {
   struct DatatypeIndexTag
   {
   };
+  struct OracleIndexTag
+  {
+  };
   }  // namespace attr
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
@@ -57,5 +60,9 @@ using TupleDatatypeAttr =
 /** Mapping datatype types to the index of their datatype in node manager */
 using DatatypeIndexAttr = Attribute<attr::DatatypeIndexTag, uint64_t>;
 
+/** Mapping oracle constant nodes to the index of their oracle in the node
+ * manager */
+using OracleIndexAttr = expr::Attribute<expr::attr::OracleIndexTag, uint64_t>;
+
 }  // namespace expr
 }  // namespace cvc5::internal

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 0a7ef904af6dc9a102dd81e9cb96a0116e84d919..419cf50556293cc16300dd0e07298b7d7a295d57 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -26,6 +26,7 @@
 #include "expr/metakind.h"
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
+#include "expr/oracle.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
 #include "expr/type_properties.h"
@@ -248,8 +249,9 @@ NodeManager::~NodeManager()
   d_rt_cache.d_children.clear();
   d_rt_cache.d_data = dummy;
 
-  // clear the datatypes
+  // clear the datatypes and oracles
   d_dtypes.clear();
+  d_oracles.clear();
 
   Assert(!d_attrManager->inGarbageCollection());
 
@@ -950,6 +952,25 @@ TypeNode NodeManager::mkUnresolvedDatatypeSort(const std::string& name,
   return usort;
 }
 
+Node NodeManager::mkOracle(Oracle& o)
+{
+  Node n = NodeBuilder(this, kind::ORACLE);
+  n.setAttribute(TypeAttr(), builtinOperatorType());
+  n.setAttribute(TypeCheckedAttr(), true);
+  n.setAttribute(OracleIndexAttr(), d_oracles.size());
+  // we allocate a new oracle, to take ownership
+  d_oracles.push_back(std::unique_ptr<Oracle>(new Oracle(o.getFunction())));
+  return n;
+}
+
+const Oracle& NodeManager::getOracleFor(const Node& n) const
+{
+  Assert(n.getKind() == kind::ORACLE);
+  size_t index = n.getAttribute(OracleIndexAttr());
+  Assert(index < d_oracles.size());
+  return *d_oracles[index];
+}
+
 Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
 {
   Node n = NodeBuilder(this, kind::VARIABLE);

diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h
index 0ad5005ecf4b606193cdd77431a409cb0056e110..513742383a5ee18fd2e7c05ad138d3cb27681e57 100644 (file)
--- a/src/expr/node_manager_template.h
+++ b/src/expr/node_manager_template.h
@@ -45,6 +45,7 @@ class SkolemManager;
 class BoundVarManager;
 
 class DType;
+class Oracle;
 class Rational;
 
 namespace expr {
@@ -741,6 +742,18 @@ class NodeManager
   /** Make an unresolved datatype sort */
   TypeNode mkUnresolvedDatatypeSort(const std::string& name, size_t arity = 0);
 
+  /**
+   * Make an oracle node. This returns a constant of kind ORACLE that stores
+   * the given method in an Oracle object. This Oracle can later be obtained by
+   * getOracleFor below.
+   */
+  Node mkOracle(Oracle& o);
+
+  /**
+   * Get the oracle for an oracle node n, which should have kind ORACLE.
+   */
+  const Oracle& getOracleFor(const Node& n) const;
+
  private:
   /**
    * Make a set of types representing the given datatypes, which may
@@ -1034,6 +1047,9 @@ class NodeManager
   /** A list of datatypes owned by this node manager */
   std::vector<std::unique_ptr<DType>> d_dtypes;
 
+  /** A list of oracles owned by this node manager */
+  std::vector<std::unique_ptr<Oracle>> d_oracles;
+
   TupleTypeCache d_tt_cache;
   RecTypeCache d_rt_cache;
 }; /* class NodeManager */

diff --git a/src/expr/oracle.h b/src/expr/oracle.h
new file mode 100644 (file)
index 0000000..90fe2ff
--- /dev/null
+++ b/src/expr/oracle.h
@@ -0,0 +1,59 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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_H
+#define CVC5__EXPR__ORACLE_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace cvc5::internal {
+
+/**
+ * An oracle, which stores a function whose interface is from a vector of nodes
+ * to a vector of nodes. It is expected to serve as an oracle interface as
+ * described in Polgreen et al VMCAI 2022 and the SyGuS version 2.1 standard.
+ */
+class Oracle
+{
+ public:
+  /** Construct an oracle whose implementation is the given function. */
+  Oracle(std::function<std::vector<Node>(const std::vector<Node>&)> fn)
+      : d_fn(fn)
+  {
+  }
+  ~Oracle() {}
+  /** Run the function on the given input */
+  std::vector<Node> run(const std::vector<Node>& input) const
+  {
+    return d_fn(input);
+  }
+  /** Get the function for this oracle */
+  std::function<std::vector<Node>(const std::vector<Node>&)> getFunction() const
+  {
+    return d_fn;
+  }
+
+ private:
+  /** The function for this oracle */
+  std::function<std::vector<Node>(const std::vector<Node>&)> d_fn;
+};
+
+}  // namespace cvc5::internal
+
+#endif /*CVC5__EXPR__ORACLE_H*/

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 481499f2e340290c0775c99b980e440b179198b7..7c1b9fe0fab043a3177e1912389d0d0b69594a22 100644 (file)
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -17,6 +17,8 @@ operator EXISTS 2:3 "existentially quantified formula; first parameter is an BOU
 
 variable INST_CONSTANT "instantiation constant"
 
+variable ORACLE "oracle"
+
 sort BOUND_VAR_LIST_TYPE \
     Cardinality::INTEGERS \
     not-well-founded \