Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_poly_norm.cpp	Lines:	121	125	96.8 %
Date:	2021-11-07	Branches:	184	403	45.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Arithmetic utility for polynomial normalization
 */

#include "theory/arith/arith_poly_norm.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {

void PolyNorm::addMonomial(TNode x, const Rational& c, bool isNeg)
{
  Assert(c.sgn() != 0);
  std::unordered_map<Node, Rational>::iterator it = d_polyNorm.find(x);
  if (it == d_polyNorm.end())
  {
    d_polyNorm[x] = isNeg ? -c : c;
    return;
  }
  Rational res(it->second + (isNeg ? -c : c));
  if (res.sgn() == 0)
  {
    // cancels
    d_polyNorm.erase(it);
  }
  else
  {
    d_polyNorm[x] = res;
  }
}

void PolyNorm::multiplyMonomial(TNode x, const Rational& c)
{
  Assert(c.sgn() != 0);
  if (x.isNull())
  {
    // multiply by constant
    for (std::pair<const Node, Rational>& m : d_polyNorm)
    {
      // c1*x*c2 = (c1*c2)*x
      m.second *= c;
    }
  }
  else
  {
    std::unordered_map<Node, Rational> ptmp = d_polyNorm;
    d_polyNorm.clear();
    for (const std::pair<const Node, Rational>& m : ptmp)
    {
      // c1*x1*c2*x2 = (c1*c2)*(x1*x2)
      Node newM = multMonoVar(m.first, x);
      d_polyNorm[newM] = m.second * c;
    }
  }
}

void PolyNorm::add(const PolyNorm& p)
{
  for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
  {
    addMonomial(m.first, m.second);
  }
}

void PolyNorm::subtract(const PolyNorm& p)
{
  for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
  {
    addMonomial(m.first, m.second, true);
  }
}

void PolyNorm::multiply(const PolyNorm& p)
{
  if (p.d_polyNorm.size() == 1)
  {
    for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
    {
      multiplyMonomial(m.first, m.second);
    }
  }
  else
  {
    // If multiplying by sum, must distribute; if multiplying by zero, clear.
    // First, remember the current state and clear.
    std::unordered_map<Node, Rational> ptmp = d_polyNorm;
    d_polyNorm.clear();
    for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
    {
      PolyNorm pbase;
      pbase.d_polyNorm = ptmp;
      pbase.multiplyMonomial(m.first, m.second);
      // add this to current
      add(pbase);
    }
  }
}

void PolyNorm::clear() { d_polyNorm.clear(); }

bool PolyNorm::empty() const { return d_polyNorm.empty(); }

bool PolyNorm::isEqual(const PolyNorm& p) const
{
  if (d_polyNorm.size() != p.d_polyNorm.size())
  {
    return false;
  }
  std::unordered_map<Node, Rational>::const_iterator it;
  for (const std::pair<const Node, Rational>& m : d_polyNorm)
  {
    Assert(m.second.sgn() != 0);
    it = p.d_polyNorm.find(m.first);
    if (it == p.d_polyNorm.end() || m.second != it->second)
    {
      return false;
    }
  }
  return true;
}

Node PolyNorm::multMonoVar(TNode m1, TNode m2)
{
  std::vector<TNode> vars = getMonoVars(m1);
  std::vector<TNode> vars2 = getMonoVars(m2);
  vars.insert(vars.end(), vars2.begin(), vars2.end());
  if (vars.empty())
  {
    // constants
    return Node::null();
  }
  else if (vars.size() == 1)
  {
    return vars[0];
  }
  // use default sorting
  std::sort(vars.begin(), vars.end());
  return NodeManager::currentNM()->mkNode(NONLINEAR_MULT, vars);
}

std::vector<TNode> PolyNorm::getMonoVars(TNode m)
{
  std::vector<TNode> vars;
  // m is null if this is the empty variable (for constant monomials)
  if (!m.isNull())
  {
    Kind k = m.getKind();
    Assert(k != CONST_RATIONAL);
    if (k == MULT || k == NONLINEAR_MULT)
    {
      vars.insert(vars.end(), m.begin(), m.end());
    }
    else
    {
      vars.push_back(m);
    }
  }
  return vars;
}

PolyNorm PolyNorm::mkPolyNorm(TNode n)
{
  Assert(n.getType().isReal());
  Rational one(1);
  Node null;
  std::unordered_map<TNode, PolyNorm> visited;
  std::unordered_map<TNode, PolyNorm>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    it = visited.find(cur);
    Kind k = cur.getKind();
    if (it == visited.end())
    {
      if (k == CONST_RATIONAL)
      {
        Rational r = cur.getConst<Rational>();
        if (r.sgn() == 0)
        {
          // zero is not an entry
          visited[cur] = PolyNorm();
        }
        else
        {
          visited[cur].addMonomial(null, r);
        }
      }
      else if (k == PLUS || k == MINUS || k == UMINUS || k == MULT
               || k == NONLINEAR_MULT)
      {
        visited[cur] = PolyNorm();
        for (const Node& cn : cur)
        {
          visit.push_back(cn);
        }
      }
      else
      {
        // it is a leaf
        visited[cur].addMonomial(cur, one);
        visit.pop_back();
      }
      continue;
    }
    visit.pop_back();
    if (it->second.empty())
    {
      PolyNorm& ret = visited[cur];
      switch (k)
      {
        case PLUS:
        case MINUS:
        case UMINUS:
        case MULT:
        case NONLINEAR_MULT:
          for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
          {
            it = visited.find(cur[i]);
            Assert(it != visited.end());
            if ((k == MINUS && i == 1) || k == UMINUS)
            {
              ret.subtract(it->second);
            }
            else if (i > 0 && (k == MULT || k == NONLINEAR_MULT))
            {
              ret.multiply(it->second);
            }
            else
            {
              ret.add(it->second);
            }
          }
          break;
        case CONST_RATIONAL: break;
        default: Unhandled() << "Unhandled polynomial operation " << cur; break;
      }
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  return visited[n];
}

bool PolyNorm::isArithPolyNorm(TNode a, TNode b)
{
  PolyNorm pa = PolyNorm::mkPolyNorm(a);
  PolyNorm pb = PolyNorm::mkPolyNorm(b);
  return pa.isEqual(pb);
}

}  // 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
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		* Arithmetic utility for polynomial normalization
14		*/
15
16		#include "theory/arith/arith_poly_norm.h"
17
18		using namespace cvc5::kind;
19
20		namespace cvc5 {
21		namespace theory {
22		namespace arith {
23
24	298	void PolyNorm::addMonomial(TNode x, const Rational& c, bool isNeg)
25		{
26	298	Assert(c.sgn() != 0);
27	298	std::unordered_map<Node, Rational>::iterator it = d_polyNorm.find(x);
28	298	if (it == d_polyNorm.end())
29		{
30	272	d_polyNorm[x] = isNeg ? -c : c;
31	272	return;
32		}
33	52	Rational res(it->second + (isNeg ? -c : c));
34	26	if (res.sgn() == 0)
35		{
36		// cancels
37	8	d_polyNorm.erase(it);
38		}
39		else
40		{
41	18	d_polyNorm[x] = res;
42		}
43		}
44
45	28	void PolyNorm::multiplyMonomial(TNode x, const Rational& c)
46		{
47	28	Assert(c.sgn() != 0);
48	28	if (x.isNull())
49		{
50		// multiply by constant
51	14	for (std::pair<const Node, Rational>& m : d_polyNorm)
52		{
53		// c1xc2 = (c1c2)x
54	8	m.second *= c;
55		}
56		}
57		else
58		{
59	44	std::unordered_map<Node, Rational> ptmp = d_polyNorm;
60	22	d_polyNorm.clear();
61	44	for (const std::pair<const Node, Rational>& m : ptmp)
62		{
63		// c1x1c2x2 = (c1c2)(x1x2)
64	44	Node newM = multMonoVar(m.first, x);
65	22	d_polyNorm[newM] = m.second * c;
66		}
67		}
68	28	}
69
70	156	void PolyNorm::add(const PolyNorm& p)
71		{
72	314	for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
73		{
74	158	addMonomial(m.first, m.second);
75		}
76	156	}
77
78	10	void PolyNorm::subtract(const PolyNorm& p)
79		{
80	30	for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
81		{
82	20	addMonomial(m.first, m.second, true);
83		}
84	10	}
85
86	26	void PolyNorm::multiply(const PolyNorm& p)
87		{
88	26	if (p.d_polyNorm.size() == 1)
89		{
90	40	for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
91		{
92	20	multiplyMonomial(m.first, m.second);
93		}
94		}
95		else
96		{
97		// If multiplying by sum, must distribute; if multiplying by zero, clear.
98		// First, remember the current state and clear.
99	12	std::unordered_map<Node, Rational> ptmp = d_polyNorm;
100	6	d_polyNorm.clear();
101	14	for (const std::pair<const Node, Rational>& m : p.d_polyNorm)
102		{
103	16	PolyNorm pbase;
104	8	pbase.d_polyNorm = ptmp;
105	8	pbase.multiplyMonomial(m.first, m.second);
106		// add this to current
107	8	add(pbase);
108		}
109		}
110	26	}
111
112		void PolyNorm::clear() { d_polyNorm.clear(); }
113
114	138	bool PolyNorm::empty() const { return d_polyNorm.empty(); }
115
116	28	bool PolyNorm::isEqual(const PolyNorm& p) const
117		{
118	28	if (d_polyNorm.size() != p.d_polyNorm.size())
119		{
120	2	return false;
121		}
122	26	std::unordered_map<Node, Rational>::const_iterator it;
123	68	for (const std::pair<const Node, Rational>& m : d_polyNorm)
124		{
125	44	Assert(m.second.sgn() != 0);
126	44	it = p.d_polyNorm.find(m.first);
127	44	if (it == p.d_polyNorm.end() \|\| m.second != it->second)
128		{
129	2	return false;
130		}
131		}
132	24	return true;
133		}
134
135	22	Node PolyNorm::multMonoVar(TNode m1, TNode m2)
136		{
137	44	std::vector<TNode> vars = getMonoVars(m1);
138	44	std::vector<TNode> vars2 = getMonoVars(m2);
139	22	vars.insert(vars.end(), vars2.begin(), vars2.end());
140	22	if (vars.empty())
141		{
142		// constants
143		return Node::null();
144		}
145	22	else if (vars.size() == 1)
146		{
147	10	return vars[0];
148		}
149		// use default sorting
150	12	std::sort(vars.begin(), vars.end());
151	12	return NodeManager::currentNM()->mkNode(NONLINEAR_MULT, vars);
152		}
153
154	44	std::vector<TNode> PolyNorm::getMonoVars(TNode m)
155		{
156	44	std::vector<TNode> vars;
157		// m is null if this is the empty variable (for constant monomials)
158	44	if (!m.isNull())
159		{
160	34	Kind k = m.getKind();
161	34	Assert(k != CONST_RATIONAL);
162	34	if (k == MULT \|\| k == NONLINEAR_MULT)
163		{
164		vars.insert(vars.end(), m.begin(), m.end());
165		}
166		else
167		{
168	34	vars.push_back(m);
169		}
170		}
171	44	return vars;
172		}
173
174	56	PolyNorm PolyNorm::mkPolyNorm(TNode n)
175		{
176	56	Assert(n.getType().isReal());
177	112	Rational one(1);
178	112	Node null;
179	112	std::unordered_map<TNode, PolyNorm> visited;
180	56	std::unordered_map<TNode, PolyNorm>::iterator it;
181	112	std::vector<TNode> visit;
182	112	TNode cur;
183	56	visit.push_back(n);
184	292	do
185		{
186	348	cur = visit.back();
187	348	it = visited.find(cur);
188	348	Kind k = cur.getKind();
189	348	if (it == visited.end())
190		{
191	210	if (k == CONST_RATIONAL)
192		{
193	56	Rational r = cur.getConst<Rational>();
194	28	if (r.sgn() == 0)
195		{
196		// zero is not an entry
197	10	visited[cur] = PolyNorm();
198		}
199		else
200		{
201	18	visited[cur].addMonomial(null, r);
202		}
203		}
204	182	else if (k == PLUS \|\| k == MINUS \|\| k == UMINUS \|\| k == MULT
205	102	\|\| k == NONLINEAR_MULT)
206		{
207	80	visited[cur] = PolyNorm();
208	264	for (const Node& cn : cur)
209		{
210	184	visit.push_back(cn);
211	80	}
212		}
213		else
214		{
215		// it is a leaf
216	102	visited[cur].addMonomial(cur, one);
217	102	visit.pop_back();
218		}
219	210	continue;
220		}
221	138	visit.pop_back();
222	138	if (it->second.empty())
223		{
224	90	PolyNorm& ret = visited[cur];
225	90	switch (k)
226		{
227	80	case PLUS:
228		case MINUS:
229		case UMINUS:
230		case MULT:
231		case NONLINEAR_MULT:
232	264	for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
233		{
234	184	it = visited.find(cur[i]);
235	184	Assert(it != visited.end());
236	184	if ((k == MINUS && i == 1) \|\| k == UMINUS)
237		{
238	10	ret.subtract(it->second);
239		}
240	174	else if (i > 0 && (k == MULT \|\| k == NONLINEAR_MULT))
241		{
242	26	ret.multiply(it->second);
243		}
244		else
245		{
246	148	ret.add(it->second);
247		}
248	80	}
249	80	break;
250	10	case CONST_RATIONAL: break;
251		default: Unhandled() << "Unhandled polynomial operation " << cur; break;
252		}
253		}
254	348	} while (!visit.empty());
255	56	Assert(visited.find(n) != visited.end());
256	112	return visited[n];
257		}
258
259	28	bool PolyNorm::isArithPolyNorm(TNode a, TNode b)
260		{
261	56	PolyNorm pa = PolyNorm::mkPolyNorm(a);
262	56	PolyNorm pb = PolyNorm::mkPolyNorm(b);
263	56	return pa.isEqual(pb);
264		}
265
266		} // namespace arith
267		} // namespace theory
268	31137	} // namespace cvc5