Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/ho_extension.cpp	Lines:	205	247	83.0 %
Date:	2021-09-30	Branches:	424	1032	41.1 %


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