Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp	Lines:	87	88	98.9 %
Date:	2021-09-07	Branches:	113	232	48.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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 multi-linear inst match generator class.
 */
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/trigger_trie.h"
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;

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

InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
    Trigger* tparent, Node q, std::vector<Node>& pats)
    : InstMatchGenerator(tparent, Node::null())
{
  // order patterns to maximize eager matching failures
  std::map<Node, std::vector<Node> > var_contains;
  for (const Node& pat : pats)
  {
    TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
  }
  std::map<Node, std::vector<Node> > var_to_node;
  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
  {
    for (const Node& n : vc.second)
    {
      var_to_node[n].push_back(vc.first);
    }
  }
  std::vector<Node> pats_ordered;
  std::vector<bool> pats_ordered_independent;
  std::map<Node, bool> var_bound;
  size_t patsSize = pats.size();
  while (pats_ordered.size() < patsSize)
  {
    // score is lexographic ( bound vars, shared vars )
    int score_max_1 = -1;
    int score_max_2 = -1;
    unsigned score_index = 0;
    bool set_score_index = false;
    for (size_t i = 0; i < patsSize; i++)
    {
      Node p = pats[i];
      if (std::find(pats_ordered.begin(), pats_ordered.end(), p)
          == pats_ordered.end())
      {
        int score_1 = 0;
        int score_2 = 0;
        for (unsigned j = 0; j < var_contains[p].size(); j++)
        {
          Node v = var_contains[p][j];
          if (var_bound.find(v) != var_bound.end())
          {
            score_1++;
          }
          else if (var_to_node[v].size() > 1)
          {
            score_2++;
          }
        }
        if (!set_score_index || score_1 > score_max_1
            || (score_1 == score_max_1 && score_2 > score_max_2))
        {
          score_index = i;
          set_score_index = true;
          score_max_1 = score_1;
          score_max_2 = score_2;
        }
      }
    }
    Assert(set_score_index);
    // update the variable bounds
    Node mp = pats[score_index];
    std::vector<Node>& vcm = var_contains[mp];
    for (const Node& vc : vcm)
    {
      var_bound[vc] = true;
    }
    pats_ordered.push_back(mp);
    pats_ordered_independent.push_back(score_max_1 == 0);
  }

  Trace("multi-trigger-linear")
      << "Make children for linear multi trigger." << std::endl;
  for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
  {
    Node po = pats_ordered[i];
    Trace("multi-trigger-linear") << "...make for " << po << std::endl;
    InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
    Assert(cimg != nullptr);
    d_children.push_back(cimg);
    // this could be improved
    if (i == 0)
    {
      cimg->setIndependent();
    }
  }
}

int InstMatchGeneratorMultiLinear::resetChildren()
{
  for (InstMatchGenerator* c : d_children)
  {
    if (!c->reset(Node::null()))
    {
      return -2;
    }
  }
  return 1;
}

bool InstMatchGeneratorMultiLinear::reset(Node eqc)
{
  Assert(eqc.isNull());
  if (options::multiTriggerLinear())
  {
    return true;
  }
  return resetChildren() > 0;
}

int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
{
  Trace("multi-trigger-linear-debug")
      << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
  if (options::multiTriggerLinear())
  {
    // reset everyone
    int rc_ret = resetChildren();
    if (rc_ret < 0)
    {
      return rc_ret;
    }
  }
  Trace("multi-trigger-linear-debug")
      << "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
      << std::endl;
  Assert(d_next != nullptr);
  int ret_val =
      continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
  if (ret_val > 0)
  {
    Trace("multi-trigger-linear")
        << "Successful multi-trigger instantiation." << std::endl;
    if (options::multiTriggerLinear())
    {
      // now, restrict everyone
      for (size_t i = 0, csize = d_children.size(); i < csize; i++)
      {
        Node mi = d_children[i]->getCurrentMatch();
        Trace("multi-trigger-linear")
            << "   child " << i << " match : " << mi << std::endl;
        d_children[i]->excludeMatch(mi);
      }
    }
  }
  return ret_val;
}

}  // 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, Aina Niemetz
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 multi-linear inst match generator class.
14		*/
15		#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
16
17		#include "options/quantifiers_options.h"
18		#include "theory/quantifiers/ematching/trigger_trie.h"
19		#include "theory/quantifiers/term_util.h"
20
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26		namespace inst {
27
28	1300	InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
29	1300	Trigger* tparent, Node q, std::vector<Node>& pats)
30	1300	: InstMatchGenerator(tparent, Node::null())
31		{
32		// order patterns to maximize eager matching failures
33	2600	std::map<Node, std::vector<Node> > var_contains;
34	4178	for (const Node& pat : pats)
35		{
36	2878	TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]);
37		}
38	2600	std::map<Node, std::vector<Node> > var_to_node;
39	4178	for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
40		{
41	8251	for (const Node& n : vc.second)
42		{
43	5373	var_to_node[n].push_back(vc.first);
44		}
45		}
46	2600	std::vector<Node> pats_ordered;
47	2600	std::vector<bool> pats_ordered_independent;
48	2600	std::map<Node, bool> var_bound;
49	1300	size_t patsSize = pats.size();
50	7056	while (pats_ordered.size() < patsSize)
51		{
52		// score is lexographic ( bound vars, shared vars )
53	2878	int score_max_1 = -1;
54	2878	int score_max_2 = -1;
55	2878	unsigned score_index = 0;
56	2878	bool set_score_index = false;
57	9618	for (size_t i = 0; i < patsSize; i++)
58		{
59	13480	Node p = pats[i];
60	20220	if (std::find(pats_ordered.begin(), pats_ordered.end(), p)
61	20220	== pats_ordered.end())
62		{
63	4809	int score_1 = 0;
64	4809	int score_2 = 0;
65	13516	for (unsigned j = 0; j < var_contains[p].size(); j++)
66		{
67	17414	Node v = var_contains[p][j];
68	8707	if (var_bound.find(v) != var_bound.end())
69		{
70	818	score_1++;
71		}
72	7889	else if (var_to_node[v].size() > 1)
73		{
74	1492	score_2++;
75		}
76		}
77	4809	if (!set_score_index \|\| score_1 > score_max_1
78	1817	\|\| (score_1 == score_max_1 && score_2 > score_max_2))
79		{
80	3022	score_index = i;
81	3022	set_score_index = true;
82	3022	score_max_1 = score_1;
83	3022	score_max_2 = score_2;
84		}
85		}
86		}
87	2878	Assert(set_score_index);
88		// update the variable bounds
89	5756	Node mp = pats[score_index];
90	2878	std::vector<Node>& vcm = var_contains[mp];
91	8251	for (const Node& vc : vcm)
92		{
93	5373	var_bound[vc] = true;
94		}
95	2878	pats_ordered.push_back(mp);
96	2878	pats_ordered_independent.push_back(score_max_1 == 0);
97		}
98
99	2600	Trace("multi-trigger-linear")
100	1300	<< "Make children for linear multi trigger." << std::endl;
101	4178	for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
102		{
103	5756	Node po = pats_ordered[i];
104	2878	Trace("multi-trigger-linear") << "...make for " << po << std::endl;
105	2878	InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
106	2878	Assert(cimg != nullptr);
107	2878	d_children.push_back(cimg);
108		// this could be improved
109	2878	if (i == 0)
110		{
111	1300	cimg->setIndependent();
112		}
113		}
114	1300	}
115
116	7353	int InstMatchGeneratorMultiLinear::resetChildren()
117		{
118	17359	for (InstMatchGenerator* c : d_children)
119		{
120	12825	if (!c->reset(Node::null()))
121		{
122	2819	return -2;
123		}
124		}
125	4534	return 1;
126		}
127
128	10862	bool InstMatchGeneratorMultiLinear::reset(Node eqc)
129		{
130	10862	Assert(eqc.isNull());
131	10862	if (options::multiTriggerLinear())
132		{
133	10862	return true;
134		}
135		return resetChildren() > 0;
136		}
137
138	7353	int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
139		{
140	14706	Trace("multi-trigger-linear-debug")
141	7353	<< "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
142	7353	if (options::multiTriggerLinear())
143		{
144		// reset everyone
145	7353	int rc_ret = resetChildren();
146	7353	if (rc_ret < 0)
147		{
148	2819	return rc_ret;
149		}
150		}
151	9068	Trace("multi-trigger-linear-debug")
152	4534	<< "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
153	4534	<< std::endl;
154	4534	Assert(d_next != nullptr);
155		int ret_val =
156	4534	continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
157	4534	if (ret_val > 0)
158		{
159	7410	Trace("multi-trigger-linear")
160	3705	<< "Successful multi-trigger instantiation." << std::endl;
161	3705	if (options::multiTriggerLinear())
162		{
163		// now, restrict everyone
164	11308	for (size_t i = 0, csize = d_children.size(); i < csize; i++)
165		{
166	15206	Node mi = d_children[i]->getCurrentMatch();
167	15206	Trace("multi-trigger-linear")
168	7603	<< " child " << i << " match : " << mi << std::endl;
169	7603	d_children[i]->excludeMatch(mi);
170		}
171		}
172		}
173	4534	return ret_val;
174		}
175
176		} // namespace inst
177		} // namespace quantifiers
178		} // namespace theory
179	29502	} // namespace cvc5