Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ho_term_database.cpp	Lines:	106	121	87.6 %
Date:	2021-09-16	Branches:	202	430	47.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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 higher-order term database class.
 */

#include "theory/quantifiers/ho_term_database.h"

#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/rewriter.h"
#include "theory/uf/equality_engine.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
    : TermDb(env, qs, qr)
{
}

HoTermDb::~HoTermDb() {}

void HoTermDb::addTermInternal(Node n)
{
  if (n.getType().isFunction())
  {
    // nothing special to do with functions
    return;
  }
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node curr = n;
  std::vector<Node> args;
  while (curr.getKind() == HO_APPLY)
  {
    args.insert(args.begin(), curr[1]);
    curr = curr[0];
    if (!curr.isVar())
    {
      // purify the term
      std::map<Node, Node>::iterator itp = d_hoFunOpPurify.find(curr);
      Node psk;
      if (itp == d_hoFunOpPurify.end())
      {
        psk = sm->mkPurifySkolem(
            curr, "pfun", "purify for function operator term indexing");
        d_hoFunOpPurify[curr] = psk;
        // we do not add it to d_ops since it is an internal operator
      }
      else
      {
        psk = itp->second;
      }
      std::vector<Node> children;
      children.push_back(psk);
      children.insert(children.end(), args.begin(), args.end());
      Node p_n = nm->mkNode(APPLY_UF, children);
      Trace("term-db") << "register term in db (via purify) " << p_n
                       << std::endl;
      // also add this one internally
      DbList* dblp = getOrMkDbListForOp(psk);
      dblp->d_list.push_back(p_n);
      // maintain backwards mapping
      d_hoPurifyToTerm[p_n] = n;
    }
  }
  if (!args.empty() && curr.isVar())
  {
    // also add standard application version
    args.insert(args.begin(), curr);
    Node uf_n = nm->mkNode(APPLY_UF, args);
    addTerm(uf_n);
  }
}

void HoTermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
{
  ops.push_back(f);
  ops.insert(ops.end(), d_hoOpSlaves[f].begin(), d_hoOpSlaves[f].end());
}

Node HoTermDb::getOperatorRepresentative(TNode op) const
{
  std::map<TNode, TNode>::const_iterator it = d_hoOpRep.find(op);
  if (it != d_hoOpRep.end())
  {
    return it->second;
  }
  return op;
}

bool HoTermDb::resetInternal(Theory::Effort effort)
{
  Trace("quant-ho")
      << "HoTermDb::reset : assert higher-order purify equalities..."
      << std::endl;
  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
  for (std::pair<const Node, Node>& pp : d_hoPurifyToTerm)
  {
    if (ee->hasTerm(pp.second)
        && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
    {
      Node eq;
      std::map<Node, Node>::iterator itpe = d_hoPurifyToEq.find(pp.first);
      if (itpe == d_hoPurifyToEq.end())
      {
        eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
        d_hoPurifyToEq[pp.first] = eq;
      }
      else
      {
        eq = itpe->second;
      }
      Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
      // Note that ee may be the central equality engine, in which case this
      // equality is explained trivially with "true", since both sides of
      // eq are HOL and FOL encodings of the same thing.
      ee->assertEquality(eq, true, d_true);
      if (!ee->consistent())
      {
        // In some rare cases, purification functions (in the domain of
        // d_hoPurifyToTerm) may escape the term database. For example,
        // matching algorithms may construct instantiations involving these
        // functions. As a result, asserting these equalities internally may
        // cause a conflict. In this case, we insist that the purification
        // equality is sent out as a lemma here.
        Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl;
        d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY);
        d_qstate.notifyInConflict();
        d_consistent_ee = false;
        return false;
      }
    }
  }
  return true;
}

bool HoTermDb::finishResetInternal(Theory::Effort effort)
{
  if (!options().quantifiers.hoMergeTermDb)
  {
    return true;
  }
  Trace("quant-ho") << "HoTermDb::reset : compute equal functions..."
                    << std::endl;
  // build operator representative map
  d_hoOpRep.clear();
  d_hoOpSlaves.clear();
  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
  while (!eqcs_i.isFinished())
  {
    TNode r = (*eqcs_i);
    if (r.getType().isFunction())
    {
      Trace("quant-ho") << "  process function eqc " << r << std::endl;
      Node first;
      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
      while (!eqc_i.isFinished())
      {
        TNode n = (*eqc_i);
        Node n_use;
        if (n.isVar())
        {
          n_use = n;
        }
        else
        {
          // use its purified variable, if it exists
          std::map<Node, Node>::iterator itp = d_hoFunOpPurify.find(n);
          if (itp != d_hoFunOpPurify.end())
          {
            n_use = itp->second;
          }
        }
        Trace("quant-ho") << "  - process " << n_use << ", from " << n
                          << std::endl;
        if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end())
        {
          if (first.isNull())
          {
            first = n_use;
            d_hoOpRep[n_use] = n_use;
          }
          else
          {
            Trace("quant-ho") << "  have : " << n_use << " == " << first
                              << ", type = " << n_use.getType() << std::endl;
            d_hoOpRep[n_use] = first;
            d_hoOpSlaves[first].push_back(n_use);
          }
        }
        ++eqc_i;
      }
    }
    ++eqcs_i;
  }
  Trace("quant-ho") << "...finished compute equal functions." << std::endl;

  return true;
}
bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
{
  if (!d_qstate.areDisequal(a, b))
  {
    return false;
  }
  exp.push_back(a.eqNode(b));
  // operators might be disequal
  Node af = getMatchOperator(a);
  Node bf = getMatchOperator(b);
  if (af != bf)
  {
    if (a.getKind() == APPLY_UF && b.getKind() == APPLY_UF)
    {
      exp.push_back(af.eqNode(bf).negate());
    }
    else
    {
      Assert(false);
      return false;
    }
  }
  return true;
}

Node HoTermDb::getHoTypeMatchPredicate(TypeNode tn)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
  return sm->mkSkolemFunction(SkolemFunId::HO_TYPE_MATCH_PRED, ptn);
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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 higher-order term database class.
14		*/
15
16		#include "theory/quantifiers/ho_term_database.h"
17
18		#include "expr/skolem_manager.h"
19		#include "options/quantifiers_options.h"
20		#include "theory/quantifiers/quantifiers_inference_manager.h"
21		#include "theory/quantifiers/quantifiers_state.h"
22		#include "theory/rewriter.h"
23		#include "theory/uf/equality_engine.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30
31	191	HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
32	191	: TermDb(env, qs, qr)
33		{
34	191	}
35
36	380	HoTermDb::~HoTermDb() {}
37
38	42287	void HoTermDb::addTermInternal(Node n)
39		{
40	42287	if (n.getType().isFunction())
41		{
42		// nothing special to do with functions
43	437	return;
44		}
45	41850	NodeManager* nm = NodeManager::currentNM();
46	41850	SkolemManager* sm = nm->getSkolemManager();
47	83700	Node curr = n;
48	83700	std::vector<Node> args;
49	92366	while (curr.getKind() == HO_APPLY)
50		{
51	25258	args.insert(args.begin(), curr[1]);
52	25258	curr = curr[0];
53	25258	if (!curr.isVar())
54		{
55		// purify the term
56	12485	std::map<Node, Node>::iterator itp = d_hoFunOpPurify.find(curr);
57	24970	Node psk;
58	12485	if (itp == d_hoFunOpPurify.end())
59		{
60	197	psk = sm->mkPurifySkolem(
61		curr, "pfun", "purify for function operator term indexing");
62	197	d_hoFunOpPurify[curr] = psk;
63		// we do not add it to d_ops since it is an internal operator
64		}
65		else
66		{
67	12288	psk = itp->second;
68		}
69	24970	std::vector<Node> children;
70	12485	children.push_back(psk);
71	12485	children.insert(children.end(), args.begin(), args.end());
72	24970	Node p_n = nm->mkNode(APPLY_UF, children);
73	24970	Trace("term-db") << "register term in db (via purify) " << p_n
74	12485	<< std::endl;
75		// also add this one internally
76	12485	DbList* dblp = getOrMkDbListForOp(psk);
77	12485	dblp->d_list.push_back(p_n);
78		// maintain backwards mapping
79	12485	d_hoPurifyToTerm[p_n] = n;
80		}
81		}
82	41850	if (!args.empty() && curr.isVar())
83		{
84		// also add standard application version
85	12773	args.insert(args.begin(), curr);
86	25546	Node uf_n = nm->mkNode(APPLY_UF, args);
87	12773	addTerm(uf_n);
88		}
89		}
90
91	3030	void HoTermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
92		{
93	3030	ops.push_back(f);
94	3030	ops.insert(ops.end(), d_hoOpSlaves[f].begin(), d_hoOpSlaves[f].end());
95	3030	}
96
97	497592	Node HoTermDb::getOperatorRepresentative(TNode op) const
98		{
99	497592	std::map<TNode, TNode>::const_iterator it = d_hoOpRep.find(op);
100	497592	if (it != d_hoOpRep.end())
101		{
102	479430	return it->second;
103		}
104	18162	return op;
105		}
106
107	934	bool HoTermDb::resetInternal(Theory::Effort effort)
108		{
109	1868	Trace("quant-ho")
110	934	<< "HoTermDb::reset : assert higher-order purify equalities..."
111	934	<< std::endl;
112	934	eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
113	12286	for (std::pair<const Node, Node>& pp : d_hoPurifyToTerm)
114		{
115	34056	if (ee->hasTerm(pp.second)
116	34056	&& (!ee->hasTerm(pp.first) \|\| !ee->areEqual(pp.second, pp.first)))
117		{
118	15050	Node eq;
119	7525	std::map<Node, Node>::iterator itpe = d_hoPurifyToEq.find(pp.first);
120	7525	if (itpe == d_hoPurifyToEq.end())
121		{
122	542	eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
123	542	d_hoPurifyToEq[pp.first] = eq;
124		}
125		else
126		{
127	6983	eq = itpe->second;
128		}
129	7525	Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
130		// Note that ee may be the central equality engine, in which case this
131		// equality is explained trivially with "true", since both sides of
132		// eq are HOL and FOL encodings of the same thing.
133	7525	ee->assertEquality(eq, true, d_true);
134	7525	if (!ee->consistent())
135		{
136		// In some rare cases, purification functions (in the domain of
137		// d_hoPurifyToTerm) may escape the term database. For example,
138		// matching algorithms may construct instantiations involving these
139		// functions. As a result, asserting these equalities internally may
140		// cause a conflict. In this case, we insist that the purification
141		// equality is sent out as a lemma here.
142		Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl;
143		d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY);
144		d_qstate.notifyInConflict();
145		d_consistent_ee = false;
146		return false;
147		}
148		}
149		}
150	934	return true;
151		}
152
153	934	bool HoTermDb::finishResetInternal(Theory::Effort effort)
154		{
155	934	if (!options().quantifiers.hoMergeTermDb)
156		{
157		return true;
158		}
159	1868	Trace("quant-ho") << "HoTermDb::reset : compute equal functions..."
160	934	<< std::endl;
161		// build operator representative map
162	934	d_hoOpRep.clear();
163	934	d_hoOpSlaves.clear();
164	934	eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
165	934	eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
166	88628	while (!eqcs_i.isFinished())
167		{
168	87694	TNode r = (*eqcs_i);
169	43847	if (r.getType().isFunction())
170		{
171	3637	Trace("quant-ho") << " process function eqc " << r << std::endl;
172	7274	Node first;
173	3637	eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
174	14479	while (!eqc_i.isFinished())
175		{
176	10842	TNode n = (*eqc_i);
177	10842	Node n_use;
178	5421	if (n.isVar())
179		{
180	3849	n_use = n;
181		}
182		else
183		{
184		// use its purified variable, if it exists
185	1572	std::map<Node, Node>::iterator itp = d_hoFunOpPurify.find(n);
186	1572	if (itp != d_hoFunOpPurify.end())
187		{
188	1499	n_use = itp->second;
189		}
190		}
191	10842	Trace("quant-ho") << " - process " << n_use << ", from " << n
192	5421	<< std::endl;
193	5421	if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end())
194		{
195	4627	if (first.isNull())
196		{
197	3230	first = n_use;
198	3230	d_hoOpRep[n_use] = n_use;
199		}
200		else
201		{
202	2794	Trace("quant-ho") << " have : " << n_use << " == " << first
203	1397	<< ", type = " << n_use.getType() << std::endl;
204	1397	d_hoOpRep[n_use] = first;
205	1397	d_hoOpSlaves[first].push_back(n_use);
206		}
207		}
208	5421	++eqc_i;
209		}
210		}
211	43847	++eqcs_i;
212		}
213	934	Trace("quant-ho") << "...finished compute equal functions." << std::endl;
214
215	934	return true;
216		}
217	8052	bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
218		{
219	8052	if (!d_qstate.areDisequal(a, b))
220		{
221	8052	return false;
222		}
223		exp.push_back(a.eqNode(b));
224		// operators might be disequal
225		Node af = getMatchOperator(a);
226		Node bf = getMatchOperator(b);
227		if (af != bf)
228		{
229		if (a.getKind() == APPLY_UF && b.getKind() == APPLY_UF)
230		{
231		exp.push_back(af.eqNode(bf).negate());
232		}
233		else
234		{
235		Assert(false);
236		return false;
237		}
238		}
239		return true;
240		}
241
242	268	Node HoTermDb::getHoTypeMatchPredicate(TypeNode tn)
243		{
244	268	NodeManager* nm = NodeManager::currentNM();
245	268	SkolemManager* sm = nm->getSkolemManager();
246	536	TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
247	536	return sm->mkSkolemFunction(SkolemFunId::HO_TYPE_MATCH_PRED, ptn);
248		}
249
250		} // namespace quantifiers
251		} // namespace theory
252	29577	} // namespace cvc5