diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-14 09:39:13 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-14 09:39:13 -0600 |
commit | dddddbfa12aaeb433074382fb9e2b4c9c92c8a66 (patch) | |
tree | 0ddaa90be32ede1601747771f67469dea67a721e /src | |
parent | 219fb439a1a5ac8f8c53f0d287a259fa82c30ee2 (diff) |
(proof-new) Add bound variable manager (#5655)
This is a common utility for constructing canonical bound variables.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/bound_var_manager.cpp | 57 | ||||
-rw-r--r-- | src/expr/bound_var_manager.h | 103 |
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 */ |