Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/ext/monomial.cpp	Lines:	162	168	96.4 %
Date:	2021-09-06	Branches:	251	520	48.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, Andres Noetzli
 *
 * 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 utilities for monomials.
 */

#include "theory/arith/nl/ext/monomial.h"

#include "theory/arith/arith_utilities.h"
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {

// Returns a[key] if key is in a or value otherwise.
unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value)
{
  NodeMultiset::const_iterator it = a.find(key);
  return (it == a.end()) ? value : it->second;
}
// Given two multisets return the multiset difference a \ b.
NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b)
{
  NodeMultiset difference;
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
  {
    Node key = it_a->first;
    const unsigned a_value = it_a->second;
    const unsigned b_value = getCountWithDefault(b, key, 0);
    if (a_value > b_value)
    {
      difference[key] = a_value - b_value;
    }
  }
  return difference;
}

// Return a vector containing a[key] repetitions of key in a multiset a.
std::vector<Node> ExpandMultiset(const NodeMultiset& a)
{
  std::vector<Node> expansion;
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
  {
    expansion.insert(expansion.end(), it_a->second, it_a->first);
  }
  return expansion;
}

// status 0 : n equal, -1 : n superset, 1 : n subset
void MonomialIndex::addTerm(Node n,
                            const std::vector<Node>& reps,
                            MonomialDb* nla,
                            int status,
                            unsigned argIndex)
{
  if (status == 0)
  {
    if (argIndex == reps.size())
    {
      d_monos.push_back(n);
    }
    else
    {
      d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1);
    }
  }
  for (std::map<Node, MonomialIndex>::iterator it = d_data.begin();
       it != d_data.end();
       ++it)
  {
    if (status != 0 || argIndex == reps.size() || it->first != reps[argIndex])
    {
      // if we do not contain this variable, then if we were a superset,
      // fail (-2), otherwise we are subset.  if we do contain this
      // variable, then if we were equal, we are superset since variables
      // are ordered, otherwise we remain the same.
      int new_status =
          std::find(reps.begin(), reps.end(), it->first) == reps.end()
              ? (status >= 0 ? 1 : -2)
              : (status == 0 ? -1 : status);
      if (new_status != -2)
      {
        it->second.addTerm(n, reps, nla, new_status, argIndex);
      }
    }
  }
  // compare for subsets
  for (unsigned i = 0; i < d_monos.size(); i++)
  {
    Node m = d_monos[i];
    if (m != n)
    {
      // we are superset if we are equal and haven't traversed all variables
      int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status;
      Trace("nl-ext-mindex-debug") << "  compare " << n << " and " << m
                                   << ", status = " << cstatus << std::endl;
      if (cstatus <= 0 && nla->isMonomialSubset(m, n))
      {
        nla->registerMonomialSubset(m, n);
        Trace("nl-ext-mindex-debug") << "...success" << std::endl;
      }
      else if (cstatus >= 0 && nla->isMonomialSubset(n, m))
      {
        nla->registerMonomialSubset(n, m);
        Trace("nl-ext-mindex-debug") << "...success (rev)" << std::endl;
      }
    }
  }
}

MonomialDb::MonomialDb()
{
  d_one = NodeManager::currentNM()->mkConst(Rational(1));
}

void MonomialDb::registerMonomial(Node n)
{
  if (std::find(d_monomials.begin(), d_monomials.end(), n) != d_monomials.end())
  {
    return;
  }
  d_monomials.push_back(n);
  Trace("nl-ext-debug") << "Register monomial : " << n << std::endl;
  Kind k = n.getKind();
  if (k == NONLINEAR_MULT)
  {
    // get exponent count
    unsigned nchild = n.getNumChildren();
    for (unsigned i = 0; i < nchild; i++)
    {
      d_m_exp[n][n[i]]++;
      if (i == 0 || n[i] != n[i - 1])
      {
        d_m_vlist[n].push_back(n[i]);
      }
    }
    d_m_degree[n] = nchild;
  }
  else if (n == d_one)
  {
    d_m_exp[n].clear();
    d_m_vlist[n].clear();
    d_m_degree[n] = 0;
  }
  else
  {
    Assert(k != PLUS && k != MULT);
    d_m_exp[n][n] = 1;
    d_m_vlist[n].push_back(n);
    d_m_degree[n] = 1;
  }
  std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end());
  Trace("nl-ext-mindex") << "Add monomial to index : " << n << std::endl;
  d_m_index.addTerm(n, d_m_vlist[n], this);
}

void MonomialDb::registerMonomialSubset(Node a, Node b)
{
  Assert(isMonomialSubset(a, b));

  const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
  const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);

  std::vector<Node> diff_children =
      ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map));
  Assert(!diff_children.empty());

  d_m_contain_parent[a].push_back(b);
  d_m_contain_children[b].push_back(a);

  Node mult_term = safeConstructNary(MULT, diff_children);
  Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children);
  d_m_contain_mult[a][b] = mult_term;
  d_m_contain_umult[a][b] = nlmult_term;
  Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b
                         << ", difference is " << mult_term << std::endl;
}

bool MonomialDb::isMonomialSubset(Node am, Node bm) const
{
  const NodeMultiset& a = getMonomialExponentMap(am);
  const NodeMultiset& b = getMonomialExponentMap(bm);
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
  {
    Node key = it_a->first;
    const unsigned a_value = it_a->second;
    const unsigned b_value = getCountWithDefault(b, key, 0);
    if (a_value > b_value)
    {
      return false;
    }
  }
  return true;
}

const NodeMultiset& MonomialDb::getMonomialExponentMap(Node monomial) const
{
  MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
  Assert(it != d_m_exp.end());
  return it->second;
}

unsigned MonomialDb::getExponent(Node monomial, Node v) const
{
  MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
  if (it == d_m_exp.end())
  {
    return 0;
  }
  std::map<Node, unsigned>::const_iterator itv = it->second.find(v);
  if (itv == it->second.end())
  {
    return 0;
  }
  return itv->second;
}

const std::vector<Node>& MonomialDb::getVariableList(Node monomial) const
{
  std::map<Node, std::vector<Node> >::const_iterator itvl =
      d_m_vlist.find(monomial);
  Assert(itvl != d_m_vlist.end());
  return itvl->second;
}

unsigned MonomialDb::getDegree(Node monomial) const
{
  std::map<Node, unsigned>::const_iterator it = d_m_degree.find(monomial);
  Assert(it != d_m_degree.end());
  return it->second;
}

void MonomialDb::sortByDegree(std::vector<Node>& ms) const
{
  SortNonlinearDegree snlad(d_m_degree);
  std::sort(ms.begin(), ms.end(), snlad);
}

void MonomialDb::sortVariablesByModel(std::vector<Node>& ms, NlModel& m)
{
  SortNlModel smv;
  smv.d_nlm = &m;
  smv.d_isConcrete = false;
  smv.d_isAbsolute = true;
  smv.d_reverse_order = true;
  for (const Node& msc : ms)
  {
    std::sort(d_m_vlist[msc].begin(), d_m_vlist[msc].end(), smv);
  }
}

const std::map<Node, std::vector<Node> >& MonomialDb::getContainsChildrenMap()
{
  return d_m_contain_children;
}

const std::map<Node, std::vector<Node> >& MonomialDb::getContainsParentMap()
{
  return d_m_contain_parent;
}

Node MonomialDb::getContainsDiff(Node a, Node b) const
{
  std::map<Node, std::map<Node, Node> >::const_iterator it =
      d_m_contain_mult.find(a);
  if (it == d_m_contain_mult.end())
  {
    return Node::null();
  }
  std::map<Node, Node>::const_iterator it2 = it->second.find(b);
  if (it2 == it->second.end())
  {
    return Node::null();
  }
  return it2->second;
}

Node MonomialDb::getContainsDiffNl(Node a, Node b) const
{
  std::map<Node, std::map<Node, Node> >::const_iterator it =
      d_m_contain_umult.find(a);
  if (it == d_m_contain_umult.end())
  {
    return Node::null();
  }
  std::map<Node, Node>::const_iterator it2 = it->second.find(b);
  if (it2 == it->second.end())
  {
    return Node::null();
  }
  return it2->second;
}

Node MonomialDb::mkMonomialRemFactor(Node n,
                                     const NodeMultiset& n_exp_rem) const
{
  std::vector<Node> children;
  const NodeMultiset& exponent_map = getMonomialExponentMap(n);
  for (NodeMultiset::const_iterator itme2 = exponent_map.begin();
       itme2 != exponent_map.end();
       ++itme2)
  {
    Node v = itme2->first;
    unsigned inc = itme2->second;
    Trace("nl-ext-mono-factor")
        << "..." << inc << " factors of " << v << std::endl;
    unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0);
    Assert(count_in_n_exp_rem <= inc);
    inc -= count_in_n_exp_rem;
    Trace("nl-ext-mono-factor")
        << "......rem, now " << inc << " factors of " << v << std::endl;
    children.insert(children.end(), inc, v);
  }
  Node ret = safeConstructNary(MULT, children);
  ret = Rewriter::rewrite(ret);
  Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
  return ret;
}

}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, Andres Noetzli
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 utilities for monomials.
14		*/
15
16		#include "theory/arith/nl/ext/monomial.h"
17
18		#include "theory/arith/arith_utilities.h"
19		#include "theory/arith/nl/nl_lemma_utils.h"
20		#include "theory/rewriter.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace arith {
27		namespace nl {
28
29		// Returns a[key] if key is in a or value otherwise.
30	95923	unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value)
31		{
32	95923	NodeMultiset::const_iterator it = a.find(key);
33	95923	return (it == a.end()) ? value : it->second;
34		}
35		// Given two multisets return the multiset difference a \ b.
36	7365	NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b)
37		{
38	7365	NodeMultiset difference;
39	19913	for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
40		{
41	25096	Node key = it_a->first;
42	12548	const unsigned a_value = it_a->second;
43	12548	const unsigned b_value = getCountWithDefault(b, key, 0);
44	12548	if (a_value > b_value)
45		{
46	9632	difference[key] = a_value - b_value;
47		}
48		}
49	7365	return difference;
50		}
51
52		// Return a vector containing a[key] repetitions of key in a multiset a.
53	7365	std::vector<Node> ExpandMultiset(const NodeMultiset& a)
54		{
55	7365	std::vector<Node> expansion;
56	16997	for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
57		{
58	9632	expansion.insert(expansion.end(), it_a->second, it_a->first);
59		}
60	7365	return expansion;
61		}
62
63		// status 0 : n equal, -1 : n superset, 1 : n subset
64	74836	void MonomialIndex::addTerm(Node n,
65		const std::vector<Node>& reps,
66		MonomialDb* nla,
67		int status,
68		unsigned argIndex)
69		{
70	74836	if (status == 0)
71		{
72	9989	if (argIndex == reps.size())
73		{
74	4569	d_monos.push_back(n);
75		}
76		else
77		{
78	5420	d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1);
79		}
80		}
81	145216	for (std::map<Node, MonomialIndex>::iterator it = d_data.begin();
82	145216	it != d_data.end();
83		++it)
84		{
85	70380	if (status != 0 \|\| argIndex == reps.size() \|\| it->first != reps[argIndex])
86		{
87		// if we do not contain this variable, then if we were a superset,
88		// fail (-2), otherwise we are subset. if we do contain this
89		// variable, then if we were equal, we are superset since variables
90		// are ordered, otherwise we remain the same.
91		int new_status =
92	129920	std::find(reps.begin(), reps.end(), it->first) == reps.end()
93	67022	? (status >= 0 ? 1 : -2)
94	67022	: (status == 0 ? -1 : status);
95	64960	if (new_status != -2)
96		{
97	64847	it->second.addTerm(n, reps, nla, new_status, argIndex);
98		}
99		}
100		}
101		// compare for subsets
102	148154	for (unsigned i = 0; i < d_monos.size(); i++)
103		{
104	146636	Node m = d_monos[i];
105	73318	if (m != n)
106		{
107		// we are superset if we are equal and haven't traversed all variables
108	68749	int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status;
109	137498	Trace("nl-ext-mindex-debug") << " compare " << n << " and " << m
110	68749	<< ", status = " << cstatus << std::endl;
111	68749	if (cstatus <= 0 && nla->isMonomialSubset(m, n))
112		{
113	4289	nla->registerMonomialSubset(m, n);
114	4289	Trace("nl-ext-mindex-debug") << "...success" << std::endl;
115		}
116	64460	else if (cstatus >= 0 && nla->isMonomialSubset(n, m))
117		{
118	3076	nla->registerMonomialSubset(n, m);
119	3076	Trace("nl-ext-mindex-debug") << "...success (rev)" << std::endl;
120		}
121		}
122		}
123	74836	}
124
125	5211	MonomialDb::MonomialDb()
126		{
127	5211	d_one = NodeManager::currentNM()->mkConst(Rational(1));
128	5211	}
129
130	68589	void MonomialDb::registerMonomial(Node n)
131		{
132	68589	if (std::find(d_monomials.begin(), d_monomials.end(), n) != d_monomials.end())
133		{
134	64020	return;
135		}
136	4569	d_monomials.push_back(n);
137	4569	Trace("nl-ext-debug") << "Register monomial : " << n << std::endl;
138	4569	Kind k = n.getKind();
139	4569	if (k == NONLINEAR_MULT)
140		{
141		// get exponent count
142	1498	unsigned nchild = n.getNumChildren();
143	4913	for (unsigned i = 0; i < nchild; i++)
144		{
145	3415	d_m_exp[n][n[i]]++;
146	3415	if (i == 0 \|\| n[i] != n[i - 1])
147		{
148	2834	d_m_vlist[n].push_back(n[i]);
149		}
150		}
151	1498	d_m_degree[n] = nchild;
152		}
153	3071	else if (n == d_one)
154		{
155	485	d_m_exp[n].clear();
156	485	d_m_vlist[n].clear();
157	485	d_m_degree[n] = 0;
158		}
159		else
160		{
161	2586	Assert(k != PLUS && k != MULT);
162	2586	d_m_exp[n][n] = 1;
163	2586	d_m_vlist[n].push_back(n);
164	2586	d_m_degree[n] = 1;
165		}
166	4569	std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end());
167	4569	Trace("nl-ext-mindex") << "Add monomial to index : " << n << std::endl;
168	4569	d_m_index.addTerm(n, d_m_vlist[n], this);
169		}
170
171	7365	void MonomialDb::registerMonomialSubset(Node a, Node b)
172		{
173	7365	Assert(isMonomialSubset(a, b));
174
175	7365	const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
176	7365	const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);
177
178		std::vector<Node> diff_children =
179	14730	ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map));
180	7365	Assert(!diff_children.empty());
181
182	7365	d_m_contain_parent[a].push_back(b);
183	7365	d_m_contain_children[b].push_back(a);
184
185	14730	Node mult_term = safeConstructNary(MULT, diff_children);
186	14730	Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children);
187	7365	d_m_contain_mult[a][b] = mult_term;
188	7365	d_m_contain_umult[a][b] = nlmult_term;
189	14730	Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b
190	7365	<< ", difference is " << mult_term << std::endl;
191	7365	}
192
193	76470	bool MonomialDb::isMonomialSubset(Node am, Node bm) const
194		{
195	76470	const NodeMultiset& a = getMonomialExponentMap(am);
196	76470	const NodeMultiset& b = getMonomialExponentMap(bm);
197	85931	for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
198		{
199	80662	Node key = it_a->first;
200	71201	const unsigned a_value = it_a->second;
201	71201	const unsigned b_value = getCountWithDefault(b, key, 0);
202	71201	if (a_value > b_value)
203		{
204	61740	return false;
205		}
206		}
207	14730	return true;
208		}
209
210	221953	const NodeMultiset& MonomialDb::getMonomialExponentMap(Node monomial) const
211		{
212	221953	MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
213	221953	Assert(it != d_m_exp.end());
214	221953	return it->second;
215		}
216
217	393291	unsigned MonomialDb::getExponent(Node monomial, Node v) const
218		{
219	393291	MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
220	393291	if (it == d_m_exp.end())
221		{
222		return 0;
223		}
224	393291	std::map<Node, unsigned>::const_iterator itv = it->second.find(v);
225	393291	if (itv == it->second.end())
226		{
227		return 0;
228		}
229	393291	return itv->second;
230		}
231
232	699405	const std::vector<Node>& MonomialDb::getVariableList(Node monomial) const
233		{
234		std::map<Node, std::vector<Node> >::const_iterator itvl =
235	699405	d_m_vlist.find(monomial);
236	699405	Assert(itvl != d_m_vlist.end());
237	699405	return itvl->second;
238		}
239
240	23068	unsigned MonomialDb::getDegree(Node monomial) const
241		{
242	23068	std::map<Node, unsigned>::const_iterator it = d_m_degree.find(monomial);
243	23068	Assert(it != d_m_degree.end());
244	23068	return it->second;
245		}
246
247	743	void MonomialDb::sortByDegree(std::vector<Node>& ms) const
248		{
249	743	SortNonlinearDegree snlad(d_m_degree);
250	743	std::sort(ms.begin(), ms.end(), snlad);
251	743	}
252
253	1988	void MonomialDb::sortVariablesByModel(std::vector<Node>& ms, NlModel& m)
254		{
255	1988	SortNlModel smv;
256	1988	smv.d_nlm = &m;
257	1988	smv.d_isConcrete = false;
258	1988	smv.d_isAbsolute = true;
259	1988	smv.d_reverse_order = true;
260	13548	for (const Node& msc : ms)
261		{
262	11560	std::sort(d_m_vlist[msc].begin(), d_m_vlist[msc].end(), smv);
263		}
264	1988	}
265
266	24	const std::map<Node, std::vector<Node> >& MonomialDb::getContainsChildrenMap()
267		{
268	24	return d_m_contain_children;
269		}
270
271	743	const std::map<Node, std::vector<Node> >& MonomialDb::getContainsParentMap()
272		{
273	743	return d_m_contain_parent;
274		}
275
276	67023	Node MonomialDb::getContainsDiff(Node a, Node b) const
277		{
278		std::map<Node, std::map<Node, Node> >::const_iterator it =
279	67023	d_m_contain_mult.find(a);
280	67023	if (it == d_m_contain_mult.end())
281		{
282		return Node::null();
283		}
284	67023	std::map<Node, Node>::const_iterator it2 = it->second.find(b);
285	67023	if (it2 == it->second.end())
286		{
287		return Node::null();
288		}
289	67023	return it2->second;
290		}
291
292	45	Node MonomialDb::getContainsDiffNl(Node a, Node b) const
293		{
294		std::map<Node, std::map<Node, Node> >::const_iterator it =
295	45	d_m_contain_umult.find(a);
296	45	if (it == d_m_contain_umult.end())
297		{
298		return Node::null();
299		}
300	45	std::map<Node, Node>::const_iterator it2 = it->second.find(b);
301	45	if (it2 == it->second.end())
302		{
303		return Node::null();
304		}
305	45	return it2->second;
306		}
307
308	6962	Node MonomialDb::mkMonomialRemFactor(Node n,
309		const NodeMultiset& n_exp_rem) const
310		{
311	13924	std::vector<Node> children;
312	6962	const NodeMultiset& exponent_map = getMonomialExponentMap(n);
313	19136	for (NodeMultiset::const_iterator itme2 = exponent_map.begin();
314	19136	itme2 != exponent_map.end();
315		++itme2)
316		{
317	24348	Node v = itme2->first;
318	12174	unsigned inc = itme2->second;
319	24348	Trace("nl-ext-mono-factor")
320	12174	<< "..." << inc << " factors of " << v << std::endl;
321	12174	unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0);
322	12174	Assert(count_in_n_exp_rem <= inc);
323	12174	inc -= count_in_n_exp_rem;
324	24348	Trace("nl-ext-mono-factor")
325	12174	<< "......rem, now " << inc << " factors of " << v << std::endl;
326	12174	children.insert(children.end(), inc, v);
327		}
328	6962	Node ret = safeConstructNary(MULT, children);
329	6962	ret = Rewriter::rewrite(ret);
330	6962	Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
331	13924	return ret;
332		}
333
334		} // namespace nl
335		} // namespace arith
336		} // namespace theory
337	29508	} // namespace cvc5