Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/trigger_database.cpp	Lines:	74	81	91.4 %
Date:	2021-09-30	Branches:	90	182	49.5 %


/******************************************************************************
 * 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(Env& env,
                                 QuantifiersState& qs,
                                 QuantifiersInferenceManager& qim,
                                 QuantifiersRegistry& qr,
                                 TermRegistry& tr)
    : EnvObj(env), 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_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
  }
  else
  {
    t = new Trigger(d_env, 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	4587	TriggerDatabase::TriggerDatabase(Env& env,
28		QuantifiersState& qs,
29		QuantifiersInferenceManager& qim,
30		QuantifiersRegistry& qr,
31	4587	TermRegistry& tr)
32	4587	: EnvObj(env), d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
33		{
34	4587	}
35	4584	TriggerDatabase::~TriggerDatabase() {}
36
37	6197	Trigger* TriggerDatabase::mkTrigger(Node q,
38		const std::vector<Node>& nodes,
39		bool keepAll,
40		int trOption,
41		size_t useNVars)
42		{
43	12394	std::vector<Node> trNodes;
44	6197	if (!keepAll)
45		{
46	4980	size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
47	4980	if (!mkTriggerTerms(q, nodes, nvars, trNodes))
48		{
49		return nullptr;
50		}
51		}
52		else
53		{
54	1217	trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
55		}
56
57		// check for duplicate?
58	6197	if (trOption != TR_MAKE_NEW)
59		{
60	4980	Trigger* t = d_trie.getTrigger(trNodes);
61	4980	if (t)
62		{
63	25	if (trOption == TR_GET_OLD)
64		{
65		// just return old trigger
66	25	return t;
67		}
68		return nullptr;
69		}
70		}
71
72		// check if higher-order
73	12344	Trace("trigger-debug") << "Collect higher-order variable triggers..."
74	6172	<< std::endl;
75	12344	std::map<Node, std::vector<Node> > hoApps;
76	6172	HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
77	12344	Trace("trigger-debug") << "...got " << hoApps.size()
78	6172	<< " higher-order applications." << std::endl;
79		Trigger* t;
80	6172	if (!hoApps.empty())
81		{
82	16	t = new HigherOrderTrigger(
83	8	d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
84		}
85		else
86		{
87	6164	t = new Trigger(d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes);
88		}
89	6172	d_trie.addTrigger(trNodes, t);
90	6172	return t;
91		}
92
93	4562	Trigger* TriggerDatabase::mkTrigger(
94		Node q, Node n, bool keepAll, int trOption, size_t useNVars)
95		{
96	9124	std::vector<Node> nodes;
97	4562	nodes.push_back(n);
98	9124	return mkTrigger(q, nodes, keepAll, trOption, useNVars);
99		}
100
101	4980	bool TriggerDatabase::mkTriggerTerms(Node q,
102		const std::vector<Node>& nodes,
103		size_t nvars,
104		std::vector<Node>& trNodes)
105		{
106		// only take nodes that contribute variables to the trigger when added
107	9960	std::map<Node, bool> vars;
108	9960	std::map<Node, std::vector<Node> > patterns;
109	4980	size_t varCount = 0;
110	9960	std::map<Node, std::vector<Node> > varContains;
111	11592	for (const Node& pat : nodes)
112		{
113	6612	TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
114		}
115	6110	for (const Node& t : nodes)
116		{
117	6110	const std::vector<Node>& vct = varContains[t];
118	6110	bool foundVar = false;
119	20344	for (const Node& v : vct)
120		{
121	14234	Assert(TermUtil::getInstConstAttr(v) == q);
122	14234	if (vars.find(v) == vars.end())
123		{
124	13052	varCount++;
125	13052	vars[v] = true;
126	13052	foundVar = true;
127		}
128		}
129	6110	if (foundVar)
130		{
131	5934	trNodes.push_back(t);
132	19760	for (const Node& v : vct)
133		{
134	13826	patterns[v].push_back(t);
135		}
136		}
137	6110	if (varCount == nvars)
138		{
139	4980	break;
140		}
141		}
142	4980	if (varCount < nvars)
143		{
144		Trace("trigger-debug") << "Don't consider trigger since it does not "
145		"contain specified number of variables."
146		<< std::endl;
147		Trace("trigger-debug") << nodes << std::endl;
148		// do not generate multi-trigger if it does not contain all variables
149		return false;
150		}
151		// now, minimize the trigger
152	11349	for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
153		{
154	6369	bool keepPattern = false;
155	12738	Node n = trNodes[i];
156	6369	const std::vector<Node>& vcn = varContains[n];
157	7044	for (const Node& v : vcn)
158		{
159	6609	if (patterns[v].size() == 1)
160		{
161	5934	keepPattern = true;
162	5934	break;
163		}
164		}
165	6369	if (!keepPattern)
166		{
167		// remove from pattern vector
168	1011	for (const Node& v : vcn)
169		{
170	576	std::vector<Node>& pv = patterns[v];
171	598	for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
172		{
173	598	if (pv[k] == n)
174		{
175	576	pv.erase(pv.begin() + k, pv.begin() + k + 1);
176	576	break;
177		}
178		}
179		}
180		// remove from trigger nodes
181	435	trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
182	435	i--;
183		}
184		}
185	4980	return true;
186		}
187
188		} // namespace inst
189		} // namespace quantifiers
190		} // namespace theory
191	22755	} // namespace cvc5