diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-08 15:54:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-08 20:54:22 +0000 |
| commit | 4b0650bfe0c1df81ad3236def912543510932320 (patch) | |
| tree | 16ca312b99881bcf36ccf840ab26079d7bafb35c /src/theory/quantifiers/skolemize.cpp | |
| parent | 73a9f07321a854f8f9123c3645db5b7cddb827be (diff) | |
Improve pre-skolemization, move quantifiers preprocess to own file (#7153)
This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
Diffstat (limited to 'src/theory/quantifiers/skolemize.cpp')
| -rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index fa91b1782..23b66b1de 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -178,13 +178,18 @@ void Skolemize::getSelfSel(const DType& dt, Node Skolemize::mkSkolemizedBody(Node f, Node n, - std::vector<TypeNode>& argTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, std::vector<unsigned>& sub_vars) { NodeManager* nm = NodeManager::currentNM(); + // compute the argument types from the free variables + std::vector<TypeNode> argTypes; + for (TNode v : fvs) + { + argTypes.push_back(v.getType()); + } SkolemManager* sm = nm->getSkolemManager(); Assert(sk.empty() || sk.size() == f[0].getNumChildren()); // calculate the variables and substitution @@ -329,12 +334,11 @@ Node Skolemize::getSkolemizedBody(Node f) std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f); if (it == d_skolem_body.end()) { - std::vector<TypeNode> fvTypes; std::vector<TNode> fvs; Node sub; std::vector<unsigned> sub_vars; - Node ret = mkSkolemizedBody( - f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars); + Node ret = + mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars); d_skolem_body[f] = ret; // store sub quantifier information if (!sub.isNull()) |