diff options
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()) |