Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/trigger_database.cpp	Lines:	73	80	91.3 %
Date:	2021-08-06	Branches:	89	182	48.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Trigger database class.
 */

#include "theory/quantifiers/ematching/trigger_database.h"

#include "theory/quantifiers/ematching/ho_trigger.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/term_util.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {
namespace inst {

TriggerDatabase::TriggerDatabase(QuantifiersState& qs,
                                 QuantifiersInferenceManager& qim,
                                 QuantifiersRegistry& qr,
                                 TermRegistry& tr)
    : d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
{
}
TriggerDatabase::~TriggerDatabase() {}

Trigger* TriggerDatabase::mkTrigger(Node q,
                                    const std::vector<Node>& nodes,
                                    bool keepAll,
                                    int trOption,
                                    size_t useNVars)
{
  std::vector<Node> trNodes;
  if (!keepAll)
  {
    size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
    if (!mkTriggerTerms(q, nodes, nvars, trNodes))
    {
      return nullptr;
    }
  }
  else
  {
    trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
  }

  // check for duplicate?
  if (trOption != TR_MAKE_NEW)
  {
    Trigger* t = d_trie.getTrigger(trNodes);
    if (t)
    {
      if (trOption == TR_GET_OLD)
      {
        // just return old trigger
        return t;
      }
      return nullptr;
    }
  }

  // check if higher-order
  Trace("trigger-debug") << "Collect higher-order variable triggers..."
                         << std::endl;
  std::map<Node, std::vector<Node> > hoApps;
  HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
  Trace("trigger-debug") << "...got " << hoApps.size()
                         << " higher-order applications." << std::endl;
  Trigger* t;
  if (!hoApps.empty())
  {
    t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
  }
  else
  {
    t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes);
  }
  d_trie.addTrigger(trNodes, t);
  return t;
}

Trigger* TriggerDatabase::mkTrigger(
    Node q, Node n, bool keepAll, int trOption, size_t useNVars)
{
  std::vector<Node> nodes;
  nodes.push_back(n);
  return mkTrigger(q, nodes, keepAll, trOption, useNVars);
}

bool TriggerDatabase::mkTriggerTerms(Node q,
                                     const std::vector<Node>& nodes,
                                     size_t nvars,
                                     std::vector<Node>& trNodes)
{
  // only take nodes that contribute variables to the trigger when added
  std::map<Node, bool> vars;
  std::map<Node, std::vector<Node> > patterns;
  size_t varCount = 0;
  std::map<Node, std::vector<Node> > varContains;
  for (const Node& pat : nodes)
  {
    TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
  }
  for (const Node& t : nodes)
  {
    const std::vector<Node>& vct = varContains[t];
    bool foundVar = false;
    for (const Node& v : vct)
    {
      Assert(TermUtil::getInstConstAttr(v) == q);
      if (vars.find(v) == vars.end())
      {
        varCount++;
        vars[v] = true;
        foundVar = true;
      }
    }
    if (foundVar)
    {
      trNodes.push_back(t);
      for (const Node& v : vct)
      {
        patterns[v].push_back(t);
      }
    }
    if (varCount == nvars)
    {
      break;
    }
  }
  if (varCount < nvars)
  {
    Trace("trigger-debug") << "Don't consider trigger since it does not "
                              "contain specified number of variables."
                           << std::endl;
    Trace("trigger-debug") << nodes << std::endl;
    // do not generate multi-trigger if it does not contain all variables
    return false;
  }
  // now, minimize the trigger
  for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
  {
    bool keepPattern = false;
    Node n = trNodes[i];
    const std::vector<Node>& vcn = varContains[n];
    for (const Node& v : vcn)
    {
      if (patterns[v].size() == 1)
      {
        keepPattern = true;
        break;
      }
    }
    if (!keepPattern)
    {
      // remove from pattern vector
      for (const Node& v : vcn)
      {
        std::vector<Node>& pv = patterns[v];
        for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
        {
          if (pv[k] == n)
          {
            pv.erase(pv.begin() + k, pv.begin() + k + 1);
            break;
          }
        }
      }
      // remove from trigger nodes
      trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
      i--;
    }
  }
  return true;
}

}  // namespace inst
}  // 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, Morgan Deters
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		* Trigger database class.
14		*/
15
16		#include "theory/quantifiers/ematching/trigger_database.h"
17
18		#include "theory/quantifiers/ematching/ho_trigger.h"
19		#include "theory/quantifiers/ematching/trigger.h"
20		#include "theory/quantifiers/term_util.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace quantifiers {
25		namespace inst {
26
27	6503	TriggerDatabase::TriggerDatabase(QuantifiersState& qs,
28		QuantifiersInferenceManager& qim,
29		QuantifiersRegistry& qr,
30	6503	TermRegistry& tr)
31	6503	: d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
32		{
33	6503	}
34	6503	TriggerDatabase::~TriggerDatabase() {}
35
36	16889	Trigger* TriggerDatabase::mkTrigger(Node q,
37		const std::vector<Node>& nodes,
38		bool keepAll,
39		int trOption,
40		size_t useNVars)
41		{
42	33778	std::vector<Node> trNodes;
43	16889	if (!keepAll)
44		{
45	12849	size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
46	12849	if (!mkTriggerTerms(q, nodes, nvars, trNodes))
47		{
48		return nullptr;
49		}
50		}
51		else
52		{
53	4040	trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
54		}
55
56		// check for duplicate?
57	16889	if (trOption != TR_MAKE_NEW)
58		{
59	12849	Trigger* t = d_trie.getTrigger(trNodes);
60	12849	if (t)
61		{
62	39	if (trOption == TR_GET_OLD)
63		{
64		// just return old trigger
65	39	return t;
66		}
67		return nullptr;
68		}
69		}
70
71		// check if higher-order
72	33700	Trace("trigger-debug") << "Collect higher-order variable triggers..."
73	16850	<< std::endl;
74	33700	std::map<Node, std::vector<Node> > hoApps;
75	16850	HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
76	33700	Trace("trigger-debug") << "...got " << hoApps.size()
77	16850	<< " higher-order applications." << std::endl;
78		Trigger* t;
79	16850	if (!hoApps.empty())
80		{
81	36	t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
82		}
83		else
84		{
85	16814	t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes);
86		}
87	16850	d_trie.addTrigger(trNodes, t);
88	16850	return t;
89		}
90
91	11811	Trigger* TriggerDatabase::mkTrigger(
92		Node q, Node n, bool keepAll, int trOption, size_t useNVars)
93		{
94	23622	std::vector<Node> nodes;
95	11811	nodes.push_back(n);
96	23622	return mkTrigger(q, nodes, keepAll, trOption, useNVars);
97		}
98
99	12849	bool TriggerDatabase::mkTriggerTerms(Node q,
100		const std::vector<Node>& nodes,
101		size_t nvars,
102		std::vector<Node>& trNodes)
103		{
104		// only take nodes that contribute variables to the trigger when added
105	25698	std::map<Node, bool> vars;
106	25698	std::map<Node, std::vector<Node> > patterns;
107	12849	size_t varCount = 0;
108	25698	std::map<Node, std::vector<Node> > varContains;
109	29670	for (const Node& pat : nodes)
110		{
111	16821	TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
112		}
113	15704	for (const Node& t : nodes)
114		{
115	15704	const std::vector<Node>& vct = varContains[t];
116	15704	bool foundVar = false;
117	53017	for (const Node& v : vct)
118		{
119	37313	Assert(TermUtil::getInstConstAttr(v) == q);
120	37313	if (vars.find(v) == vars.end())
121		{
122	34270	varCount++;
123	34270	vars[v] = true;
124	34270	foundVar = true;
125		}
126		}
127	15704	if (foundVar)
128		{
129	15231	trNodes.push_back(t);
130	51443	for (const Node& v : vct)
131		{
132	36212	patterns[v].push_back(t);
133		}
134		}
135	15704	if (varCount == nvars)
136		{
137	12849	break;
138		}
139		}
140	12849	if (varCount < nvars)
141		{
142		Trace("trigger-debug") << "Don't consider trigger since it does not "
143		"contain specified number of variables."
144		<< std::endl;
145		Trace("trigger-debug") << nodes << std::endl;
146		// do not generate multi-trigger if it does not contain all variables
147		return false;
148		}
149		// now, minimize the trigger
150	29155	for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
151		{
152	16306	bool keepPattern = false;
153	32612	Node n = trNodes[i];
154	16306	const std::vector<Node>& vcn = varContains[n];
155	18037	for (const Node& v : vcn)
156		{
157	16962	if (patterns[v].size() == 1)
158		{
159	15231	keepPattern = true;
160	15231	break;
161		}
162		}
163	16306	if (!keepPattern)
164		{
165		// remove from pattern vector
166	2520	for (const Node& v : vcn)
167		{
168	1445	std::vector<Node>& pv = patterns[v];
169	1505	for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
170		{
171	1505	if (pv[k] == n)
172		{
173	1445	pv.erase(pv.begin() + k, pv.begin() + k + 1);
174	1445	break;
175		}
176		}
177		}
178		// remove from trigger nodes
179	1075	trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
180	1075	i--;
181		}
182		}
183	12849	return true;
184		}
185
186		} // namespace inst
187		} // namespace quantifiers
188		} // namespace theory
189	29322	} // namespace cvc5