Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/ho_elim.cpp	Lines:	323	330	97.9 %
Date:	2021-09-10	Branches:	700	1518	46.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * The HoElim preprocessing pass.
 *
 * Eliminates higher-order constraints.
 */

#include "preprocessing/passes/ho_elim.h"

#include <sstream>

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
#include "theory/uf/theory_uf_rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace preprocessing {
namespace passes {

HoElim::HoElim(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "ho-elim"){};

Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  std::unordered_map<Node, Node>::iterator it;
  std::vector<Node> 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<Node> lvars;
        std::vector<TypeNode> ftypes;
        std::unordered_set<Node> fvs;
        expr::getFreeVariables(cur, fvs);
        std::vector<Node> nvars;
        std::vector<Node> 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 = sm->mkDummySkolem("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<Node> 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();
  SkolemManager* sm = nm->getSkolemManager();
  std::unordered_map<Node, Node>::iterator it;
  std::map<Node, Node> preReplace;
  std::map<Node, Node>::iterator itr;
  std::vector<TNode> 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().quantifiers.hoElim)
        {
          if (tn.isFunction())
          {
            TypeNode ut = getUSort(tn);
            if (cur.getKind() == BOUND_VARIABLE)
            {
              ret = nm->mkBoundVar(ut);
            }
            else
            {
              ret = sm->mkDummySkolem("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().quantifiers.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<Node> children;
        std::vector<TypeNode> 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<TNode, Node>::iterator ito =
                d_visited_op.find(op);
            if (ito == d_visited_op.end())
            {
              Assert(!childrent.empty());
              TypeNode newFType = nm->mkFunctionType(childrent, cur.getType());
              retOp = sm->mkDummySkolem("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().quantifiers.hoElim)
        {
          TypeNode tnr = ret.getType();
          tnr = getUSort(tnr);
          Node hoa =
              getHoApplyUf(children[0].getType(), children[1].getType(), tnr);
          std::vector<Node> 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<Node> axioms;
  std::map<Node, Node> newLambda;
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    Node prev = (*assertionsToPreprocess)[i];
    Node res = eliminateLambdaComplete(prev, newLambda);
    if (res != prev)
    {
      res = 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<Node, Node> lproc = newLambda;
    newLambda.clear();
    for (const std::pair<const Node, Node>& l : lproc)
    {
      Node lambda = l.second;
      std::vector<Node> vars;
      std::vector<Node> 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 conj = nm->mkAnd(axioms);
    conj = rewrite(conj);
    Assert(!expr::hasFreeVar(conj));
    assertionsToPreprocess->conjoin(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 = rewrite(res);
      Assert(!expr::hasFreeVar(res));
      assertionsToPreprocess->replace(i, res);
    }
  }
  // extensionality: process all function types
  for (const TypeNode& ftn : d_funTypes)
  {
    if (options().quantifiers.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().quantifiers.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().quantifiers.hoElimStoreAx)
    {
      Node u = nm->mkBoundVar("u", ftn);
      Node v = nm->mkBoundVar("v", ftn);
      std::vector<TypeNode> 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 conj = nm->mkAnd(axioms);
    conj = rewrite(conj);
    Assert(!expr::hasFreeVar(conj));
    assertionsToPreprocess->conjoin(0, conj);
  }

  return PreprocessingPassResult::NO_CONFLICT;
}

Node HoElim::getHoApplyUf(TypeNode tn)
{
  TypeNode tnu = getUSort(tn);
  TypeNode rangeType = tn.getRangeType();
  std::vector<TypeNode> argTypes = tn.getArgTypes();
  TypeNode tna = getUSort(argTypes[0]);

  TypeNode tr = rangeType;
  if (argTypes.size() > 1)
  {
    std::vector<TypeNode> 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<TypeNode, Node>::iterator it = d_hoApplyUf.find(tnf);
  if (it == d_hoApplyUf.end())
  {
    NodeManager* nm = NodeManager::currentNM();
    SkolemManager* sm = nm->getSkolemManager();

    std::vector<TypeNode> hoTypeArgs;
    hoTypeArgs.push_back(tnf);
    hoTypeArgs.push_back(tna);
    TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
    Node k = sm->mkDummySkolem("ho", tnh);
    d_hoApplyUf[tnf] = k;
    return k;
  }
  return it->second;
}

TypeNode HoElim::getUSort(TypeNode tn)
{
  if (!tn.isFunction())
  {
    return tn;
  }
  std::map<TypeNode, TypeNode>::iterator it = d_ftypeMap.find(tn);
  if (it == d_ftypeMap.end())
  {
    // flatten function arguments
    std::vector<TypeNode> 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 cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The HoElim preprocessing pass.
14		*
15		* Eliminates higher-order constraints.
16		*/
17
18		#include "preprocessing/passes/ho_elim.h"
19
20		#include <sstream>
21
22		#include "expr/node_algorithm.h"
23		#include "expr/skolem_manager.h"
24		#include "options/quantifiers_options.h"
25		#include "preprocessing/assertion_pipeline.h"
26		#include "theory/rewriter.h"
27		#include "theory/uf/theory_uf_rewriter.h"
28
29		using namespace cvc5::kind;
30
31		namespace cvc5 {
32		namespace preprocessing {
33		namespace passes {
34
35	9913	HoElim::HoElim(PreprocessingPassContext* preprocContext)
36	9913	: PreprocessingPass(preprocContext, "ho-elim"){};
37
38	4555	Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
39		{
40	4555	NodeManager* nm = NodeManager::currentNM();
41	4555	SkolemManager* sm = nm->getSkolemManager();
42	4555	std::unordered_map<Node, Node>::iterator it;
43	9110	std::vector<Node> visit;
44	9110	TNode cur;
45	4555	visit.push_back(n);
46	109457	do
47		{
48	114012	cur = visit.back();
49	114012	visit.pop_back();
50	114012	it = d_visited.find(cur);
51
52	114012	if (it == d_visited.end())
53		{
54	44719	if (cur.getKind() == LAMBDA)
55		{
56	170	Trace("ho-elim-ll") << "Lambda lift: " << cur << std::endl;
57		// must also get free variables in lambda
58	340	std::vector<Node> lvars;
59	340	std::vector<TypeNode> ftypes;
60	340	std::unordered_set<Node> fvs;
61	170	expr::getFreeVariables(cur, fvs);
62	340	std::vector<Node> nvars;
63	340	std::vector<Node> vars;
64	340	Node sbd = cur[1];
65	170	if (!fvs.empty())
66		{
67	252	Trace("ho-elim-ll")
68	126	<< "Has " << fvs.size() << " free variables" << std::endl;
69	351	for (const Node& v : fvs)
70		{
71	450	TypeNode vt = v.getType();
72	225	ftypes.push_back(vt);
73	450	Node vs = nm->mkBoundVar(vt);
74	225	vars.push_back(v);
75	225	nvars.push_back(vs);
76	225	lvars.push_back(vs);
77		}
78	126	sbd = sbd.substitute(
79		vars.begin(), vars.end(), nvars.begin(), nvars.end());
80		}
81	371	for (const Node& bv : cur[0])
82		{
83	402	TypeNode bvt = bv.getType();
84	201	ftypes.push_back(bvt);
85	201	lvars.push_back(bv);
86		}
87	340	Node nlambda = cur;
88	170	if (!fvs.empty())
89		{
90	126	nlambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lvars), sbd);
91	252	Trace("ho-elim-ll")
92	126	<< "...new lambda definition: " << nlambda << std::endl;
93		}
94	340	TypeNode rangeType = cur.getType().getRangeType();
95	340	TypeNode nft = nm->mkFunctionType(ftypes, rangeType);
96	340	Node nf = sm->mkDummySkolem("ll", nft);
97	340	Trace("ho-elim-ll")
98	170	<< "...introduce: " << nf << " of type " << nft << std::endl;
99	170	newLambda[nf] = nlambda;
100	170	Assert(nf.getType() == nlambda.getType());
101	170	if (!vars.empty())
102		{
103	351	for (const Node& v : vars)
104		{
105	225	nf = nm->mkNode(HO_APPLY, nf, v);
106		}
107	126	Trace("ho-elim-ll") << "...partial application: " << nf << std::endl;
108		}
109	170	d_visited[cur] = nf;
110	340	Trace("ho-elim-ll") << "...return types : " << nf.getType() << " "
111	170	<< cur.getType() << std::endl;
112	170	Assert(nf.getType() == cur.getType());
113		}
114		else
115		{
116	44549	d_visited[cur] = Node::null();
117	44549	visit.push_back(cur);
118	109457	for (const Node& cn : cur)
119		{
120	64908	visit.push_back(cn);
121		}
122		}
123		}
124	69293	else if (it->second.isNull())
125		{
126	89098	Node ret = cur;
127	44549	bool childChanged = false;
128	89098	std::vector<Node> children;
129	44549	if (cur.getMetaKind() == metakind::PARAMETERIZED)
130		{
131	8248	children.push_back(cur.getOperator());
132		}
133	109457	for (const Node& cn : cur)
134		{
135	64908	it = d_visited.find(cn);
136	64908	Assert(it != d_visited.end());
137	64908	Assert(!it->second.isNull());
138	64908	childChanged = childChanged \|\| cn != it->second;
139	64908	children.push_back(it->second);
140		}
141	44549	if (childChanged)
142		{
143	1463	ret = nm->mkNode(cur.getKind(), children);
144		}
145	44549	d_visited[cur] = ret;
146		}
147	114012	} while (!visit.empty());
148	4555	Assert(d_visited.find(n) != d_visited.end());
149	4555	Assert(!d_visited.find(n)->second.isNull());
150	9110	return d_visited[n];
151		}
152
153	4385	Node HoElim::eliminateHo(Node n)
154		{
155	4385	Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
156	4385	NodeManager* nm = NodeManager::currentNM();
157	4385	SkolemManager* sm = nm->getSkolemManager();
158	4385	std::unordered_map<Node, Node>::iterator it;
159	8770	std::map<Node, Node> preReplace;
160	4385	std::map<Node, Node>::iterator itr;
161	8770	std::vector<TNode> visit;
162	8770	TNode cur;
163	4385	visit.push_back(n);
164	104200	do
165		{
166	108585	cur = visit.back();
167	108585	visit.pop_back();
168	108585	it = d_visited.find(cur);
169	108585	Trace("ho-elim-visit") << "Process: " << cur << std::endl;
170
171	108585	if (it == d_visited.end())
172		{
173	91976	TypeNode tn = cur.getType();
174		// lambdas are already eliminated by now
175	45988	Assert(cur.getKind() != LAMBDA);
176	45988	if (tn.isFunction())
177		{
178	7896	d_funTypes.insert(tn);
179		}
180	45988	if (cur.isVar())
181		{
182	19990	Node ret = cur;
183	9995	if (options().quantifiers.hoElim)
184		{
185	3526	if (tn.isFunction())
186		{
187	4156	TypeNode ut = getUSort(tn);
188	2078	if (cur.getKind() == BOUND_VARIABLE)
189		{
190	1713	ret = nm->mkBoundVar(ut);
191		}
192		else
193		{
194	365	ret = sm->mkDummySkolem("k", ut);
195		}
196		// must get the ho apply to ensure extensionality is applied
197	4156	Node hoa = getHoApplyUf(tn);
198	2078	Trace("ho-elim-visit") << "Hoa is " << hoa << std::endl;
199		}
200		}
201	9995	d_visited[cur] = ret;
202		}
203		else
204		{
205	35993	d_visited[cur] = Node::null();
206	35993	if (cur.getKind() == APPLY_UF && options().quantifiers.hoElim)
207		{
208	1912	Node op = cur.getOperator();
209		// convert apply uf with variable arguments eagerly to ho apply
210		// chains, so they are processed uniformly.
211	956	visit.push_back(cur);
212	1912	Node newCur = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(cur);
213	956	preReplace[cur] = newCur;
214	956	cur = newCur;
215	956	d_visited[cur] = Node::null();
216		}
217	35993	visit.push_back(cur);
218	103244	for (const Node& cn : cur)
219		{
220	67251	visit.push_back(cn);
221		}
222		}
223		}
224	62597	else if (it->second.isNull())
225		{
226	73898	Node ret = cur;
227	36949	itr = preReplace.find(cur);
228	36949	if (itr != preReplace.end())
229		{
230	1912	Trace("ho-elim-visit")
231	956	<< "return (pre-repl): " << d_visited[itr->second] << std::endl;
232	956	d_visited[cur] = d_visited[itr->second];
233		}
234		else
235		{
236	35993	bool childChanged = false;
237	71986	std::vector<Node> children;
238	71986	std::vector<TypeNode> childrent;
239	35993	bool typeChanged = false;
240	103244	for (const Node& cn : ret)
241		{
242	67251	it = d_visited.find(cn);
243	67251	Assert(it != d_visited.end());
244	67251	Assert(!it->second.isNull());
245	67251	childChanged = childChanged \|\| cn != it->second;
246	67251	children.push_back(it->second);
247	134502	TypeNode ct = it->second.getType();
248	67251	childrent.push_back(ct);
249	67251	typeChanged = typeChanged \|\| ct != cn.getType();
250		}
251	35993	if (ret.getMetaKind() == metakind::PARAMETERIZED)
252		{
253		// child of an argument changed type, must change type
254	14584	Node op = ret.getOperator();
255	14584	Node retOp = op;
256	14584	Trace("ho-elim-visit")
257	7292	<< "Process op " << op << ", typeChanged = " << typeChanged
258	7292	<< std::endl;
259	7292	if (typeChanged)
260		{
261		std::unordered_map<TNode, Node>::iterator ito =
262		d_visited_op.find(op);
263		if (ito == d_visited_op.end())
264		{
265		Assert(!childrent.empty());
266		TypeNode newFType = nm->mkFunctionType(childrent, cur.getType());
267		retOp = sm->mkDummySkolem("rf", newFType);
268		d_visited_op[op] = retOp;
269		}
270		else
271		{
272		retOp = ito->second;
273		}
274		}
275	7292	children.insert(children.begin(), retOp);
276		}
277		// process ho apply
278	35993	if (ret.getKind() == HO_APPLY && options().quantifiers.hoElim)
279		{
280	15592	TypeNode tnr = ret.getType();
281	7796	tnr = getUSort(tnr);
282		Node hoa =
283	15592	getHoApplyUf(children[0].getType(), children[1].getType(), tnr);
284	15592	std::vector<Node> hchildren;
285	7796	hchildren.push_back(hoa);
286	7796	hchildren.push_back(children[0]);
287	7796	hchildren.push_back(children[1]);
288	7796	ret = nm->mkNode(APPLY_UF, hchildren);
289		}
290	28197	else if (childChanged)
291		{
292	5229	ret = nm->mkNode(ret.getKind(), children);
293		}
294	35993	Trace("ho-elim-visit") << "return (pre-repl): " << ret << std::endl;
295	35993	d_visited[cur] = ret;
296		}
297		}
298	108585	} while (!visit.empty());
299	4385	Assert(d_visited.find(n) != d_visited.end());
300	4385	Assert(!d_visited.find(n)->second.isNull());
301	4385	Trace("ho-elim-assert") << "...got : " << d_visited[n] << std::endl;
302	8770	return d_visited[n];
303		}
304
305	187	PreprocessingPassResult HoElim::applyInternal(
306		AssertionPipeline* assertionsToPreprocess)
307		{
308		// step [1]: apply lambda lifting to eliminate all lambdas
309	187	NodeManager* nm = NodeManager::currentNM();
310	374	std::vector<Node> axioms;
311	374	std::map<Node, Node> newLambda;
312	4572	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
313		{
314	8770	Node prev = (*assertionsToPreprocess)[i];
315	8770	Node res = eliminateLambdaComplete(prev, newLambda);
316	4385	if (res != prev)
317		{
318	306	res = rewrite(res);
319	306	Assert(!expr::hasFreeVar(res));
320	306	assertionsToPreprocess->replace(i, res);
321		}
322		}
323		// do lambda lifting on new lambda definitions
324		// this will do fixed point to eliminate lambdas within lambda lifting axioms.
325	235	while (!newLambda.empty())
326		{
327	48	std::map<Node, Node> lproc = newLambda;
328	24	newLambda.clear();
329	194	for (const std::pair<const Node, Node>& l : lproc)
330		{
331	340	Node lambda = l.second;
332	340	std::vector<Node> vars;
333	340	std::vector<Node> nvars;
334	596	for (const Node& v : lambda[0])
335		{
336	852	Node bv = nm->mkBoundVar(v.getType());
337	426	vars.push_back(v);
338	426	nvars.push_back(bv);
339		}
340
341		Node bd = lambda[1].substitute(
342	340	vars.begin(), vars.end(), nvars.begin(), nvars.end());
343	340	Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars);
344
345	170	nvars.insert(nvars.begin(), l.first);
346	340	Node curr = nm->mkNode(APPLY_UF, nvars);
347
348	340	Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd));
349	340	Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax
350	170	<< " for " << lambda << std::endl;
351	170	Assert(!expr::hasFreeVar(llfax));
352	340	Node llfaxe = eliminateLambdaComplete(llfax, newLambda);
353	340	Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for "
354	170	<< lambda << std::endl;
355	170	axioms.push_back(llfaxe);
356		}
357		}
358
359	187	d_visited.clear();
360		// add lambda lifting axioms as a conjunction to the first assertion
361	187	if (!axioms.empty())
362		{
363	40	Node conj = nm->mkAnd(axioms);
364	20	conj = rewrite(conj);
365	20	Assert(!expr::hasFreeVar(conj));
366	20	assertionsToPreprocess->conjoin(0, conj);
367		}
368	187	axioms.clear();
369
370		// step [2]: eliminate all higher-order constraints
371	4572	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
372		{
373	8770	Node prev = (*assertionsToPreprocess)[i];
374	8770	Node res = eliminateHo(prev);
375	4385	if (res != prev)
376		{
377	1432	res = rewrite(res);
378	1432	Assert(!expr::hasFreeVar(res));
379	1432	assertionsToPreprocess->replace(i, res);
380		}
381		}
382		// extensionality: process all function types
383	865	for (const TypeNode& ftn : d_funTypes)
384		{
385	678	if (options().quantifiers.hoElim)
386		{
387	530	Node h = getHoApplyUf(ftn);
388	265	Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl;
389	530	TypeNode ft = h.getType();
390	530	TypeNode uf = getUSort(ft[0]);
391	530	TypeNode ut = getUSort(ft[1]);
392		// extensionality
393	530	Node x = nm->mkBoundVar("x", uf);
394	530	Node y = nm->mkBoundVar("y", uf);
395	530	Node z = nm->mkBoundVar("z", ut);
396		Node eq =
397	530	nm->mkNode(APPLY_UF, h, x, z).eqNode(nm->mkNode(APPLY_UF, h, y, z));
398	530	Node antec = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, z), eq);
399	530	Node conc = x.eqNode(y);
400		Node ax = nm->mkNode(FORALL,
401	530	nm->mkNode(BOUND_VAR_LIST, x, y),
402	1060	nm->mkNode(OR, antec.negate(), conc));
403	265	axioms.push_back(ax);
404	265	Trace("ho-elim-ax") << "...ext axiom : " << ax << std::endl;
405		// Make the "store" axiom, which asserts for every function, there
406		// exists another function that acts like the "store" operator for
407		// arrays, e.g. it is the same function with one I/O pair updated.
408		// Without this axiom, the translation is model unsound.
409	265	if (options().quantifiers.hoElimStoreAx)
410		{
411	530	Node u = nm->mkBoundVar("u", uf);
412	530	Node v = nm->mkBoundVar("v", uf);
413	530	Node i = nm->mkBoundVar("i", ut);
414	530	Node ii = nm->mkBoundVar("ii", ut);
415	530	Node huii = nm->mkNode(APPLY_UF, h, u, ii);
416	530	Node e = nm->mkBoundVar("e", huii.getType());
417		Node store = nm->mkNode(
418		FORALL,
419	530	nm->mkNode(BOUND_VAR_LIST, u, e, i),
420	1060	nm->mkNode(EXISTS,
421	530	nm->mkNode(BOUND_VAR_LIST, v),
422	1060	nm->mkNode(FORALL,
423	530	nm->mkNode(BOUND_VAR_LIST, ii),
424	530	nm->mkNode(APPLY_UF, h, v, ii)
425	1060	.eqNode(nm->mkNode(
426	1590	ITE, ii.eqNode(i), e, huii)))));
427	265	axioms.push_back(store);
428	265	Trace("ho-elim-ax") << "...store axiom : " << store << std::endl;
429		}
430		}
431	413	else if (options().quantifiers.hoElimStoreAx)
432		{
433	2	Node u = nm->mkBoundVar("u", ftn);
434	2	Node v = nm->mkBoundVar("v", ftn);
435	2	std::vector<TypeNode> argTypes = ftn.getArgTypes();
436	2	Node i = nm->mkBoundVar("i", argTypes[0]);
437	2	Node ii = nm->mkBoundVar("ii", argTypes[0]);
438	2	Node huii = nm->mkNode(HO_APPLY, u, ii);
439	2	Node e = nm->mkBoundVar("e", huii.getType());
440		Node store = nm->mkNode(
441		FORALL,
442	2	nm->mkNode(BOUND_VAR_LIST, u, e, i),
443	4	nm->mkNode(
444		EXISTS,
445	2	nm->mkNode(BOUND_VAR_LIST, v),
446	4	nm->mkNode(FORALL,
447	2	nm->mkNode(BOUND_VAR_LIST, ii),
448	2	nm->mkNode(HO_APPLY, v, ii)
449	6	.eqNode(nm->mkNode(ITE, ii.eqNode(i), e, huii)))));
450	1	axioms.push_back(store);
451	2	Trace("ho-elim-ax") << "...store (ho_apply) axiom : " << store
452	1	<< std::endl;
453		}
454		}
455		// add new axioms as a conjunction to the first assertion
456	187	if (!axioms.empty())
457		{
458	20	Node conj = nm->mkAnd(axioms);
459	10	conj = rewrite(conj);
460	10	Assert(!expr::hasFreeVar(conj));
461	10	assertionsToPreprocess->conjoin(0, conj);
462		}
463
464	374	return PreprocessingPassResult::NO_CONFLICT;
465		}
466
467	2343	Node HoElim::getHoApplyUf(TypeNode tn)
468		{
469	4686	TypeNode tnu = getUSort(tn);
470	4686	TypeNode rangeType = tn.getRangeType();
471	4686	std::vector<TypeNode> argTypes = tn.getArgTypes();
472	4686	TypeNode tna = getUSort(argTypes[0]);
473
474	4686	TypeNode tr = rangeType;
475	2343	if (argTypes.size() > 1)
476		{
477	1400	std::vector<TypeNode> remArgTypes;
478	700	remArgTypes.insert(remArgTypes.end(), argTypes.begin() + 1, argTypes.end());
479	700	tr = NodeManager::currentNM()->mkFunctionType(remArgTypes, tr);
480		}
481	4686	TypeNode tnr = getUSort(tr);
482
483	4686	return getHoApplyUf(tnu, tna, tnr);
484		}
485
486	10139	Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr)
487		{
488	10139	std::map<TypeNode, Node>::iterator it = d_hoApplyUf.find(tnf);
489	10139	if (it == d_hoApplyUf.end())
490		{
491	265	NodeManager* nm = NodeManager::currentNM();
492	265	SkolemManager* sm = nm->getSkolemManager();
493
494	530	std::vector<TypeNode> hoTypeArgs;
495	265	hoTypeArgs.push_back(tnf);
496	265	hoTypeArgs.push_back(tna);
497	530	TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
498	530	Node k = sm->mkDummySkolem("ho", tnh);
499	265	d_hoApplyUf[tnf] = k;
500	265	return k;
501		}
502	9874	return it->second;
503		}
504
505	17883	TypeNode HoElim::getUSort(TypeNode tn)
506		{
507	17883	if (!tn.isFunction())
508		{
509	7170	return tn;
510		}
511	10713	std::map<TypeNode, TypeNode>::iterator it = d_ftypeMap.find(tn);
512	10713	if (it == d_ftypeMap.end())
513		{
514		// flatten function arguments
515	880	std::vector<TypeNode> argTypes = tn.getArgTypes();
516	880	TypeNode rangeType = tn.getRangeType();
517	440	bool typeChanged = false;
518	1419	for (unsigned i = 0; i < argTypes.size(); i++)
519		{
520	979	if (argTypes[i].isFunction())
521		{
522	275	argTypes[i] = getUSort(argTypes[i]);
523	275	typeChanged = true;
524		}
525		}
526	880	TypeNode s;
527	440	if (typeChanged)
528		{
529		TypeNode ntn =
530	350	NodeManager::currentNM()->mkFunctionType(argTypes, rangeType);
531	175	s = getUSort(ntn);
532		}
533		else
534		{
535	530	std::stringstream ss;
536	265	ss << "u_" << tn;
537	265	s = NodeManager::currentNM()->mkSort(ss.str());
538		}
539	440	d_ftypeMap[tn] = s;
540	440	return s;
541		}
542	10273	return it->second;
543		}
544
545		} // namespace passes
546		} // namespace preprocessing
547	29502	} // namespace cvc5