Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/ho_extension.cpp	Lines:	205	247	83.0 %
Date:	2021-09-15	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	191	HoExtension::HoExtension(Env& env,
32		TheoryState& state,
33	191	TheoryInferenceManager& im)
34		: EnvObj(env),
35		d_state(state),
36		d_im(im),
37	191	d_extensionality(userContext()),
38	382	d_uf_std_skolem(userContext())
39		{
40	191	d_true = NodeManager::currentNM()->mkConst(true);
41	191	}
42
43	284	Node HoExtension::ppRewrite(Node node)
44		{
45		// convert HO_APPLY to APPLY_UF if fully applied
46	284	if (node[0].getType().getNumChildren() == 2)
47		{
48	113	Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
49	226	Node ret = getApplyUfForHoApply(node);
50	226	Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
51	113	<< std::endl;
52	113	return ret;
53		}
54	171	return node;
55		}
56
57	866	Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
58		{
59	866	Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
60	866	Assert(deq[0][0].getType().isFunction());
61	866	if (isCached)
62		{
63	276	std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
64	276	if (it != d_extensionality_deq.end())
65		{
66		return it->second;
67		}
68		}
69	1732	TypeNode tn = deq[0][0].getType();
70	1732	std::vector<TypeNode> argTypes = tn.getArgTypes();
71	1732	std::vector<Node> skolems;
72	866	NodeManager* nm = NodeManager::currentNM();
73	866	SkolemManager* sm = nm->getSkolemManager();
74	1778	for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
75		{
76		Node k = sm->mkDummySkolem(
77	1824	"k", argTypes[i], "skolem created for extensionality.");
78	912	skolems.push_back(k);
79		}
80	1732	Node t[2];
81	2598	for (unsigned i = 0; i < 2; i++)
82		{
83	3464	std::vector<Node> children;
84	3464	Node curr = deq[0][i];
85	2838	while (curr.getKind() == HO_APPLY)
86		{
87	553	children.push_back(curr[1]);
88	553	curr = curr[0];
89		}
90	1732	children.push_back(curr);
91	1732	std::reverse(children.begin(), children.end());
92	1732	children.insert(children.end(), skolems.begin(), skolems.end());
93	1732	t[i] = nm->mkNode(APPLY_UF, children);
94		}
95	1732	Node conc = t[0].eqNode(t[1]).negate();
96	866	if (isCached)
97		{
98	276	d_extensionality_deq[deq] = conc;
99		}
100	866	return conc;
101		}
102
103	4035	unsigned HoExtension::applyExtensionality(TNode deq)
104		{
105	4035	Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
106	4035	Assert(deq[0][0].getType().isFunction());
107		// apply extensionality
108	4035	if (d_extensionality.find(deq) == d_extensionality.end())
109		{
110	276	d_extensionality.insert(deq);
111	552	Node conc = getExtensionalityDeq(deq);
112	552	Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
113	552	Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
114	276	<< std::endl;
115	276	d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
116	276	return 1;
117		}
118	3759	return 0;
119		}
120
121	113	Node HoExtension::getApplyUfForHoApply(Node node)
122		{
123	113	Assert(node[0].getType().getNumChildren() == 2);
124	226	std::vector<TNode> args;
125	226	Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
126	226	Node new_f = f;
127	113	NodeManager* nm = NodeManager::currentNM();
128	113	SkolemManager* sm = nm->getSkolemManager();
129	113	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	113	Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
192	113	args[0] = new_f;
193	113	Node ret = nm->mkNode(APPLY_UF, args);
194	113	Assert(ret.getType() == node.getType());
195	226	return ret;
196		}
197
198	1399	unsigned HoExtension::checkExtensionality(TheoryModel* m)
199		{
200	1399	eq::EqualityEngine* ee = d_state.getEqualityEngine();
201	1399	NodeManager* nm = NodeManager::currentNM();
202	1399	unsigned num_lemmas = 0;
203	1399	bool isCollectModel = (m != nullptr);
204	2798	Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
205	1399	<< isCollectModel << "..." << std::endl;
206	2798	std::map<TypeNode, std::vector<Node> > func_eqcs;
207	1399	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
208	1399	bool hasFunctions = false;
209	42215	while (!eqcs_i.isFinished())
210		{
211	40816	Node eqc = (*eqcs_i);
212	40816	TypeNode tn = eqc.getType();
213	20408	if (tn.isFunction())
214		{
215	4639	hasFunctions = true;
216		// if during collect model, must have an infinite type
217		// if not during collect model, must have a finite type
218	4639	if (d_state.isFiniteType(tn) != isCollectModel)
219		{
220	2142	func_eqcs[tn].push_back(eqc);
221	4284	Trace("uf-ho-debug")
222	2142	<< " func eqc : " << tn << " : " << eqc << std::endl;
223		}
224		}
225	20408	++eqcs_i;
226		}
227	1399	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	2663	for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
239	2663	itf != func_eqcs.end();
240		++itf)
241		{
242	3406	for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
243		{
244	3778	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	1636	if (!ee->areDisequal(itf->second[j], itf->second[k], false))
249		{
250		Node deq =
251	1580	Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
252		// either add to model, or add lemma
253	790	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	200	num_lemmas += applyExtensionality(deq);
285		}
286		}
287		}
288		}
289		}
290	1399	return num_lemmas;
291		}
292
293	682239	unsigned HoExtension::applyAppCompletion(TNode n)
294		{
295	682239	Assert(n.getKind() == APPLY_UF);
296
297	682239	eq::EqualityEngine* ee = d_state.getEqualityEngine();
298		// must expand into APPLY_HO version if not there already
299	1364478	Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
300	682239	if (!ee->hasTerm(ret) \|\| !ee->areEqual(ret, n))
301		{
302	25554	Node eq = n.eqNode(ret);
303	25554	Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
304	12777	<< std::endl;
305	25554	d_im.assertInternalFact(eq,
306		true,
307		InferenceId::UF_HO_APP_ENCODE,
308		PfRule::HO_APP_ENCODE,
309		{},
310	12777	{n});
311	12777	return 1;
312		}
313	1338924	Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "."
314	669462	<< std::endl;
315	669462	return 0;
316		}
317
318	13755	unsigned HoExtension::checkAppCompletion()
319		{
320	13755	Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
321		// compute the operators that are relevant (those for which an HO_APPLY exist)
322	27510	std::set<TNode> rlvOp;
323	13755	eq::EqualityEngine* ee = d_state.getEqualityEngine();
324	13755	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
325	27510	std::map<TNode, std::vector<Node> > apply_uf;
326	77853	while (!eqcs_i.isFinished())
327		{
328	76875	Node eqc = (*eqcs_i);
329	89652	Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc
330	44826	<< std::endl;
331	44826	eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
332	5090086	while (!eqc_i.isFinished())
333		{
334	5058037	Node n = *eqc_i;
335	2535407	if (n.getKind() == APPLY_UF \|\| n.getKind() == HO_APPLY)
336		{
337	1583192	int curr_sum = 0;
338	3153607	std::map<TNode, bool> curr_rops;
339	1583192	if (n.getKind() == APPLY_UF)
340		{
341	1814279	TNode rop = ee->getRepresentative(n.getOperator());
342	911037	if (rlvOp.find(rop) != rlvOp.end())
343		{
344		// try if its operator is relevant
345	370924	curr_sum = applyAppCompletion(n);
346	370924	if (curr_sum > 0)
347		{
348	7795	return curr_sum;
349		}
350		}
351		else
352		{
353		// add to pending list
354	540113	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	2702953	for (unsigned k = 0; k < n.getNumChildren(); k++)
359		{
360	1799711	if (n[k].getType().isFunction())
361		{
362	63754	TNode rop2 = ee->getRepresentative(n[k]);
363	31877	curr_rops[rop2] = true;
364		}
365		}
366		}
367		else
368		{
369	672155	Assert(n.getKind() == HO_APPLY);
370	1344310	TNode rop = ee->getRepresentative(n[0]);
371	672155	curr_rops[rop] = true;
372		}
373	2274375	for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
374	2274375	itc != curr_rops.end();
375		++itc)
376		{
377	1402938	TNode rop = itc->first;
378	703960	if (rlvOp.find(rop) == rlvOp.end())
379		{
380	47011	rlvOp.insert(rop);
381		// now, try each pending APPLY_UF for this operator
382		std::map<TNode, std::vector<Node> >::iterator itu =
383	47011	apply_uf.find(rop);
384	47011	if (itu != apply_uf.end())
385		{
386	327787	for (unsigned j = 0, size = itu->second.size(); j < size; j++)
387		{
388	311315	curr_sum = applyAppCompletion(itu->second[j]);
389	311315	if (curr_sum > 0)
390		{
391	4982	return curr_sum;
392		}
393		}
394		}
395		}
396		}
397		}
398	2522630	++eqc_i;
399		}
400	32049	++eqcs_i;
401		}
402	978	return 0;
403		}
404
405	1116	unsigned HoExtension::check()
406		{
407	1116	Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;
408
409		// infer new facts based on apply completion until fixed point
410		unsigned num_facts;
411	12639	do
412		{
413	13755	num_facts = checkAppCompletion();
414	13755	if (d_state.isInConflict())
415		{
416	138	Trace("uf-ho") << "...conflict during app-completion." << std::endl;
417	138	return 1;
418		}
419	13617	} while (num_facts > 0);
420
421	978	unsigned num_lemmas = 0;
422
423	978	num_lemmas = checkExtensionality();
424	978	if (num_lemmas > 0)
425		{
426	74	Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas."
427	37	<< std::endl;
428	37	return num_lemmas;
429		}
430
431	941	Trace("uf-ho") << "...finished check higher order." << std::endl;
432
433	941	return 0;
434		}
435
436	421	bool HoExtension::collectModelInfoHo(TheoryModel* m,
437		const std::set<Node>& termSet)
438		{
439	3782	for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
440		{
441	6722	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	3361	if (!collectModelInfoHoTerm(n, m))
446		{
447		return false;
448		}
449		}
450	421	int addedLemmas = checkExtensionality(m);
451	421	return addedLemmas == 0;
452		}
453
454	4541	bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
455		{
456	4541	if (n.getKind() == APPLY_UF)
457		{
458	4874	Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
459	2437	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	4541	return true;
469		}
470
471		} // namespace uf
472		} // namespace theory
473	29577	} // namespace cvc5