From 084ccdd6f05781decad5f9faee60249216183ce5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 1 Jul 2019 15:23:15 -0500 Subject: [PATCH] Add higher-order elimination preprocessing pass (#2865) --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 18 + src/preprocessing/passes/ho_elim.cpp | 543 +++++++++++++++++++++++++++ src/preprocessing/passes/ho_elim.h | 151 ++++++++ 4 files changed, 714 insertions(+) create mode 100644 src/preprocessing/passes/ho_elim.cpp create mode 100644 src/preprocessing/passes/ho_elim.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 011ba6ab5..f79c82d49 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -60,6 +60,8 @@ libcvc4_add_sources( preprocessing/passes/extended_rewriter_pass.h preprocessing/passes/global_negate.cpp preprocessing/passes/global_negate.h + preprocessing/passes/ho_elim.cpp + preprocessing/passes/ho_elim.h preprocessing/passes/int_to_bv.cpp preprocessing/passes/int_to_bv.h preprocessing/passes/ite_removal.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 0a69178b3..03ffade46 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1784,6 +1784,24 @@ header = "options/quantifiers_options.h" read_only = true help = "merge term indices modulo equality" +[[option]] + name = "hoElim" + category = "regular" + long = "ho-elim" + type = "bool" + default = "false" + read_only = true + help = "eagerly eliminate higher-order constraints" + +[[option]] + name = "hoElimStoreAx" + category = "regular" + long = "ho-elim-store-ax" + type = "bool" + default = "true" + read_only = false + help = "use store axiom during ho-elim" + ### Proof options [[option]] diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp new file mode 100644 index 000000000..65945f0d7 --- /dev/null +++ b/src/preprocessing/passes/ho_elim.cpp @@ -0,0 +1,543 @@ +/********************* */ +/*! \file ho_elim.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The HoElim preprocessing pass + ** + ** Eliminates higher-order constraints. + **/ + +#include "preprocessing/passes/ho_elim.h" + +#include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" +#include "theory/rewriter.h" +#include "theory/uf/theory_uf_rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +HoElim::HoElim(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ho-elim"){}; + +Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + + if (it == d_visited.end()) + { + if (cur.getKind() == LAMBDA) + { + Trace("ho-elim-ll") << "Lambda lift: " << cur << std::endl; + // must also get free variables in lambda + std::vector lvars; + std::vector ftypes; + std::unordered_set fvs; + expr::getFreeVariables(cur, fvs); + std::vector nvars; + std::vector vars; + Node sbd = cur[1]; + if (!fvs.empty()) + { + Trace("ho-elim-ll") + << "Has " << fvs.size() << " free variables" << std::endl; + for (const Node& v : fvs) + { + TypeNode vt = v.getType(); + ftypes.push_back(vt); + Node vs = nm->mkBoundVar(vt); + vars.push_back(v); + nvars.push_back(vs); + lvars.push_back(vs); + } + sbd = sbd.substitute( + vars.begin(), vars.end(), nvars.begin(), nvars.end()); + } + for (const Node& bv : cur[0]) + { + TypeNode bvt = bv.getType(); + ftypes.push_back(bvt); + lvars.push_back(bv); + } + Node nlambda = cur; + if (!fvs.empty()) + { + nlambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lvars), sbd); + Trace("ho-elim-ll") + << "...new lambda definition: " << nlambda << std::endl; + } + TypeNode rangeType = cur.getType().getRangeType(); + TypeNode nft = nm->mkFunctionType(ftypes, rangeType); + Node nf = nm->mkSkolem("ll", nft); + Trace("ho-elim-ll") + << "...introduce: " << nf << " of type " << nft << std::endl; + newLambda[nf] = nlambda; + Assert(nf.getType() == nlambda.getType()); + if (!vars.empty()) + { + for (const Node& v : vars) + { + nf = nm->mkNode(HO_APPLY, nf, v); + } + Trace("ho-elim-ll") << "...partial application: " << nf << std::endl; + } + d_visited[cur] = nf; + Trace("ho-elim-ll") << "...return types : " << nf.getType() << " " + << cur.getType() << std::endl; + Assert(nf.getType() == cur.getType()); + } + else + { + d_visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = d_visited.find(cn); + Assert(it != d_visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + d_visited[cur] = ret; + } + } while (!visit.empty()); + Assert(d_visited.find(n) != d_visited.end()); + Assert(!d_visited.find(n)->second.isNull()); + return d_visited[n]; +} + +Node HoElim::eliminateHo(Node n) +{ + Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator it; + std::map preReplace; + std::map::iterator itr; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + Trace("ho-elim-visit") << "Process: " << cur << std::endl; + + if (it == d_visited.end()) + { + TypeNode tn = cur.getType(); + // lambdas are already eliminated by now + Assert(cur.getKind() != LAMBDA); + if (tn.isFunction()) + { + d_funTypes.insert(tn); + } + if (cur.isVar()) + { + Node ret = cur; + if (options::hoElim()) + { + if (tn.isFunction()) + { + TypeNode ut = getUSort(tn); + if (cur.getKind() == BOUND_VARIABLE) + { + ret = nm->mkBoundVar(ut); + } + else + { + ret = nm->mkSkolem("k", ut); + } + // must get the ho apply to ensure extensionality is applied + Node hoa = getHoApplyUf(tn); + Trace("ho-elim-visit") << "Hoa is " << hoa << std::endl; + } + } + d_visited[cur] = ret; + } + else + { + d_visited[cur] = Node::null(); + if (cur.getKind() == APPLY_UF && options::hoElim()) + { + Node op = cur.getOperator(); + // convert apply uf with variable arguments eagerly to ho apply + // chains, so they are processed uniformly. + visit.push_back(cur); + Node newCur = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(cur); + preReplace[cur] = newCur; + cur = newCur; + d_visited[cur] = Node::null(); + } + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + itr = preReplace.find(cur); + if (itr != preReplace.end()) + { + Trace("ho-elim-visit") + << "return (pre-repl): " << d_visited[itr->second] << std::endl; + d_visited[cur] = d_visited[itr->second]; + } + else + { + bool childChanged = false; + std::vector children; + std::vector childrent; + bool typeChanged = false; + for (const Node& cn : ret) + { + it = d_visited.find(cn); + Assert(it != d_visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + TypeNode ct = it->second.getType(); + childrent.push_back(ct); + typeChanged = typeChanged || ct != cn.getType(); + } + if (ret.getMetaKind() == metakind::PARAMETERIZED) + { + // child of an argument changed type, must change type + Node op = ret.getOperator(); + Node retOp = op; + Trace("ho-elim-visit") + << "Process op " << op << ", typeChanged = " << typeChanged + << std::endl; + if (typeChanged) + { + std::unordered_map::iterator ito = + d_visited_op.find(op); + if (ito == d_visited_op.end()) + { + Assert(!childrent.empty()); + TypeNode newFType = nm->mkFunctionType(childrent, cur.getType()); + retOp = nm->mkSkolem("rf", newFType); + d_visited_op[op] = retOp; + } + else + { + retOp = ito->second; + } + } + children.insert(children.begin(), retOp); + } + // process ho apply + if (ret.getKind() == HO_APPLY && options::hoElim()) + { + TypeNode tnr = ret.getType(); + tnr = getUSort(tnr); + Node hoa = + getHoApplyUf(children[0].getType(), children[1].getType(), tnr); + std::vector hchildren; + hchildren.push_back(hoa); + hchildren.push_back(children[0]); + hchildren.push_back(children[1]); + ret = nm->mkNode(APPLY_UF, hchildren); + } + else if (childChanged) + { + ret = nm->mkNode(ret.getKind(), children); + } + Trace("ho-elim-visit") << "return (pre-repl): " << ret << std::endl; + d_visited[cur] = ret; + } + } + } while (!visit.empty()); + Assert(d_visited.find(n) != d_visited.end()); + Assert(!d_visited.find(n)->second.isNull()); + Trace("ho-elim-assert") << "...got : " << d_visited[n] << std::endl; + return d_visited[n]; +} + +PreprocessingPassResult HoElim::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + // step [1]: apply lambda lifting to eliminate all lambdas + NodeManager* nm = NodeManager::currentNM(); + std::vector axioms; + std::map newLambda; + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + Node res = eliminateLambdaComplete(prev, newLambda); + if (res != prev) + { + res = theory::Rewriter::rewrite(res); + Assert(!expr::hasFreeVar(res)); + assertionsToPreprocess->replace(i, res); + } + } + // do lambda lifting on new lambda definitions + // this will do fixed point to eliminate lambdas within lambda lifting axioms. + while (!newLambda.empty()) + { + std::map lproc = newLambda; + newLambda.clear(); + for (const std::pair& l : lproc) + { + Node lambda = l.second; + std::vector vars; + std::vector nvars; + for (const Node& v : lambda[0]) + { + Node bv = nm->mkBoundVar(v.getType()); + vars.push_back(v); + nvars.push_back(bv); + } + + Node bd = lambda[1].substitute( + vars.begin(), vars.end(), nvars.begin(), nvars.end()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars); + + nvars.insert(nvars.begin(), l.first); + Node curr = nm->mkNode(APPLY_UF, nvars); + + Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd)); + Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax + << " for " << lambda << std::endl; + Assert(!expr::hasFreeVar(llfax)); + Node llfaxe = eliminateLambdaComplete(llfax, newLambda); + Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for " + << lambda << std::endl; + axioms.push_back(llfaxe); + } + } + + d_visited.clear(); + // add lambda lifting axioms as a conjunction to the first assertion + if (!axioms.empty()) + { + Node orig = (*assertionsToPreprocess)[0]; + axioms.push_back(orig); + Node conj = nm->mkNode(AND, axioms); + conj = theory::Rewriter::rewrite(conj); + Assert(!expr::hasFreeVar(conj)); + assertionsToPreprocess->replace(0, conj); + } + axioms.clear(); + + // step [2]: eliminate all higher-order constraints + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + Node res = eliminateHo(prev); + if (res != prev) + { + res = theory::Rewriter::rewrite(res); + Assert(!expr::hasFreeVar(res)); + assertionsToPreprocess->replace(i, res); + } + } + // extensionality: process all function types + for (const TypeNode& ftn : d_funTypes) + { + if (options::hoElim()) + { + Node h = getHoApplyUf(ftn); + Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl; + TypeNode ft = h.getType(); + TypeNode uf = getUSort(ft[0]); + TypeNode ut = getUSort(ft[1]); + // extensionality + Node x = nm->mkBoundVar("x", uf); + Node y = nm->mkBoundVar("y", uf); + Node z = nm->mkBoundVar("z", ut); + Node eq = + nm->mkNode(APPLY_UF, h, x, z).eqNode(nm->mkNode(APPLY_UF, h, y, z)); + Node antec = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, z), eq); + Node conc = x.eqNode(y); + Node ax = nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, x, y), + nm->mkNode(OR, antec.negate(), conc)); + axioms.push_back(ax); + Trace("ho-elim-ax") << "...ext axiom : " << ax << std::endl; + // Make the "store" axiom, which asserts for every function, there + // exists another function that acts like the "store" operator for + // arrays, e.g. it is the same function with one I/O pair updated. + // Without this axiom, the translation is model unsound. + if (options::hoElimStoreAx()) + { + Node u = nm->mkBoundVar("u", uf); + Node v = nm->mkBoundVar("v", uf); + Node i = nm->mkBoundVar("i", ut); + Node ii = nm->mkBoundVar("ii", ut); + Node huii = nm->mkNode(APPLY_UF, h, u, ii); + Node e = nm->mkBoundVar("e", huii.getType()); + Node store = nm->mkNode( + FORALL, + nm->mkNode(BOUND_VAR_LIST, u, e, i), + nm->mkNode(EXISTS, + nm->mkNode(BOUND_VAR_LIST, v), + nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, ii), + nm->mkNode(APPLY_UF, h, v, ii) + .eqNode(nm->mkNode( + ITE, ii.eqNode(i), e, huii))))); + axioms.push_back(store); + Trace("ho-elim-ax") << "...store axiom : " << store << std::endl; + } + } + else if (options::hoElimStoreAx()) + { + Node u = nm->mkBoundVar("u", ftn); + Node v = nm->mkBoundVar("v", ftn); + std::vector argTypes = ftn.getArgTypes(); + Node i = nm->mkBoundVar("i", argTypes[0]); + Node ii = nm->mkBoundVar("ii", argTypes[0]); + Node huii = nm->mkNode(HO_APPLY, u, ii); + Node e = nm->mkBoundVar("e", huii.getType()); + Node store = nm->mkNode( + FORALL, + nm->mkNode(BOUND_VAR_LIST, u, e, i), + nm->mkNode( + EXISTS, + nm->mkNode(BOUND_VAR_LIST, v), + nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, ii), + nm->mkNode(HO_APPLY, v, ii) + .eqNode(nm->mkNode(ITE, ii.eqNode(i), e, huii))))); + axioms.push_back(store); + Trace("ho-elim-ax") << "...store (ho_apply) axiom : " << store + << std::endl; + } + } + // add new axioms as a conjunction to the first assertion + if (!axioms.empty()) + { + Node orig = (*assertionsToPreprocess)[0]; + axioms.push_back(orig); + Node conj = nm->mkNode(AND, axioms); + conj = theory::Rewriter::rewrite(conj); + Assert(!expr::hasFreeVar(conj)); + assertionsToPreprocess->replace(0, conj); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +Node HoElim::getHoApplyUf(TypeNode tn) +{ + TypeNode tnu = getUSort(tn); + TypeNode rangeType = tn.getRangeType(); + std::vector argTypes = tn.getArgTypes(); + TypeNode tna = getUSort(argTypes[0]); + + TypeNode tr = rangeType; + if (argTypes.size() > 1) + { + std::vector remArgTypes; + remArgTypes.insert(remArgTypes.end(), argTypes.begin() + 1, argTypes.end()); + tr = NodeManager::currentNM()->mkFunctionType(remArgTypes, tr); + } + TypeNode tnr = getUSort(tr); + + return getHoApplyUf(tnu, tna, tnr); +} + +Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr) +{ + std::map::iterator it = d_hoApplyUf.find(tnf); + if (it == d_hoApplyUf.end()) + { + NodeManager* nm = NodeManager::currentNM(); + + std::vector hoTypeArgs; + hoTypeArgs.push_back(tnf); + hoTypeArgs.push_back(tna); + TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr); + Node k = NodeManager::currentNM()->mkSkolem("ho", tnh); + d_hoApplyUf[tnf] = k; + return k; + } + return it->second; +} + +TypeNode HoElim::getUSort(TypeNode tn) +{ + if (!tn.isFunction()) + { + return tn; + } + std::map::iterator it = d_ftypeMap.find(tn); + if (it == d_ftypeMap.end()) + { + // flatten function arguments + std::vector argTypes = tn.getArgTypes(); + TypeNode rangeType = tn.getRangeType(); + bool typeChanged = false; + for (unsigned i = 0; i < argTypes.size(); i++) + { + if (argTypes[i].isFunction()) + { + argTypes[i] = getUSort(argTypes[i]); + typeChanged = true; + } + } + TypeNode s; + if (typeChanged) + { + TypeNode ntn = + NodeManager::currentNM()->mkFunctionType(argTypes, rangeType); + s = getUSort(ntn); + } + else + { + std::stringstream ss; + ss << "u_" << tn; + s = NodeManager::currentNM()->mkSort(ss.str()); + } + d_ftypeMap[tn] = s; + return s; + } + return it->second; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h new file mode 100644 index 000000000..f0de321c4 --- /dev/null +++ b/src/preprocessing/passes/ho_elim.h @@ -0,0 +1,151 @@ +/********************* */ +/*! \file ho_elim.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The HoElim preprocessing pass + ** + ** Eliminates higher-order constraints. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H +#define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** Higher-order elimination. + * + * This preprocessing pass eliminates all occurrences of higher-order + * constraints in the input, and replaces the entire input problem with + * an equisatisfiable one. This is based on the following steps. + * + * [1] Eliminate all occurrences of lambdas via lambda lifting. This includes + * lambdas with free variables that occur in quantifier bodies (see + * documentation for eliminateLambdaComplete). + * + * [2] Eliminate all occurrences of partial applications and constraints + * involving functions as first-class members. This is done by first + * turning all function applications into an applicative encoding involving the + * parametric binary operator @ (of kind HO_APPLY). Then we introduce: + * - An uninterpreted sort U(T) for each function type T, + * - A function H(f) of sort U(T1) x .. x U(Tn) -> U(T) for each function f + * of sort T1 x ... x Tn -> T. + * - A function App_{T1 x T2 ... x Tn -> T} of type + * U(T1 x T2 ... x Tn -> T) x U(T1) -> U(T2 ... x Tn -> T) + * for each occurrence of @ applied to arguments of types T1 x T2 ... x Tn -> T + * and T1. + * + * [3] Add additional axioms to ensure the correct interpretation of + * the sorts U(...), and functions App_{...}. This includes: + * + * - The "extensionality" axiom for App_{...} terms, stating that functions + * that behave the same according to App for all inputs must be equal: + * forall x : U(T1->T2), y : U(T1->T2). + * ( forall z : T1. App_{T1->T2}( x, z ) = App_{T1->T2}( y, z ) ) => + * x = y + * + * - The "store" axiom, which effectively states that for all (encoded) + * functions f, there exists a function g that behaves identically to f, except + * that g for argument i is e: + * forall x : U(T1->T2), i : U(T1), e : U(T2). + * exists g : U(T1->T2). + * forall z: T1. + * App_{T1->T2}( g, z ) = ite( z = i, e, App_{T1->T2}( f, z ) ). + * + * + * Based on options, this preprocessing pass may apply a subset o the above + * steps. In particular: + * * If options::hoElim() is true, then step [2] is taken and extensionality + * axioms are added in step [3]. + * * If options::hoElimStoreAx() is true, then store axioms are added in step 3. + * The form of these axioms depends on whether options::hoElim() is true. If it + * is true, the axiom is given in terms of the uninterpreted functions that + * encode function sorts. If it is false, then the store axiom is given in terms + * of the original function sorts. + */ +class HoElim : public PreprocessingPass +{ + public: + HoElim(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + /** + * Eliminate all occurrences of lambdas in term n, return the result. This + * is step [1] mentioned at the header of this class. + * + * The map newLambda maps newly introduced function skolems with their + * (lambda) definition, which is a closed term. + * + * Notice that to ensure that all lambda definitions are closed, we + * introduce extra bound arguments to the lambda, for example: + * forall x. (lambda y. x+y) != f + * becomes + * forall x. g(x) != f + * where g is mapped to the (closed) term ( lambda xy. x+y ). + * + * Notice that the definitions in newLambda may themselves contain lambdas, + * hence, this method is run until a fix point is reached. + */ + Node eliminateLambdaComplete(Node n, std::map& newLambda); + + /** + * Eliminate all higher-order constraints in n, return the result. This is + * step [2] mentioned at the header of this class. + */ + Node eliminateHo(Node n); + /** + * Stores the set of nodes we have current visited and their results + * in steps [1] and [2] of this pass. + */ + std::unordered_map d_visited; + /** + * Stores the mapping from functions f to their corresponding function H(f) + * in the encoding for step [2] of this pass. + */ + std::unordered_map d_visited_op; + /** The set of all function types encountered in assertions. */ + std::unordered_set d_funTypes; + + /** + * Get ho apply uf, this returns App_{@_{T1 x T2 ... x Tn -> T}} + */ + Node getHoApplyUf(TypeNode tn); + /** + * Get ho apply uf, where: + * tn is T1 x T2 ... x Tn -> T, + * tna is T1, + * tnr is T2 ... x Tn -> T + * This returns App_{@_{T1 x T2 ... x Tn -> T}}. + */ + Node getHoApplyUf(TypeNode tn, TypeNode tna, TypeNode tnr); + /** cache of getHoApplyUf */ + std::map d_hoApplyUf; + /** + * Get uninterpreted sort for function sort. This returns U(T) for function + * type T for step [2] of this pass. + */ + TypeNode getUSort(TypeNode tn); + /** cache of the above function */ + std::map d_ftypeMap; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */ -- 2.30.2