Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/ho_elim.cpp	Lines:	323	330	97.9 %
Date:	2021-05-22	Branches:	708	1538	46.0 %


/******************************************************************************
 * 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::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::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::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 = 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<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 = theory::Rewriter::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 = 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<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 = theory::Rewriter::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	9459	HoElim::HoElim(PreprocessingPassContext* preprocContext)
36	9459	: PreprocessingPass(preprocContext, "ho-elim"){};
37
38	4702	Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
39		{
40	4702	NodeManager* nm = NodeManager::currentNM();
41	4702	SkolemManager* sm = nm->getSkolemManager();
42	4702	std::unordered_map<Node, Node>::iterator it;
43	9404	std::vector<Node> visit;
44	9404	TNode cur;
45	4702	visit.push_back(n);
46	106450	do
47		{
48	111152	cur = visit.back();
49	111152	visit.pop_back();
50	111152	it = d_visited.find(cur);
51
52	111152	if (it == d_visited.end())
53		{
54	43605	if (cur.getKind() == LAMBDA)
55		{
56	185	Trace("ho-elim-ll") << "Lambda lift: " << cur << std::endl;
57		// must also get free variables in lambda
58	370	std::vector<Node> lvars;
59	370	std::vector<TypeNode> ftypes;
60	370	std::unordered_set<Node> fvs;
61	185	expr::getFreeVariables(cur, fvs);
62	370	std::vector<Node> nvars;
63	370	std::vector<Node> vars;
64	370	Node sbd = cur[1];
65	185	if (!fvs.empty())
66		{
67	252	Trace("ho-elim-ll")
68	126	<< "Has " << fvs.size() << " free variables" << std::endl;
69	352	for (const Node& v : fvs)
70		{
71	452	TypeNode vt = v.getType();
72	226	ftypes.push_back(vt);
73	452	Node vs = nm->mkBoundVar(vt);
74	226	vars.push_back(v);
75	226	nvars.push_back(vs);
76	226	lvars.push_back(vs);
77		}
78	126	sbd = sbd.substitute(
79		vars.begin(), vars.end(), nvars.begin(), nvars.end());
80		}
81	391	for (const Node& bv : cur[0])
82		{
83	412	TypeNode bvt = bv.getType();
84	206	ftypes.push_back(bvt);
85	206	lvars.push_back(bv);
86		}
87	370	Node nlambda = cur;
88	185	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	370	TypeNode rangeType = cur.getType().getRangeType();
95	370	TypeNode nft = nm->mkFunctionType(ftypes, rangeType);
96	370	Node nf = sm->mkDummySkolem("ll", nft);
97	370	Trace("ho-elim-ll")
98	185	<< "...introduce: " << nf << " of type " << nft << std::endl;
99	185	newLambda[nf] = nlambda;
100	185	Assert(nf.getType() == nlambda.getType());
101	185	if (!vars.empty())
102		{
103	352	for (const Node& v : vars)
104		{
105	226	nf = nm->mkNode(HO_APPLY, nf, v);
106		}
107	126	Trace("ho-elim-ll") << "...partial application: " << nf << std::endl;
108		}
109	185	d_visited[cur] = nf;
110	370	Trace("ho-elim-ll") << "...return types : " << nf.getType() << " "
111	185	<< cur.getType() << std::endl;
112	185	Assert(nf.getType() == cur.getType());
113		}
114		else
115		{
116	43420	d_visited[cur] = Node::null();
117	43420	visit.push_back(cur);
118	106450	for (const Node& cn : cur)
119		{
120	63030	visit.push_back(cn);
121		}
122		}
123		}
124	67547	else if (it->second.isNull())
125		{
126	86840	Node ret = cur;
127	43420	bool childChanged = false;
128	86840	std::vector<Node> children;
129	43420	if (cur.getMetaKind() == metakind::PARAMETERIZED)
130		{
131	8276	children.push_back(cur.getOperator());
132		}
133	106450	for (const Node& cn : cur)
134		{
135	63030	it = d_visited.find(cn);
136	63030	Assert(it != d_visited.end());
137	63030	Assert(!it->second.isNull());
138	63030	childChanged = childChanged \|\| cn != it->second;
139	63030	children.push_back(it->second);
140		}
141	43420	if (childChanged)
142		{
143	1460	ret = nm->mkNode(cur.getKind(), children);
144		}
145	43420	d_visited[cur] = ret;
146		}
147	111152	} while (!visit.empty());
148	4702	Assert(d_visited.find(n) != d_visited.end());
149	4702	Assert(!d_visited.find(n)->second.isNull());
150	9404	return d_visited[n];
151		}
152
153	4517	Node HoElim::eliminateHo(Node n)
154		{
155	4517	Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
156	4517	NodeManager* nm = NodeManager::currentNM();
157	4517	SkolemManager* sm = nm->getSkolemManager();
158	4517	std::unordered_map<Node, Node>::iterator it;
159	9034	std::map<Node, Node> preReplace;
160	4517	std::map<Node, Node>::iterator itr;
161	9034	std::vector<TNode> visit;
162	9034	TNode cur;
163	4517	visit.push_back(n);
164	101573	do
165		{
166	106090	cur = visit.back();
167	106090	visit.pop_back();
168	106090	it = d_visited.find(cur);
169	106090	Trace("ho-elim-visit") << "Process: " << cur << std::endl;
170
171	106090	if (it == d_visited.end())
172		{
173	89840	TypeNode tn = cur.getType();
174		// lambdas are already eliminated by now
175	44920	Assert(cur.getKind() != LAMBDA);
176	44920	if (tn.isFunction())
177		{
178	7618	d_funTypes.insert(tn);
179		}
180	44920	if (cur.isVar())
181		{
182	19634	Node ret = cur;
183	36567	if (options::hoElim())
184		{
185	3327	if (tn.isFunction())
186		{
187	4088	TypeNode ut = getUSort(tn);
188	2044	if (cur.getKind() == BOUND_VARIABLE)
189		{
190	1672	ret = nm->mkBoundVar(ut);
191		}
192		else
193		{
194	372	ret = sm->mkDummySkolem("k", ut);
195		}
196		// must get the ho apply to ensure extensionality is applied
197	4088	Node hoa = getHoApplyUf(tn);
198	2044	Trace("ho-elim-visit") << "Hoa is " << hoa << std::endl;
199		}
200		}
201	9817	d_visited[cur] = ret;
202		}
203		else
204		{
205	35103	d_visited[cur] = Node::null();
206	35103	if (cur.getKind() == APPLY_UF && options::hoElim())
207		{
208	2000	Node op = cur.getOperator();
209		// convert apply uf with variable arguments eagerly to ho apply
210		// chains, so they are processed uniformly.
211	1000	visit.push_back(cur);
212	2000	Node newCur = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(cur);
213	1000	preReplace[cur] = newCur;
214	1000	cur = newCur;
215	1000	d_visited[cur] = Node::null();
216		}
217	35103	visit.push_back(cur);
218	100573	for (const Node& cn : cur)
219		{
220	65470	visit.push_back(cn);
221		}
222		}
223		}
224	61170	else if (it->second.isNull())
225		{
226	72206	Node ret = cur;
227	36103	itr = preReplace.find(cur);
228	36103	if (itr != preReplace.end())
229		{
230	2000	Trace("ho-elim-visit")
231	1000	<< "return (pre-repl): " << d_visited[itr->second] << std::endl;
232	1000	d_visited[cur] = d_visited[itr->second];
233		}
234		else
235		{
236	35103	bool childChanged = false;
237	70206	std::vector<Node> children;
238	70206	std::vector<TypeNode> childrent;
239	35103	bool typeChanged = false;
240	100573	for (const Node& cn : ret)
241		{
242	65470	it = d_visited.find(cn);
243	65470	Assert(it != d_visited.end());
244	65470	Assert(!it->second.isNull());
245	65470	childChanged = childChanged \|\| cn != it->second;
246	65470	children.push_back(it->second);
247	130940	TypeNode ct = it->second.getType();
248	65470	childrent.push_back(ct);
249	65470	typeChanged = typeChanged \|\| ct != cn.getType();
250		}
251	35103	if (ret.getMetaKind() == metakind::PARAMETERIZED)
252		{
253		// child of an argument changed type, must change type
254	14552	Node op = ret.getOperator();
255	14552	Node retOp = op;
256	14552	Trace("ho-elim-visit")
257	7276	<< "Process op " << op << ", typeChanged = " << typeChanged
258	7276	<< std::endl;
259	7276	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	7276	children.insert(children.begin(), retOp);
276		}
277		// process ho apply
278	35103	if (ret.getKind() == HO_APPLY && options::hoElim())
279		{
280	14468	TypeNode tnr = ret.getType();
281	7234	tnr = getUSort(tnr);
282		Node hoa =
283	14468	getHoApplyUf(children[0].getType(), children[1].getType(), tnr);
284	14468	std::vector<Node> hchildren;
285	7234	hchildren.push_back(hoa);
286	7234	hchildren.push_back(children[0]);
287	7234	hchildren.push_back(children[1]);
288	7234	ret = nm->mkNode(APPLY_UF, hchildren);
289		}
290	27869	else if (childChanged)
291		{
292	4901	ret = nm->mkNode(ret.getKind(), children);
293		}
294	35103	Trace("ho-elim-visit") << "return (pre-repl): " << ret << std::endl;
295	35103	d_visited[cur] = ret;
296		}
297		}
298	106090	} while (!visit.empty());
299	4517	Assert(d_visited.find(n) != d_visited.end());
300	4517	Assert(!d_visited.find(n)->second.isNull());
301	4517	Trace("ho-elim-assert") << "...got : " << d_visited[n] << std::endl;
302	9034	return d_visited[n];
303		}
304
305	198	PreprocessingPassResult HoElim::applyInternal(
306		AssertionPipeline* assertionsToPreprocess)
307		{
308		// step [1]: apply lambda lifting to eliminate all lambdas
309	198	NodeManager* nm = NodeManager::currentNM();
310	396	std::vector<Node> axioms;
311	396	std::map<Node, Node> newLambda;
312	4715	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
313		{
314	9034	Node prev = (*assertionsToPreprocess)[i];
315	9034	Node res = eliminateLambdaComplete(prev, newLambda);
316	4517	if (res != prev)
317		{
318	309	res = theory::Rewriter::rewrite(res);
319	309	Assert(!expr::hasFreeVar(res));
320	309	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	262	while (!newLambda.empty())
326		{
327	64	std::map<Node, Node> lproc = newLambda;
328	32	newLambda.clear();
329	217	for (const std::pair<const Node, Node>& l : lproc)
330		{
331	370	Node lambda = l.second;
332	370	std::vector<Node> vars;
333	370	std::vector<Node> nvars;
334	617	for (const Node& v : lambda[0])
335		{
336	864	Node bv = nm->mkBoundVar(v.getType());
337	432	vars.push_back(v);
338	432	nvars.push_back(bv);
339		}
340
341		Node bd = lambda[1].substitute(
342	370	vars.begin(), vars.end(), nvars.begin(), nvars.end());
343	370	Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars);
344
345	185	nvars.insert(nvars.begin(), l.first);
346	370	Node curr = nm->mkNode(APPLY_UF, nvars);
347
348	370	Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd));
349	370	Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax
350	185	<< " for " << lambda << std::endl;
351	185	Assert(!expr::hasFreeVar(llfax));
352	370	Node llfaxe = eliminateLambdaComplete(llfax, newLambda);
353	370	Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for "
354	185	<< lambda << std::endl;
355	185	axioms.push_back(llfaxe);
356		}
357		}
358
359	198	d_visited.clear();
360		// add lambda lifting axioms as a conjunction to the first assertion
361	198	if (!axioms.empty())
362		{
363	60	Node conj = nm->mkAnd(axioms);
364	30	conj = theory::Rewriter::rewrite(conj);
365	30	Assert(!expr::hasFreeVar(conj));
366	30	assertionsToPreprocess->conjoin(0, conj);
367		}
368	198	axioms.clear();
369
370		// step [2]: eliminate all higher-order constraints
371	4715	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
372		{
373	9034	Node prev = (*assertionsToPreprocess)[i];
374	9034	Node res = eliminateHo(prev);
375	4517	if (res != prev)
376		{
377	1420	res = theory::Rewriter::rewrite(res);
378	1420	Assert(!expr::hasFreeVar(res));
379	1420	assertionsToPreprocess->replace(i, res);
380		}
381		}
382		// extensionality: process all function types
383	883	for (const TypeNode& ftn : d_funTypes)
384		{
385	685	if (options::hoElim())
386		{
387	528	Node h = getHoApplyUf(ftn);
388	264	Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl;
389	528	TypeNode ft = h.getType();
390	528	TypeNode uf = getUSort(ft[0]);
391	528	TypeNode ut = getUSort(ft[1]);
392		// extensionality
393	528	Node x = nm->mkBoundVar("x", uf);
394	528	Node y = nm->mkBoundVar("y", uf);
395	528	Node z = nm->mkBoundVar("z", ut);
396		Node eq =
397	528	nm->mkNode(APPLY_UF, h, x, z).eqNode(nm->mkNode(APPLY_UF, h, y, z));
398	528	Node antec = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, z), eq);
399	528	Node conc = x.eqNode(y);
400		Node ax = nm->mkNode(FORALL,
401	528	nm->mkNode(BOUND_VAR_LIST, x, y),
402	1056	nm->mkNode(OR, antec.negate(), conc));
403	264	axioms.push_back(ax);
404	264	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	1349	if (options::hoElimStoreAx())
410		{
411	528	Node u = nm->mkBoundVar("u", uf);
412	528	Node v = nm->mkBoundVar("v", uf);
413	528	Node i = nm->mkBoundVar("i", ut);
414	528	Node ii = nm->mkBoundVar("ii", ut);
415	528	Node huii = nm->mkNode(APPLY_UF, h, u, ii);
416	528	Node e = nm->mkBoundVar("e", huii.getType());
417		Node store = nm->mkNode(
418		FORALL,
419	528	nm->mkNode(BOUND_VAR_LIST, u, e, i),
420	1056	nm->mkNode(EXISTS,
421	528	nm->mkNode(BOUND_VAR_LIST, v),
422	1056	nm->mkNode(FORALL,
423	528	nm->mkNode(BOUND_VAR_LIST, ii),
424	528	nm->mkNode(APPLY_UF, h, v, ii)
425	1056	.eqNode(nm->mkNode(
426	1584	ITE, ii.eqNode(i), e, huii)))));
427	264	axioms.push_back(store);
428	264	Trace("ho-elim-ax") << "...store axiom : " << store << std::endl;
429		}
430		}
431	421	else if (options::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	198	if (!axioms.empty())
457		{
458	26	Node conj = nm->mkAnd(axioms);
459	13	conj = theory::Rewriter::rewrite(conj);
460	13	Assert(!expr::hasFreeVar(conj));
461	13	assertionsToPreprocess->conjoin(0, conj);
462		}
463
464	396	return PreprocessingPassResult::NO_CONFLICT;
465		}
466
467	2308	Node HoElim::getHoApplyUf(TypeNode tn)
468		{
469	4616	TypeNode tnu = getUSort(tn);
470	4616	TypeNode rangeType = tn.getRangeType();
471	4616	std::vector<TypeNode> argTypes = tn.getArgTypes();
472	4616	TypeNode tna = getUSort(argTypes[0]);
473
474	4616	TypeNode tr = rangeType;
475	2308	if (argTypes.size() > 1)
476		{
477	1360	std::vector<TypeNode> remArgTypes;
478	680	remArgTypes.insert(remArgTypes.end(), argTypes.begin() + 1, argTypes.end());
479	680	tr = NodeManager::currentNM()->mkFunctionType(remArgTypes, tr);
480		}
481	4616	TypeNode tnr = getUSort(tr);
482
483	4616	return getHoApplyUf(tnu, tna, tnr);
484		}
485
486	9542	Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr)
487		{
488	9542	std::map<TypeNode, Node>::iterator it = d_hoApplyUf.find(tnf);
489	9542	if (it == d_hoApplyUf.end())
490		{
491	264	NodeManager* nm = NodeManager::currentNM();
492	264	SkolemManager* sm = nm->getSkolemManager();
493
494	528	std::vector<TypeNode> hoTypeArgs;
495	264	hoTypeArgs.push_back(tnf);
496	264	hoTypeArgs.push_back(tna);
497	528	TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
498	528	Node k = sm->mkDummySkolem("ho", tnh);
499	264	d_hoApplyUf[tnf] = k;
500	264	return k;
501		}
502	9278	return it->second;
503		}
504
505	17171	TypeNode HoElim::getUSort(TypeNode tn)
506		{
507	17171	if (!tn.isFunction())
508		{
509	6795	return tn;
510		}
511	10376	std::map<TypeNode, TypeNode>::iterator it = d_ftypeMap.find(tn);
512	10376	if (it == d_ftypeMap.end())
513		{
514		// flatten function arguments
515	872	std::vector<TypeNode> argTypes = tn.getArgTypes();
516	872	TypeNode rangeType = tn.getRangeType();
517	436	bool typeChanged = false;
518	1405	for (unsigned i = 0; i < argTypes.size(); i++)
519		{
520	969	if (argTypes[i].isFunction())
521		{
522	269	argTypes[i] = getUSort(argTypes[i]);
523	269	typeChanged = true;
524		}
525		}
526	872	TypeNode s;
527	436	if (typeChanged)
528		{
529		TypeNode ntn =
530	344	NodeManager::currentNM()->mkFunctionType(argTypes, rangeType);
531	172	s = getUSort(ntn);
532		}
533		else
534		{
535	528	std::stringstream ss;
536	264	ss << "u_" << tn;
537	264	s = NodeManager::currentNM()->mkSort(ss.str());
538		}
539	436	d_ftypeMap[tn] = s;
540	436	return s;
541		}
542	9940	return it->second;
543		}
544
545		} // namespace passes
546		} // namespace preprocessing
547	56026	} // namespace cvc5