(proof-new) Add bound variable manager (#5655)

This is a common utility for constructing canonical bound variables.

2 files changed, 160 insertions, 0 deletions

diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
new file mode 100644
index 000000000..1532e43de
--- /dev/null
+++ b/src/expr/bound_var_manager.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file bound_var_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bound variable manager
+ **/
+
+#include "expr/bound_var_manager.h"
+
+#include "expr/node_manager_attributes.h"
+
+namespace CVC4 {
+
+// TODO: only enable when proofs are enabled
+BoundVarManager::BoundVarManager() : d_keepCacheVals(true) {}
+
+BoundVarManager::~BoundVarManager() {}
+
+void BoundVarManager::enableKeepCacheValues(bool isEnabled)
+{
+  d_keepCacheVals = isEnabled;
+}
+
+void BoundVarManager::setNameAttr(Node v, const std::string& name)
+{
+  v.setAttribute(expr::VarNameAttr(), name);
+}
+
+Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2)
+{
+  return NodeManager::currentNM()->mkNode(kind::SEXPR, cv1, cv2);
+}
+
+Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i)
+{
+  return NodeManager::currentNM()->mkNode(
+      kind::SEXPR, cv1, cv2, getCacheValue(i));
+}
+
+Node BoundVarManager::getCacheValue(size_t i)
+{
+  return NodeManager::currentNM()->mkConst(Rational(i));
+}
+
+Node BoundVarManager::getCacheValue(TNode cv, size_t i)
+{
+  return getCacheValue(cv, getCacheValue(i));
+}
+
+}  // namespace CVC4
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
new file mode 100644
index 000000000..59ce2bac9
--- /dev/null
+++ b/src/expr/bound_var_manager.h
@@ -0,0 +1,103 @@
+/*********************                                                        */
+/*! \file bound_var_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bound variable manager utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__BOUND_VAR_MANAGER_H
+#define CVC4__EXPR__BOUND_VAR_MANAGER_H
+
+#include <string>
+#include <unordered_set>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * Bound variable manager.
+ *
+ * This class is responsible for constructing BOUND_VARIABLE that are
+ * canonical based on cache keys (Node). It does this using expression
+ * attributes on these nodes.
+ */
+class BoundVarManager
+{
+ public:
+  BoundVarManager();
+  ~BoundVarManager();
+  /**
+   * Enable or disable keeping cache values. If we keep cache values, then
+   * the bound variables returned by the methods below are deterministic in the
+   * lifetime of the NodeManager we are using.
+   */
+  void enableKeepCacheValues(bool isEnabled = true);
+  /**
+   * Make a bound variable of type tn and name tn, cached based on (T, n),
+   * where T is an attribute class of the form:
+   *   expr::Attribute<id, Node>
+   * This variable is unique for (T, n) during the lifetime of n. If
+   * this bound variable manager is configured to keep cache values, then
+   * n is added to the d_cacheVals set and survives in the lifetime of the
+   * current node manager.
+   *
+   * Returns the bound variable.
+   */
+  template <class T>
+  Node mkBoundVar(Node n, TypeNode tn)
+  {
+    T attr;
+    if (n.hasAttribute(attr))
+    {
+      Assert(n.getAttribute(attr).getType() == tn);
+      return n.getAttribute(attr);
+    }
+    Node v = NodeManager::currentNM()->mkBoundVar(tn);
+    n.setAttribute(attr, v);
+    // if we are keeping cache values, insert it to the set
+    if (d_keepCacheVals)
+    {
+      d_cacheVals.insert(n);
+    }
+    return v;
+  }
+  /** Same as above, with a name for the bound variable. */
+  template <class T>
+  Node mkBoundVar(Node n, const std::string& name, TypeNode tn)
+  {
+    Node v = mkBoundVar<T>(n, tn);
+    setNameAttr(n, name);
+    return v;
+  }
+  //---------------------------------- utilities for computing Node hash
+  /** get cache value from two nodes, returns SEXPR */
+  static Node getCacheValue(TNode cv1, TNode cv2);
+  /** get cache value from two nodes and a size_t, returns SEXPR */
+  static Node getCacheValue(TNode cv1, TNode cv2, size_t i);
+  /** get cache value, returns a constant rational node */
+  static Node getCacheValue(size_t i);
+  /** get cache value, return SEXPR of cv and constant rational node */
+  static Node getCacheValue(TNode cv, size_t i);
+  //---------------------------------- end utilities for computing Node hash
+ private:
+  /** Set name of bound variable to name */
+  static void setNameAttr(Node v, const std::string& name);
+  /** Whether we keep cache values */
+  bool d_keepCacheVals;
+  /** The set of cache values we have used */
+  std::unordered_set<Node, NodeHashFunction> d_cacheVals;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */