Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/ho_extension.cpp	Lines:	204	246	82.9 %
Date:	2021-05-22	Branches:	425	1038	40.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of the higher-order extension of TheoryUF.
 */

#include "theory/uf/ho_extension.h"

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/uf_options.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace uf {

HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
    : d_state(state),
      d_im(im),
      d_extensionality(state.getUserContext()),
      d_uf_std_skolem(state.getUserContext())
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

Node HoExtension::ppRewrite(Node node)
{
  // convert HO_APPLY to APPLY_UF if fully applied
  if (node[0].getType().getNumChildren() == 2)
  {
    Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
    Node ret = getApplyUfForHoApply(node);
    Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
                   << std::endl;
    return ret;
  }
  return node;
}

Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
{
  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
  Assert(deq[0][0].getType().isFunction());
  if (isCached)
  {
    std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
    if (it != d_extensionality_deq.end())
    {
      return it->second;
    }
  }
  TypeNode tn = deq[0][0].getType();
  std::vector<TypeNode> argTypes = tn.getArgTypes();
  std::vector<Node> skolems;
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
  {
    Node k = sm->mkDummySkolem(
        "k", argTypes[i], "skolem created for extensionality.");
    skolems.push_back(k);
  }
  Node t[2];
  for (unsigned i = 0; i < 2; i++)
  {
    std::vector<Node> children;
    Node curr = deq[0][i];
    while (curr.getKind() == HO_APPLY)
    {
      children.push_back(curr[1]);
      curr = curr[0];
    }
    children.push_back(curr);
    std::reverse(children.begin(), children.end());
    children.insert(children.end(), skolems.begin(), skolems.end());
    t[i] = nm->mkNode(APPLY_UF, children);
  }
  Node conc = t[0].eqNode(t[1]).negate();
  if (isCached)
  {
    d_extensionality_deq[deq] = conc;
  }
  return conc;
}

unsigned HoExtension::applyExtensionality(TNode deq)
{
  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
  Assert(deq[0][0].getType().isFunction());
  // apply extensionality
  if (d_extensionality.find(deq) == d_extensionality.end())
  {
    d_extensionality.insert(deq);
    Node conc = getExtensionalityDeq(deq);
    Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
    Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                         << std::endl;
    d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
    return 1;
  }
  return 0;
}

Node HoExtension::getApplyUfForHoApply(Node node)
{
  Assert(node[0].getType().getNumChildren() == 2);
  std::vector<TNode> args;
  Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
  Node new_f = f;
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
  {
    NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
    if (itus == d_uf_std_skolem.end())
    {
      std::unordered_set<Node> fvs;
      expr::getFreeVariables(f, fvs);
      Node lem;
      if (!fvs.empty())
      {
        std::vector<TypeNode> newTypes;
        std::vector<Node> vs;
        std::vector<Node> nvs;
        for (const Node& v : fvs)
        {
          TypeNode vt = v.getType();
          newTypes.push_back(vt);
          Node nv = nm->mkBoundVar(vt);
          vs.push_back(v);
          nvs.push_back(nv);
        }
        TypeNode ft = f.getType();
        std::vector<TypeNode> argTypes = ft.getArgTypes();
        TypeNode rangeType = ft.getRangeType();

        newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
        TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
        new_f = sm->mkDummySkolem("app_uf", nft);
        for (const Node& v : vs)
        {
          new_f = nm->mkNode(HO_APPLY, new_f, v);
        }
        Assert(new_f.getType() == f.getType());
        Node eq = new_f.eqNode(f);
        Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
        lem = nm->mkNode(
            FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq);
      }
      else
      {
        // introduce skolem to make a standard APPLY_UF
        new_f = sm->mkDummySkolem("app_uf", f.getType());
        lem = new_f.eqNode(f);
      }
      Trace("uf-ho-lemma")
          << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
          << std::endl;
      d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
      d_uf_std_skolem[f] = new_f;
    }
    else
    {
      new_f = (*itus).second;
    }
    // unroll the HO_APPLY, adding to the first argument position
    // Note arguments in the vector args begin at position 1.
    while (new_f.getKind() == HO_APPLY)
    {
      args.insert(args.begin() + 1, new_f[1]);
      new_f = new_f[0];
    }
  }
  Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
  args[0] = new_f;
  Node ret = nm->mkNode(APPLY_UF, args);
  Assert(ret.getType() == node.getType());
  return ret;
}

unsigned HoExtension::checkExtensionality(TheoryModel* m)
{
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  NodeManager* nm = NodeManager::currentNM();
  unsigned num_lemmas = 0;
  bool isCollectModel = (m != nullptr);
  Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
                 << isCollectModel << "..." << std::endl;
  std::map<TypeNode, std::vector<Node> > func_eqcs;
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
  bool hasFunctions = false;
  while (!eqcs_i.isFinished())
  {
    Node eqc = (*eqcs_i);
    TypeNode tn = eqc.getType();
    if (tn.isFunction())
    {
      hasFunctions = true;
      // if during collect model, must have an infinite type
      // if not during collect model, must have a finite type
      if (d_state.isFiniteType(tn) != isCollectModel)
      {
        func_eqcs[tn].push_back(eqc);
        Trace("uf-ho-debug")
            << "  func eqc : " << tn << " : " << eqc << std::endl;
      }
    }
    ++eqcs_i;
  }
  if (!options::ufHoExt())
  {
    // we are not applying extensionality, thus we are incomplete if functions
    // are present
    if (hasFunctions)
    {
      d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED);
    }
    return 0;
  }

  for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
       itf != func_eqcs.end();
       ++itf)
  {
    for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
    {
      for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
      {
        // if these equivalence classes are not explicitly disequal, do
        // extensionality to ensure distinctness
        if (!ee->areDisequal(itf->second[j], itf->second[k], false))
        {
          Node deq =
              Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
          // either add to model, or add lemma
          if (isCollectModel)
          {
            // Add extentionality disequality to the model.
            // It is important that we construct new (unconstrained) variables
            // k here, so that we do not generate any inconsistencies.
            Node edeq = getExtensionalityDeq(deq, false);
            Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL);
            // introducing terms, must add required constraints, e.g. to
            // force equalities between APPLY_UF and HO_APPLY terms
            for (unsigned r = 0; r < 2; r++)
            {
              if (!collectModelInfoHoTerm(edeq[0][r], m))
              {
                return 1;
              }
            }
            Trace("uf-ho-debug")
                << "Add extensionality deq to model : " << edeq << std::endl;
            if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
            {
              Node eq = edeq[0][0].eqNode(edeq[0][1]);
              Node lem = nm->mkNode(OR, deq.negate(), eq);
              Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                             << std::endl;
              d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
              return 1;
            }
          }
          else
          {
            // apply extensionality lemma
            num_lemmas += applyExtensionality(deq);
          }
        }
      }
    }
  }
  return num_lemmas;
}

unsigned HoExtension::applyAppCompletion(TNode n)
{
  Assert(n.getKind() == APPLY_UF);

  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  // must expand into APPLY_HO version if not there already
  Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
  if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
  {
    Node eq = n.eqNode(ret);
    Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                         << std::endl;
    d_im.assertInternalFact(eq,
                            true,
                            InferenceId::UF_HO_APP_ENCODE,
                            PfRule::HO_APP_ENCODE,
                            {},
                            {n});
    return 1;
  }
  Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
                       << std::endl;
  return 0;
}

unsigned HoExtension::checkAppCompletion()
{
  Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
  // compute the operators that are relevant (those for which an HO_APPLY exist)
  std::set<TNode> rlvOp;
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
  std::map<TNode, std::vector<Node> > apply_uf;
  while (!eqcs_i.isFinished())
  {
    Node eqc = (*eqcs_i);
    Trace("uf-ho-debug") << "  apply completion : visit eqc " << eqc
                         << std::endl;
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
    while (!eqc_i.isFinished())
    {
      Node n = *eqc_i;
      if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY)
      {
        int curr_sum = 0;
        std::map<TNode, bool> curr_rops;
        if (n.getKind() == APPLY_UF)
        {
          TNode rop = ee->getRepresentative(n.getOperator());
          if (rlvOp.find(rop) != rlvOp.end())
          {
            // try if its operator is relevant
            curr_sum = applyAppCompletion(n);
            if (curr_sum > 0)
            {
              return curr_sum;
            }
          }
          else
          {
            // add to pending list
            apply_uf[rop].push_back(n);
          }
          // Arguments are also relevant operators.
          // It might be possible include fewer terms here, see #1115.
          for (unsigned k = 0; k < n.getNumChildren(); k++)
          {
            if (n[k].getType().isFunction())
            {
              TNode rop2 = ee->getRepresentative(n[k]);
              curr_rops[rop2] = true;
            }
          }
        }
        else
        {
          Assert(n.getKind() == HO_APPLY);
          TNode rop = ee->getRepresentative(n[0]);
          curr_rops[rop] = true;
        }
        for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
             itc != curr_rops.end();
             ++itc)
        {
          TNode rop = itc->first;
          if (rlvOp.find(rop) == rlvOp.end())
          {
            rlvOp.insert(rop);
            // now, try each pending APPLY_UF for this operator
            std::map<TNode, std::vector<Node> >::iterator itu =
                apply_uf.find(rop);
            if (itu != apply_uf.end())
            {
              for (unsigned j = 0, size = itu->second.size(); j < size; j++)
              {
                curr_sum = applyAppCompletion(itu->second[j]);
                if (curr_sum > 0)
                {
                  return curr_sum;
                }
              }
            }
          }
        }
      }
      ++eqc_i;
    }
    ++eqcs_i;
  }
  return 0;
}

unsigned HoExtension::check()
{
  Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;

  // infer new facts based on apply completion until fixed point
  unsigned num_facts;
  do
  {
    num_facts = checkAppCompletion();
    if (d_state.isInConflict())
    {
      Trace("uf-ho") << "...conflict during app-completion." << std::endl;
      return 1;
    }
  } while (num_facts > 0);

  unsigned num_lemmas = 0;

  num_lemmas = checkExtensionality();
  if (num_lemmas > 0)
  {
    Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas."
                   << std::endl;
    return num_lemmas;
  }

  Trace("uf-ho") << "...finished check higher order." << std::endl;

  return 0;
}

bool HoExtension::collectModelInfoHo(TheoryModel* m,
                                     const std::set<Node>& termSet)
{
  for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
  {
    Node n = *it;
    // For model-building with ufHo, we require that APPLY_UF is always
    // expanded to HO_APPLY. That is, we always expand to a fully applicative
    // encoding during model construction.
    if (!collectModelInfoHoTerm(n, m))
    {
      return false;
    }
  }
  int addedLemmas = checkExtensionality(m);
  return addedLemmas == 0;
}

bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
{
  if (n.getKind() == APPLY_UF)
  {
    Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
    if (!m->assertEquality(n, hn, true))
    {
      Node eq = n.eqNode(hn);
      Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                     << std::endl;
      d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
      return false;
    }
  }
  return true;
}

}  // namespace uf
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer, Mathias Preiner
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		* Implementation of the higher-order extension of TheoryUF.
14		*/
15
16		#include "theory/uf/ho_extension.h"
17
18		#include "expr/node_algorithm.h"
19		#include "expr/skolem_manager.h"
20		#include "options/uf_options.h"
21		#include "theory/theory_model.h"
22		#include "theory/uf/theory_uf_rewriter.h"
23
24		using namespace std;
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace uf {
30
31	200	HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
32		: d_state(state),
33		d_im(im),
34	200	d_extensionality(state.getUserContext()),
35	400	d_uf_std_skolem(state.getUserContext())
36		{
37	200	d_true = NodeManager::currentNM()->mkConst(true);
38	200	}
39
40	276	Node HoExtension::ppRewrite(Node node)
41		{
42		// convert HO_APPLY to APPLY_UF if fully applied
43	276	if (node[0].getType().getNumChildren() == 2)
44		{
45	121	Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
46	242	Node ret = getApplyUfForHoApply(node);
47	242	Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
48	121	<< std::endl;
49	121	return ret;
50		}
51	155	return node;
52		}
53
54	733	Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
55		{
56	733	Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
57	733	Assert(deq[0][0].getType().isFunction());
58	733	if (isCached)
59		{
60	159	std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
61	159	if (it != d_extensionality_deq.end())
62		{
63		return it->second;
64		}
65		}
66	1466	TypeNode tn = deq[0][0].getType();
67	1466	std::vector<TypeNode> argTypes = tn.getArgTypes();
68	1466	std::vector<Node> skolems;
69	733	NodeManager* nm = NodeManager::currentNM();
70	733	SkolemManager* sm = nm->getSkolemManager();
71	1505	for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
72		{
73		Node k = sm->mkDummySkolem(
74	1544	"k", argTypes[i], "skolem created for extensionality.");
75	772	skolems.push_back(k);
76		}
77	1466	Node t[2];
78	2199	for (unsigned i = 0; i < 2; i++)
79		{
80	2932	std::vector<Node> children;
81	2932	Node curr = deq[0][i];
82	2120	while (curr.getKind() == HO_APPLY)
83		{
84	327	children.push_back(curr[1]);
85	327	curr = curr[0];
86		}
87	1466	children.push_back(curr);
88	1466	std::reverse(children.begin(), children.end());
89	1466	children.insert(children.end(), skolems.begin(), skolems.end());
90	1466	t[i] = nm->mkNode(APPLY_UF, children);
91		}
92	1466	Node conc = t[0].eqNode(t[1]).negate();
93	733	if (isCached)
94		{
95	159	d_extensionality_deq[deq] = conc;
96		}
97	733	return conc;
98		}
99
100	384	unsigned HoExtension::applyExtensionality(TNode deq)
101		{
102	384	Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
103	384	Assert(deq[0][0].getType().isFunction());
104		// apply extensionality
105	384	if (d_extensionality.find(deq) == d_extensionality.end())
106		{
107	159	d_extensionality.insert(deq);
108	318	Node conc = getExtensionalityDeq(deq);
109	318	Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
110	318	Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
111	159	<< std::endl;
112	159	d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
113	159	return 1;
114		}
115	225	return 0;
116		}
117
118	121	Node HoExtension::getApplyUfForHoApply(Node node)
119		{
120	121	Assert(node[0].getType().getNumChildren() == 2);
121	242	std::vector<TNode> args;
122	242	Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
123	242	Node new_f = f;
124	121	NodeManager* nm = NodeManager::currentNM();
125	121	SkolemManager* sm = nm->getSkolemManager();
126	121	if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
127		{
128	2	NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
129	2	if (itus == d_uf_std_skolem.end())
130		{
131	4	std::unordered_set<Node> fvs;
132	2	expr::getFreeVariables(f, fvs);
133	4	Node lem;
134	2	if (!fvs.empty())
135		{
136		std::vector<TypeNode> newTypes;
137		std::vector<Node> vs;
138		std::vector<Node> nvs;
139		for (const Node& v : fvs)
140		{
141		TypeNode vt = v.getType();
142		newTypes.push_back(vt);
143		Node nv = nm->mkBoundVar(vt);
144		vs.push_back(v);
145		nvs.push_back(nv);
146		}
147		TypeNode ft = f.getType();
148		std::vector<TypeNode> argTypes = ft.getArgTypes();
149		TypeNode rangeType = ft.getRangeType();
150
151		newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
152		TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
153		new_f = sm->mkDummySkolem("app_uf", nft);
154		for (const Node& v : vs)
155		{
156		new_f = nm->mkNode(HO_APPLY, new_f, v);
157		}
158		Assert(new_f.getType() == f.getType());
159		Node eq = new_f.eqNode(f);
160		Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
161		lem = nm->mkNode(
162		FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq);
163		}
164		else
165		{
166		// introduce skolem to make a standard APPLY_UF
167	2	new_f = sm->mkDummySkolem("app_uf", f.getType());
168	2	lem = new_f.eqNode(f);
169		}
170	4	Trace("uf-ho-lemma")
171	2	<< "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
172	2	<< std::endl;
173	2	d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
174	2	d_uf_std_skolem[f] = new_f;
175		}
176		else
177		{
178		new_f = (*itus).second;
179		}
180		// unroll the HO_APPLY, adding to the first argument position
181		// Note arguments in the vector args begin at position 1.
182	2	while (new_f.getKind() == HO_APPLY)
183		{
184		args.insert(args.begin() + 1, new_f[1]);
185		new_f = new_f[0];
186		}
187		}
188	121	Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
189	121	args[0] = new_f;
190	121	Node ret = nm->mkNode(APPLY_UF, args);
191	121	Assert(ret.getType() == node.getType());
192	242	return ret;
193		}
194
195	1408	unsigned HoExtension::checkExtensionality(TheoryModel* m)
196		{
197	1408	eq::EqualityEngine* ee = d_state.getEqualityEngine();
198	1408	NodeManager* nm = NodeManager::currentNM();
199	1408	unsigned num_lemmas = 0;
200	1408	bool isCollectModel = (m != nullptr);
201	2816	Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
202	1408	<< isCollectModel << "..." << std::endl;
203	2816	std::map<TypeNode, std::vector<Node> > func_eqcs;
204	1408	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
205	1408	bool hasFunctions = false;
206	63972	while (!eqcs_i.isFinished())
207		{
208	62564	Node eqc = (*eqcs_i);
209	62564	TypeNode tn = eqc.getType();
210	31282	if (tn.isFunction())
211		{
212	4360	hasFunctions = true;
213		// if during collect model, must have an infinite type
214		// if not during collect model, must have a finite type
215	4360	if (d_state.isFiniteType(tn) != isCollectModel)
216		{
217	1936	func_eqcs[tn].push_back(eqc);
218	3872	Trace("uf-ho-debug")
219	1936	<< " func eqc : " << tn << " : " << eqc << std::endl;
220		}
221		}
222	31282	++eqcs_i;
223		}
224	74235	if (!options::ufHoExt())
225		{
226		// we are not applying extensionality, thus we are incomplete if functions
227		// are present
228		if (hasFunctions)
229		{
230		d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED);
231		}
232		return 0;
233		}
234
235	2664	for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
236	2664	itf != func_eqcs.end();
237		++itf)
238		{
239	3192	for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
240		{
241	2954	for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
242		{
243		// if these equivalence classes are not explicitly disequal, do
244		// extensionality to ensure distinctness
245	1018	if (!ee->areDisequal(itf->second[j], itf->second[k], false))
246		{
247		Node deq =
248	1314	Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
249		// either add to model, or add lemma
250	657	if (isCollectModel)
251		{
252		// Add extentionality disequality to the model.
253		// It is important that we construct new (unconstrained) variables
254		// k here, so that we do not generate any inconsistencies.
255	1148	Node edeq = getExtensionalityDeq(deq, false);
256	574	Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL);
257		// introducing terms, must add required constraints, e.g. to
258		// force equalities between APPLY_UF and HO_APPLY terms
259	1722	for (unsigned r = 0; r < 2; r++)
260		{
261	1148	if (!collectModelInfoHoTerm(edeq[0][r], m))
262		{
263		return 1;
264		}
265		}
266	1148	Trace("uf-ho-debug")
267	574	<< "Add extensionality deq to model : " << edeq << std::endl;
268	574	if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
269		{
270		Node eq = edeq[0][0].eqNode(edeq[0][1]);
271		Node lem = nm->mkNode(OR, deq.negate(), eq);
272		Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
273		<< std::endl;
274		d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
275		return 1;
276		}
277		}
278		else
279		{
280		// apply extensionality lemma
281	83	num_lemmas += applyExtensionality(deq);
282		}
283		}
284		}
285		}
286		}
287	1408	return num_lemmas;
288		}
289
290	10684	unsigned HoExtension::applyAppCompletion(TNode n)
291		{
292	10684	Assert(n.getKind() == APPLY_UF);
293
294	10684	eq::EqualityEngine* ee = d_state.getEqualityEngine();
295		// must expand into APPLY_HO version if not there already
296	21368	Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
297	10684	if (!ee->hasTerm(ret) \|\| !ee->areEqual(ret, n))
298		{
299	2382	Node eq = n.eqNode(ret);
300	2382	Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
301	1191	<< std::endl;
302	2382	d_im.assertInternalFact(eq,
303		true,
304		InferenceId::UF_HO_APP_ENCODE,
305		PfRule::HO_APP_ENCODE,
306		{},
307	1191	{n});
308	1191	return 1;
309		}
310	18986	Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "."
311	9493	<< std::endl;
312	9493	return 0;
313		}
314
315	2168	unsigned HoExtension::checkAppCompletion()
316		{
317	2168	Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
318		// compute the operators that are relevant (those for which an HO_APPLY exist)
319	4336	std::set<TNode> rlvOp;
320	2168	eq::EqualityEngine* ee = d_state.getEqualityEngine();
321	2168	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
322	4336	std::map<TNode, std::vector<Node> > apply_uf;
323	81546	while (!eqcs_i.isFinished())
324		{
325	80569	Node eqc = (*eqcs_i);
326	81760	Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc
327	40880	<< std::endl;
328	40880	eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
329	544032	while (!eqc_i.isFinished())
330		{
331	504343	Node n = *eqc_i;
332	252767	if (n.getKind() == APPLY_UF \|\| n.getKind() == HO_APPLY)
333		{
334	88276	int curr_sum = 0;
335	175361	std::map<TNode, bool> curr_rops;
336	88276	if (n.getKind() == APPLY_UF)
337		{
338	150869	TNode rop = ee->getRepresentative(n.getOperator());
339	75795	if (rlvOp.find(rop) != rlvOp.end())
340		{
341		// try if its operator is relevant
342	7820	curr_sum = applyAppCompletion(n);
343	7820	if (curr_sum > 0)
344		{
345	721	return curr_sum;
346		}
347		}
348		else
349		{
350		// add to pending list
351	67975	apply_uf[rop].push_back(n);
352		}
353		// Arguments are also relevant operators.
354		// It might be possible include fewer terms here, see #1115.
355	217846	for (unsigned k = 0; k < n.getNumChildren(); k++)
356		{
357	142772	if (n[k].getType().isFunction())
358		{
359	6178	TNode rop2 = ee->getRepresentative(n[k]);
360	3089	curr_rops[rop2] = true;
361		}
362		}
363		}
364		else
365		{
366	12481	Assert(n.getKind() == HO_APPLY);
367	24962	TNode rop = ee->getRepresentative(n[0]);
368	12481	curr_rops[rop] = true;
369		}
370	102583	for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
371	102583	itc != curr_rops.end();
372		++itc)
373		{
374	30526	TNode rop = itc->first;
375	15498	if (rlvOp.find(rop) == rlvOp.end())
376		{
377	4087	rlvOp.insert(rop);
378		// now, try each pending APPLY_UF for this operator
379		std::map<TNode, std::vector<Node> >::iterator itu =
380	4087	apply_uf.find(rop);
381	4087	if (itu != apply_uf.end())
382		{
383	2986	for (unsigned j = 0, size = itu->second.size(); j < size; j++)
384		{
385	2864	curr_sum = applyAppCompletion(itu->second[j]);
386	2864	if (curr_sum > 0)
387		{
388	470	return curr_sum;
389		}
390		}
391		}
392		}
393		}
394		}
395	251576	++eqc_i;
396		}
397	39689	++eqcs_i;
398		}
399	977	return 0;
400		}
401
402	1041	unsigned HoExtension::check()
403		{
404	1041	Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;
405
406		// infer new facts based on apply completion until fixed point
407		unsigned num_facts;
408	1127	do
409		{
410	2168	num_facts = checkAppCompletion();
411	2168	if (d_state.isInConflict())
412		{
413	64	Trace("uf-ho") << "...conflict during app-completion." << std::endl;
414	64	return 1;
415		}
416	2104	} while (num_facts > 0);
417
418	977	unsigned num_lemmas = 0;
419
420	977	num_lemmas = checkExtensionality();
421	977	if (num_lemmas > 0)
422		{
423	74	Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas."
424	37	<< std::endl;
425	37	return num_lemmas;
426		}
427
428	940	Trace("uf-ho") << "...finished check higher order." << std::endl;
429
430	940	return 0;
431		}
432
433	431	bool HoExtension::collectModelInfoHo(TheoryModel* m,
434		const std::set<Node>& termSet)
435		{
436	3512	for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
437		{
438	6162	Node n = *it;
439		// For model-building with ufHo, we require that APPLY_UF is always
440		// expanded to HO_APPLY. That is, we always expand to a fully applicative
441		// encoding during model construction.
442	3081	if (!collectModelInfoHoTerm(n, m))
443		{
444		return false;
445		}
446		}
447	431	int addedLemmas = checkExtensionality(m);
448	431	return addedLemmas == 0;
449		}
450
451	4229	bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
452		{
453	4229	if (n.getKind() == APPLY_UF)
454		{
455	4422	Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
456	2211	if (!m->assertEquality(n, hn, true))
457		{
458		Node eq = n.eqNode(hn);
459		Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
460		<< std::endl;
461		d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
462		return false;
463		}
464		}
465	4229	return true;
466		}
467
468		} // namespace uf
469		} // namespace theory
470	101021	} // namespace cvc5