Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/trigger_database.cpp	Lines:	74	81	91.4 %
Date:	2021-11-07	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	11880	TriggerDatabase::TriggerDatabase(Env& env,
28		QuantifiersState& qs,
29		QuantifiersInferenceManager& qim,
30		QuantifiersRegistry& qr,
31	11880	TermRegistry& tr)
32	11880	: EnvObj(env), d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
33		{
34	11880	}
35	11875	TriggerDatabase::~TriggerDatabase() {}
36
37	17792	Trigger* TriggerDatabase::mkTrigger(Node q,
38		const std::vector<Node>& nodes,
39		bool keepAll,
40		int trOption,
41		size_t useNVars)
42		{
43	35584	std::vector<Node> trNodes;
44	17792	if (!keepAll)
45		{
46	13915	size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
47	13915	if (!mkTriggerTerms(q, nodes, nvars, trNodes))
48		{
49		return nullptr;
50		}
51		}
52		else
53		{
54	3877	trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
55		}
56
57		// check for duplicate?
58	17792	if (trOption != TR_MAKE_NEW)
59		{
60	13915	Trigger* t = d_trie.getTrigger(trNodes);
61	13915	if (t)
62		{
63	89	if (trOption == TR_GET_OLD)
64		{
65		// just return old trigger
66	89	return t;
67		}
68		return nullptr;
69		}
70		}
71
72		// check if higher-order
73	35406	Trace("trigger-debug") << "Collect higher-order variable triggers..."
74	17703	<< std::endl;
75	35406	std::map<Node, std::vector<Node> > hoApps;
76	17703	HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
77	35406	Trace("trigger-debug") << "...got " << hoApps.size()
78	17703	<< " higher-order applications." << std::endl;
79		Trigger* t;
80	17703	if (!hoApps.empty())
81		{
82	72	t = new HigherOrderTrigger(
83	36	d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
84		}
85		else
86		{
87	17667	t = new Trigger(d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes);
88		}
89	17703	d_trie.addTrigger(trNodes, t);
90	17703	return t;
91		}
92
93	12742	Trigger* TriggerDatabase::mkTrigger(
94		Node q, Node n, bool keepAll, int trOption, size_t useNVars)
95		{
96	25484	std::vector<Node> nodes;
97	12742	nodes.push_back(n);
98	25484	return mkTrigger(q, nodes, keepAll, trOption, useNVars);
99		}
100
101	13915	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	27830	std::map<Node, bool> vars;
108	27830	std::map<Node, std::vector<Node> > patterns;
109	13915	size_t varCount = 0;
110	27830	std::map<Node, std::vector<Node> > varContains;
111	32329	for (const Node& pat : nodes)
112		{
113	18414	TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
114		}
115	17053	for (const Node& t : nodes)
116		{
117	17053	const std::vector<Node>& vct = varContains[t];
118	17053	bool foundVar = false;
119	57329	for (const Node& v : vct)
120		{
121	40276	Assert(TermUtil::getInstConstAttr(v) == q);
122	40276	if (vars.find(v) == vars.end())
123		{
124	36988	varCount++;
125	36988	vars[v] = true;
126	36988	foundVar = true;
127		}
128		}
129	17053	if (foundVar)
130		{
131	16568	trNodes.push_back(t);
132	55719	for (const Node& v : vct)
133		{
134	39151	patterns[v].push_back(t);
135		}
136		}
137	17053	if (varCount == nvars)
138		{
139	13915	break;
140		}
141		}
142	13915	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	31664	for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
153		{
154	17749	bool keepPattern = false;
155	35498	Node n = trNodes[i];
156	17749	const std::vector<Node>& vcn = varContains[n];
157	19628	for (const Node& v : vcn)
158		{
159	18447	if (patterns[v].size() == 1)
160		{
161	16568	keepPattern = true;
162	16568	break;
163		}
164		}
165	17749	if (!keepPattern)
166		{
167		// remove from pattern vector
168	2750	for (const Node& v : vcn)
169		{
170	1569	std::vector<Node>& pv = patterns[v];
171	1631	for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
172		{
173	1631	if (pv[k] == n)
174		{
175	1569	pv.erase(pv.begin() + k, pv.begin() + k + 1);
176	1569	break;
177		}
178		}
179		}
180		// remove from trigger nodes
181	1181	trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
182	1181	i--;
183		}
184		}
185	13915	return true;
186		}
187
188		} // namespace inst
189		} // namespace quantifiers
190		} // namespace theory
191	31137	} // namespace cvc5