diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-16 10:52:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-16 10:52:26 -0600 |
commit | 496aed3f37c37519b6a26b3346b7f06e43bb5351 (patch) | |
tree | 709ba9b60db9c3550603a8e923568039cd2365a8 /src/theory/arrays | |
parent | 3a3735d58ddac7ecfac80dad35da963901f15f55 (diff) |
(proof-new) Use bound variable manager (#5679)
This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.
This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/skolem_cache.cpp | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp index 4028a53a8..b32e89bca 100644 --- a/src/theory/arrays/skolem_cache.cpp +++ b/src/theory/arrays/skolem_cache.cpp @@ -15,6 +15,7 @@ #include "theory/arrays/skolem_cache.h" #include "expr/attribute.h" +#include "expr/bound_var_manager.h" #include "expr/skolem_manager.h" #include "expr/type_node.h" @@ -66,20 +67,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq) Node SkolemCache::getExtIndexVar(Node deq) { - ExtIndexVarAttribute eiva; - if (deq.hasAttribute(eiva)) - { - return deq.getAttribute(eiva); - } Node a = deq[0][0]; - Node b = deq[0][1]; TypeNode atn = a.getType(); Assert(atn.isArray()); - Assert(atn == b.getType()); + Assert(atn == deq[0][1].getType()); TypeNode atnIndex = atn.getArrayIndexType(); - Node v = NodeManager::currentNM()->mkBoundVar(atnIndex); - deq.setAttribute(eiva, v); - return v; + BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager(); + return bvm->mkBoundVar<ExtIndexVarAttribute>(deq, atnIndex); } } // namespace arrays |