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/expr/bound_var_manager.cpp | |
parent | 219fb439a1a5ac8f8c53f0d287a259fa82c30ee2 (diff) |
(proof-new) Add bound variable manager (#5655)
This is a common utility for constructing canonical bound variables.
Diffstat (limited to 'src/expr/bound_var_manager.cpp')
-rw-r--r-- | src/expr/bound_var_manager.cpp | 57 |
1 files changed, 57 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 |