Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/inst_match_generator_multi.cpp	Lines:	132	140	94.3 %
Date:	2021-09-29	Branches:	207	392	52.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Multi inst match generator class.
 */

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

#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_util.h"
#include "theory/uf/equality_engine_iterator.h"

using namespace cvc5::kind;

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

InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
                                                 Node q,
                                                 std::vector<Node>& pats)
    : IMGenerator(tparent), d_quant(q)
{
  Trace("multi-trigger-cache")
      << "Making smart multi-trigger for " << q << std::endl;
  std::map<Node, std::vector<Node> > var_contains;
  for (const Node& pat : pats)
  {
    TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
  }
  // convert to indicies
  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
  {
    Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
    for (const Node& vcn : vc.second)
    {
      Trace("multi-trigger-cache") << vcn << " ";
      uint64_t index = vcn.getAttribute(InstVarNumAttribute());
      d_var_contains[vc.first].push_back(index);
      d_var_to_node[index].push_back(vc.first);
    }
    Trace("multi-trigger-cache") << std::endl;
  }
  size_t patsSize = pats.size();
  for (size_t i = 0; i < patsSize; i++)
  {
    Node n = pats[i];
    // make the match generator
    InstMatchGenerator* img =
        InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
    img->setActiveAdd(false);
    d_children.push_back(img);
    // compute unique/shared variables
    std::vector<uint64_t> unique_vars;
    std::map<uint64_t, bool> shared_vars;
    unsigned numSharedVars = 0;
    std::vector<uint64_t>& vctn = d_var_contains[n];
    for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
    {
      if (d_var_to_node[vctn[j]].size() == 1)
      {
        Trace("multi-trigger-cache")
            << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
        unique_vars.push_back(vctn[j]);
      }
      else
      {
        shared_vars[vctn[j]] = true;
        numSharedVars++;
      }
    }
    // we use the latest shared variables, then unique variables
    std::vector<uint64_t> vars;
    size_t index = i == 0 ? pats.size() - 1 : (i - 1);
    while (numSharedVars > 0 && index != i)
    {
      for (std::pair<const uint64_t, bool>& sv : shared_vars)
      {
        if (sv.second)
        {
          std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
          if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
          {
            vars.push_back(sv.first);
            shared_vars[sv.first] = false;
            numSharedVars--;
          }
        }
      }
      index = index == 0 ? patsSize - 1 : (index - 1);
    }
    vars.insert(vars.end(), unique_vars.begin(), unique_vars.end());
    if (Trace.isOn("multi-trigger-cache"))
    {
      Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
      for (uint64_t v : vars)
      {
        Trace("multi-trigger-cache") << v << " ";
      }
      Trace("multi-trigger-cache") << std::endl;
    }
    // make ordered inst match trie
    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
    d_imtio[i]->d_order.insert(
        d_imtio[i]->d_order.begin(), vars.begin(), vars.end());
    d_children_trie.push_back(InstMatchTrieOrdered(d_imtio[i]));
  }
}

InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
{
  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
  {
    delete d_children[i];
  }
  for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
  {
    delete i.second;
  }
}

/** reset instantiation round (call this whenever equivalence classes have
 * changed) */
void InstMatchGeneratorMulti::resetInstantiationRound()
{
  for (InstMatchGenerator* c : d_children)
  {
    c->resetInstantiationRound();
  }
}

/** reset, eqc is the equivalence class to search in (any if eqc=null) */
bool InstMatchGeneratorMulti::reset(Node eqc)
{
  for (InstMatchGenerator* c : d_children)
  {
    if (!c->reset(eqc))
    {
      // do not return false here
    }
  }
  return true;
}

uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
{
  uint64_t addedLemmas = 0;
  Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
  {
    Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
    std::vector<InstMatch> newMatches;
    InstMatch m(q);
    while (d_children[i]->getNextMatch(q, m) > 0)
    {
      // m.makeRepresentative( qe );
      newMatches.push_back(InstMatch(&m));
      m.clear();
    }
    Trace("multi-trigger-cache") << "Made " << newMatches.size()
                                 << " new matches for index " << i << std::endl;
    for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
    {
      Trace("multi-trigger-cache2")
          << "...processing " << j << " / " << newMatches.size()
          << ", #lemmas = " << addedLemmas << std::endl;
      processNewMatch(newMatches[j], i, addedLemmas);
      if (d_qstate.isInConflict())
      {
        return addedLemmas;
      }
    }
  }
  return addedLemmas;
}

void InstMatchGeneratorMulti::processNewMatch(InstMatch& m,
                                              size_t fromChildIndex,
                                              uint64_t& addedLemmas)
{
  // see if these produce new matches
  d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.d_vals);
  // possibly only do the following if we know that new matches will be
  // produced? the issue is that instantiations are filtered in quantifiers
  // engine, and so there is no guarentee that
  // we can safely skip the following lines, even when we have already produced
  // this match.
  Trace("multi-trigger-cache-debug")
      << "Child " << fromChildIndex << " produced match " << m << std::endl;
  // process new instantiations
  size_t childIndex = (fromChildIndex + 1) % d_children.size();
  processNewInstantiations(m,
                           addedLemmas,
                           d_children_trie[childIndex].getTrie(),
                           0,
                           childIndex,
                           fromChildIndex,
                           true);
}

void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
                                                       uint64_t& addedLemmas,
                                                       InstMatchTrie* tr,
                                                       size_t trieIndex,
                                                       size_t childIndex,
                                                       size_t endChildIndex,
                                                       bool modEq)
{
  Assert(!d_qstate.isInConflict());
  if (childIndex == endChildIndex)
  {
    // m is an instantiation
    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
    {
      addedLemmas++;
      Trace("multi-trigger-cache-debug")
          << "-> Produced instantiation " << m << std::endl;
    }
    return;
  }
  InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
  if (trieIndex < iio->d_order.size())
  {
    size_t curr_index = iio->d_order[trieIndex];
    Node n = m.get(curr_index);
    if (n.isNull())
    {
      // add to InstMatch
      for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
      {
        InstMatch mn(&m);
        mn.setValue(curr_index, d.first);
        processNewInstantiations(mn,
                                 addedLemmas,
                                 &(d.second),
                                 trieIndex + 1,
                                 childIndex,
                                 endChildIndex,
                                 modEq);
        if (d_qstate.isInConflict())
        {
          break;
        }
      }
    }
    // shared and set variable, try to merge
    std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
    if (it != tr->d_data.end())
    {
      processNewInstantiations(m,
                               addedLemmas,
                               &(it->second),
                               trieIndex + 1,
                               childIndex,
                               endChildIndex,
                               modEq);
    }
    if (!modEq)
    {
      return;
    }
    QuantifiersState& qs = d_qstate;
    // check modulo equality for other possible instantiations
    if (!qs.hasTerm(n))
    {
      return;
    }
    eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
    while (!eqc.isFinished())
    {
      Node en = (*eqc);
      if (en != n)
      {
        std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
        if (itc != tr->d_data.end())
        {
          processNewInstantiations(m,
                                   addedLemmas,
                                   &(itc->second),
                                   trieIndex + 1,
                                   childIndex,
                                   endChildIndex,
                                   modEq);
          if (d_qstate.isInConflict())
          {
            break;
          }
        }
      }
      ++eqc;
    }
  }
  else
  {
    size_t newChildIndex = (childIndex + 1) % d_children.size();
    processNewInstantiations(m,
                             addedLemmas,
                             d_children_trie[newChildIndex].getTrie(),
                             0,
                             newChildIndex,
                             endChildIndex,
                             modEq);
  }
}

}  // 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, Tim King
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		* Multi inst match generator class.
14		*/
15
16		#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
17
18		#include "theory/quantifiers/quantifiers_state.h"
19		#include "theory/quantifiers/term_util.h"
20		#include "theory/uf/equality_engine_iterator.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27		namespace inst {
28
29	3	InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
30		Node q,
31	3	std::vector<Node>& pats)
32	3	: IMGenerator(tparent), d_quant(q)
33		{
34	6	Trace("multi-trigger-cache")
35	3	<< "Making smart multi-trigger for " << q << std::endl;
36	6	std::map<Node, std::vector<Node> > var_contains;
37	10	for (const Node& pat : pats)
38		{
39	7	TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
40		}
41		// convert to indicies
42	10	for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
43		{
44	7	Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
45	34	for (const Node& vcn : vc.second)
46		{
47	27	Trace("multi-trigger-cache") << vcn << " ";
48	27	uint64_t index = vcn.getAttribute(InstVarNumAttribute());
49	27	d_var_contains[vc.first].push_back(index);
50	27	d_var_to_node[index].push_back(vc.first);
51		}
52	7	Trace("multi-trigger-cache") << std::endl;
53		}
54	3	size_t patsSize = pats.size();
55	10	for (size_t i = 0; i < patsSize; i++)
56		{
57	14	Node n = pats[i];
58		// make the match generator
59		InstMatchGenerator* img =
60	7	InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
61	7	img->setActiveAdd(false);
62	7	d_children.push_back(img);
63		// compute unique/shared variables
64	14	std::vector<uint64_t> unique_vars;
65	14	std::map<uint64_t, bool> shared_vars;
66	7	unsigned numSharedVars = 0;
67	7	std::vector<uint64_t>& vctn = d_var_contains[n];
68	34	for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
69		{
70	27	if (d_var_to_node[vctn[j]].size() == 1)
71		{
72	36	Trace("multi-trigger-cache")
73	18	<< "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
74	18	unique_vars.push_back(vctn[j]);
75		}
76		else
77		{
78	9	shared_vars[vctn[j]] = true;
79	9	numSharedVars++;
80		}
81		}
82		// we use the latest shared variables, then unique variables
83	14	std::vector<uint64_t> vars;
84	7	size_t index = i == 0 ? pats.size() - 1 : (i - 1);
85	23	while (numSharedVars > 0 && index != i)
86		{
87	19	for (std::pair<const uint64_t, bool>& sv : shared_vars)
88		{
89	11	if (sv.second)
90		{
91	10	std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
92	10	if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
93		{
94	9	vars.push_back(sv.first);
95	9	shared_vars[sv.first] = false;
96	9	numSharedVars--;
97		}
98		}
99		}
100	8	index = index == 0 ? patsSize - 1 : (index - 1);
101		}
102	7	vars.insert(vars.end(), unique_vars.begin(), unique_vars.end());
103	7	if (Trace.isOn("multi-trigger-cache"))
104		{
105		Trace("multi-trigger-cache") << " Index[" << i << "]: ";
106		for (uint64_t v : vars)
107		{
108		Trace("multi-trigger-cache") << v << " ";
109		}
110		Trace("multi-trigger-cache") << std::endl;
111		}
112		// make ordered inst match trie
113	7	d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
114	14	d_imtio[i]->d_order.insert(
115	14	d_imtio[i]->d_order.begin(), vars.begin(), vars.end());
116	7	d_children_trie.push_back(InstMatchTrieOrdered(d_imtio[i]));
117		}
118	3	}
119
120	9	InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
121		{
122	10	for (size_t i = 0, csize = d_children.size(); i < csize; i++)
123		{
124	7	delete d_children[i];
125		}
126	10	for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
127		{
128	7	delete i.second;
129		}
130	6	}
131
132		/** reset instantiation round (call this whenever equivalence classes have
133		* changed) */
134	20	void InstMatchGeneratorMulti::resetInstantiationRound()
135		{
136	64	for (InstMatchGenerator* c : d_children)
137		{
138	44	c->resetInstantiationRound();
139		}
140	20	}
141
142		/** reset, eqc is the equivalence class to search in (any if eqc=null) */
143	20	bool InstMatchGeneratorMulti::reset(Node eqc)
144		{
145	64	for (InstMatchGenerator* c : d_children)
146		{
147	44	if (!c->reset(eqc))
148		{
149		// do not return false here
150		}
151		}
152	20	return true;
153		}
154
155	12	uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
156		{
157	12	uint64_t addedLemmas = 0;
158	12	Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
159	39	for (size_t i = 0, csize = d_children.size(); i < csize; i++)
160		{
161	27	Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
162	54	std::vector<InstMatch> newMatches;
163	54	InstMatch m(q);
164	659	while (d_children[i]->getNextMatch(q, m) > 0)
165		{
166		// m.makeRepresentative( qe );
167	316	newMatches.push_back(InstMatch(&m));
168	316	m.clear();
169		}
170	54	Trace("multi-trigger-cache") << "Made " << newMatches.size()
171	27	<< " new matches for index " << i << std::endl;
172	343	for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
173		{
174	632	Trace("multi-trigger-cache2")
175	632	<< "...processing " << j << " / " << newMatches.size()
176	316	<< ", #lemmas = " << addedLemmas << std::endl;
177	316	processNewMatch(newMatches[j], i, addedLemmas);
178	316	if (d_qstate.isInConflict())
179		{
180		return addedLemmas;
181		}
182		}
183		}
184	12	return addedLemmas;
185		}
186
187	316	void InstMatchGeneratorMulti::processNewMatch(InstMatch& m,
188		size_t fromChildIndex,
189		uint64_t& addedLemmas)
190		{
191		// see if these produce new matches
192	316	d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.d_vals);
193		// possibly only do the following if we know that new matches will be
194		// produced? the issue is that instantiations are filtered in quantifiers
195		// engine, and so there is no guarentee that
196		// we can safely skip the following lines, even when we have already produced
197		// this match.
198	632	Trace("multi-trigger-cache-debug")
199	316	<< "Child " << fromChildIndex << " produced match " << m << std::endl;
200		// process new instantiations
201	316	size_t childIndex = (fromChildIndex + 1) % d_children.size();
202	632	processNewInstantiations(m,
203		addedLemmas,
204	316	d_children_trie[childIndex].getTrie(),
205		0,
206		childIndex,
207		fromChildIndex,
208		true);
209	316	}
210
211	9293	void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
212		uint64_t& addedLemmas,
213		InstMatchTrie* tr,
214		size_t trieIndex,
215		size_t childIndex,
216		size_t endChildIndex,
217		bool modEq)
218		{
219	9293	Assert(!d_qstate.isInConflict());
220	9293	if (childIndex == endChildIndex)
221		{
222		// m is an instantiation
223	3069	if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
224		{
225	1300	addedLemmas++;
226	2600	Trace("multi-trigger-cache-debug")
227	1300	<< "-> Produced instantiation " << m << std::endl;
228		}
229	3069	return;
230		}
231	6224	InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
232	6224	if (trieIndex < iio->d_order.size())
233		{
234	2687	size_t curr_index = iio->d_order[trieIndex];
235	3945	Node n = m.get(curr_index);
236	2687	if (n.isNull())
237		{
238		// add to InstMatch
239	5782	for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
240		{
241	8706	InstMatch mn(&m);
242	4353	mn.setValue(curr_index, d.first);
243	4353	processNewInstantiations(mn,
244		addedLemmas,
245		&(d.second),
246		trieIndex + 1,
247		childIndex,
248		endChildIndex,
249		modEq);
250	4353	if (d_qstate.isInConflict())
251		{
252		break;
253		}
254		}
255		}
256		// shared and set variable, try to merge
257	2687	std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
258	2687	if (it != tr->d_data.end())
259		{
260	1898	processNewInstantiations(m,
261		addedLemmas,
262	949	&(it->second),
263		trieIndex + 1,
264		childIndex,
265		endChildIndex,
266		modEq);
267		}
268	2687	if (!modEq)
269		{
270		return;
271		}
272	2687	QuantifiersState& qs = d_qstate;
273		// check modulo equality for other possible instantiations
274	2687	if (!qs.hasTerm(n))
275		{
276	1429	return;
277		}
278	1258	eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
279	5914	while (!eqc.isFinished())
280		{
281	4656	Node en = (*eqc);
282	2328	if (en != n)
283		{
284	1070	std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
285	1070	if (itc != tr->d_data.end())
286		{
287	276	processNewInstantiations(m,
288		addedLemmas,
289	138	&(itc->second),
290		trieIndex + 1,
291		childIndex,
292		endChildIndex,
293		modEq);
294	138	if (d_qstate.isInConflict())
295		{
296		break;
297		}
298		}
299		}
300	2328	++eqc;
301		}
302		}
303		else
304		{
305	3537	size_t newChildIndex = (childIndex + 1) % d_children.size();
306	7074	processNewInstantiations(m,
307		addedLemmas,
308	3537	d_children_trie[newChildIndex].getTrie(),
309		0,
310		newChildIndex,
311		endChildIndex,
312		modEq);
313		}
314		}
315
316		} // namespace inst
317		} // namespace quantifiers
318		} // namespace theory
319	22746	} // namespace cvc5