Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_utilities.cpp	Lines:	127	161	78.9 %
Date:	2021-05-22	Branches:	230	654	35.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Alex Ozdemir, 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.
 * ****************************************************************************
 *
 * Implementation of common functions for dealing with nodes.
 */

#include "arith_utilities.h"

#include <cmath>

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {

Kind joinKinds(Kind k1, Kind k2)
{
  if (k2 < k1)
  {
    return joinKinds(k2, k1);
  }
  else if (k1 == k2)
  {
    return k1;
  }
  Assert(isRelationOperator(k1));
  Assert(isRelationOperator(k2));
  if (k1 == EQUAL)
  {
    if (k2 == LEQ || k2 == GEQ)
    {
      return k1;
    }
  }
  else if (k1 == LT)
  {
    if (k2 == LEQ)
    {
      return k1;
    }
  }
  else if (k1 == LEQ)
  {
    if (k2 == GEQ)
    {
      return EQUAL;
    }
  }
  else if (k1 == GT)
  {
    if (k2 == GEQ)
    {
      return k1;
    }
  }
  return UNDEFINED_KIND;
}

Kind transKinds(Kind k1, Kind k2)
{
  if (k2 < k1)
  {
    return transKinds(k2, k1);
  }
  else if (k1 == k2)
  {
    return k1;
  }
  Assert(isRelationOperator(k1));
  Assert(isRelationOperator(k2));
  if (k1 == EQUAL)
  {
    return k2;
  }
  else if (k1 == LT)
  {
    if (k2 == LEQ)
    {
      return k1;
    }
  }
  else if (k1 == GT)
  {
    if (k2 == GEQ)
    {
      return k1;
    }
  }
  return UNDEFINED_KIND;
}

bool isTranscendentalKind(Kind k)
{
  // many operators are eliminated during rewriting
  Assert(k != TANGENT && k != COSINE && k != COSECANT
         && k != SECANT && k != COTANGENT);
  return k == EXPONENTIAL || k == SINE || k == PI;
}

Node getApproximateConstant(Node c, bool isLower, unsigned prec)
{
  if (!c.isConst())
  {
    Assert(false) << "getApproximateConstant: non-constant input " << c;
    return Node::null();
  }
  Rational cr = c.getConst<Rational>();

  unsigned lower = 0;
  unsigned upper = std::pow(10, prec);

  Rational den = Rational(upper);
  if (cr.getDenominator() < den.getNumerator())
  {
    // denominator is not more than precision, we return it
    return c;
  }

  int csign = cr.sgn();
  Assert(csign != 0);
  if (csign == -1)
  {
    cr = -cr;
  }
  Rational one = Rational(1);
  Rational ten = Rational(10);
  Rational pow_ten = Rational(1);
  // inefficient for large numbers
  while (cr >= one)
  {
    cr = cr / ten;
    pow_ten = pow_ten * ten;
  }
  Rational allow_err = one / den;

  // now do binary search
  Rational two = Rational(2);
  NodeManager* nm = NodeManager::currentNM();
  Node cret;
  do
  {
    unsigned curr = (lower + upper) / 2;
    Rational curr_r = Rational(curr) / den;
    Rational err = cr - curr_r;
    int esign = err.sgn();
    if (err.abs() <= allow_err)
    {
      if (esign == 1 && !isLower)
      {
        curr_r = Rational(curr + 1) / den;
      }
      else if (esign == -1 && isLower)
      {
        curr_r = Rational(curr - 1) / den;
      }
      curr_r = curr_r * pow_ten;
      cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
    }
    else
    {
      Assert(esign != 0);
      // update lower/upper
      if (esign == -1)
      {
        upper = curr;
      }
      else if (esign == 1)
      {
        lower = curr;
      }
    }
  } while (cret.isNull());
  return cret;
}

void printRationalApprox(const char* c, Node cr, unsigned prec)
{
  if (!cr.isConst())
  {
    Assert(false) << "printRationalApprox: non-constant input " << cr;
    Trace(c) << cr;
    return;
  }
  Node ca = getApproximateConstant(cr, true, prec);
  if (ca != cr)
  {
    Trace(c) << "(+ ";
  }
  Trace(c) << ca;
  if (ca != cr)
  {
    Trace(c) << " [0,10^" << prec << "])";
  }
}

Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs)
{
  Assert(vars.size() == subs.size());
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<Node>::iterator itv;
  std::vector<TNode> visit;
  TNode cur;
  Kind ck;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited[cur] = Node::null();
      ck = cur.getKind();
      itv = std::find(vars.begin(), vars.end(), cur);
      if (itv != vars.end())
      {
        visited[cur] = subs[std::distance(vars.begin(), itv)];
      }
      else if (cur.getNumChildren() == 0)
      {
        visited[cur] = cur;
      }
      else
      {
        TheoryId ctid = theory::kindToTheoryId(ck);
        if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
             && ctid != THEORY_BUILTIN)
            || isTranscendentalKind(ck))
        {
          // Do not traverse beneath applications that belong to another theory
          // besides (core) arithmetic. Notice that transcendental function
          // applications are also not traversed here.
          visited[cur] = cur;
        }
        else
        {
          visit.push_back(cur);
          for (const Node& cn : cur)
          {
            visit.push_back(cn);
          }
        }
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        children.push_back(cur.getOperator());
      }
      for (const Node& cn : cur)
      {
        it = visited.find(cn);
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cn != it->second;
        children.push_back(it->second);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  return visited[n];
}

Node mkBounded(Node l, Node a, Node u)
{
  NodeManager* nm = NodeManager::currentNM();
  return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
}

Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }

Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }

Node negateProofLiteral(TNode n)
{
  auto nm = NodeManager::currentNM();
  switch (n.getKind())
  {
    case Kind::GT:
    {
      return nm->mkNode(Kind::LEQ, n[0], n[1]);
    }
    case Kind::LT:
    {
      return nm->mkNode(Kind::GEQ, n[0], n[1]);
    }
    case Kind::LEQ:
    {
      return nm->mkNode(Kind::GT, n[0], n[1]);
    }
    case Kind::GEQ:
    {
      return nm->mkNode(Kind::LT, n[0], n[1]);
    }
    case Kind::EQUAL:
    case Kind::NOT:
    {
      return n.negate();
    }
    default: Unhandled() << n;
  }
}

}  // 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, Alex Ozdemir, 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		* Implementation of common functions for dealing with nodes.
14		*/
15
16		#include "arith_utilities.h"
17
18		#include <cmath>
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arith {
25
26	129	Kind joinKinds(Kind k1, Kind k2)
27		{
28	129	if (k2 < k1)
29		{
30	25	return joinKinds(k2, k1);
31		}
32	104	else if (k1 == k2)
33		{
34		return k1;
35		}
36	104	Assert(isRelationOperator(k1));
37	104	Assert(isRelationOperator(k2));
38	104	if (k1 == EQUAL)
39		{
40		if (k2 == LEQ \|\| k2 == GEQ)
41		{
42		return k1;
43		}
44		}
45	104	else if (k1 == LT)
46		{
47	36	if (k2 == LEQ)
48		{
49	36	return k1;
50		}
51		}
52	68	else if (k1 == LEQ)
53		{
54		if (k2 == GEQ)
55		{
56		return EQUAL;
57		}
58		}
59	68	else if (k1 == GT)
60		{
61	68	if (k2 == GEQ)
62		{
63	68	return k1;
64		}
65		}
66		return UNDEFINED_KIND;
67		}
68
69		Kind transKinds(Kind k1, Kind k2)
70		{
71		if (k2 < k1)
72		{
73		return transKinds(k2, k1);
74		}
75		else if (k1 == k2)
76		{
77		return k1;
78		}
79		Assert(isRelationOperator(k1));
80		Assert(isRelationOperator(k2));
81		if (k1 == EQUAL)
82		{
83		return k2;
84		}
85		else if (k1 == LT)
86		{
87		if (k2 == LEQ)
88		{
89		return k1;
90		}
91		}
92		else if (k1 == GT)
93		{
94		if (k2 == GEQ)
95		{
96		return k1;
97		}
98		}
99		return UNDEFINED_KIND;
100		}
101
102	38999	bool isTranscendentalKind(Kind k)
103		{
104		// many operators are eliminated during rewriting
105	38999	Assert(k != TANGENT && k != COSINE && k != COSECANT
106		&& k != SECANT && k != COTANGENT);
107	38999	return k == EXPONENTIAL \|\| k == SINE \|\| k == PI;
108		}
109
110	1951	Node getApproximateConstant(Node c, bool isLower, unsigned prec)
111		{
112	1951	if (!c.isConst())
113		{
114		Assert(false) << "getApproximateConstant: non-constant input " << c;
115		return Node::null();
116		}
117	3902	Rational cr = c.getConst<Rational>();
118
119	1951	unsigned lower = 0;
120	1951	unsigned upper = std::pow(10, prec);
121
122	3902	Rational den = Rational(upper);
123	1951	if (cr.getDenominator() < den.getNumerator())
124		{
125		// denominator is not more than precision, we return it
126	916	return c;
127		}
128
129	1035	int csign = cr.sgn();
130	1035	Assert(csign != 0);
131	1035	if (csign == -1)
132		{
133	20	cr = -cr;
134		}
135	2070	Rational one = Rational(1);
136	2070	Rational ten = Rational(10);
137	2070	Rational pow_ten = Rational(1);
138		// inefficient for large numbers
139	5061	while (cr >= one)
140		{
141	2013	cr = cr / ten;
142	2013	pow_ten = pow_ten * ten;
143		}
144	2070	Rational allow_err = one / den;
145
146		// now do binary search
147	2070	Rational two = Rational(2);
148	1035	NodeManager* nm = NodeManager::currentNM();
149	2070	Node cret;
150	14309	do
151		{
152	15344	unsigned curr = (lower + upper) / 2;
153	30688	Rational curr_r = Rational(curr) / den;
154	30688	Rational err = cr - curr_r;
155	15344	int esign = err.sgn();
156	15344	if (err.abs() <= allow_err)
157		{
158	1035	if (esign == 1 && !isLower)
159		{
160		curr_r = Rational(curr + 1) / den;
161		}
162	1035	else if (esign == -1 && isLower)
163		{
164	225	curr_r = Rational(curr - 1) / den;
165		}
166	1035	curr_r = curr_r * pow_ten;
167	1035	cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
168		}
169		else
170		{
171	14309	Assert(esign != 0);
172		// update lower/upper
173	14309	if (esign == -1)
174		{
175	7144	upper = curr;
176		}
177	7165	else if (esign == 1)
178		{
179	7165	lower = curr;
180		}
181		}
182	15344	} while (cret.isNull());
183	1035	return cret;
184		}
185
186	1951	void printRationalApprox(const char* c, Node cr, unsigned prec)
187		{
188	1951	if (!cr.isConst())
189		{
190		Assert(false) << "printRationalApprox: non-constant input " << cr;
191		Trace(c) << cr;
192		return;
193		}
194	3902	Node ca = getApproximateConstant(cr, true, prec);
195	1951	if (ca != cr)
196		{
197	1035	Trace(c) << "(+ ";
198		}
199	1951	Trace(c) << ca;
200	1951	if (ca != cr)
201		{
202	1035	Trace(c) << " [0,10^" << prec << "])";
203		}
204		}
205
206	5685	Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs)
207		{
208	5685	Assert(vars.size() == subs.size());
209	5685	NodeManager* nm = NodeManager::currentNM();
210	11370	std::unordered_map<TNode, Node> visited;
211	5685	std::unordered_map<TNode, Node>::iterator it;
212	5685	std::vector<Node>::iterator itv;
213	11370	std::vector<TNode> visit;
214	11370	TNode cur;
215		Kind ck;
216	5685	visit.push_back(n);
217	36372	do
218		{
219	42057	cur = visit.back();
220	42057	visit.pop_back();
221	42057	it = visited.find(cur);
222
223	42057	if (it == visited.end())
224		{
225	27899	visited[cur] = Node::null();
226	27899	ck = cur.getKind();
227	27899	itv = std::find(vars.begin(), vars.end(), cur);
228	27899	if (itv != vars.end())
229		{
230	4730	visited[cur] = subs[std::distance(vars.begin(), itv)];
231		}
232	23169	else if (cur.getNumChildren() == 0)
233		{
234	9188	visited[cur] = cur;
235		}
236		else
237		{
238	13981	TheoryId ctid = theory::kindToTheoryId(ck);
239	18474	if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
240	1832	&& ctid != THEORY_BUILTIN)
241	27904	\|\| isTranscendentalKind(ck))
242		{
243		// Do not traverse beneath applications that belong to another theory
244		// besides (core) arithmetic. Notice that transcendental function
245		// applications are also not traversed here.
246	1084	visited[cur] = cur;
247		}
248		else
249		{
250	12897	visit.push_back(cur);
251	36372	for (const Node& cn : cur)
252		{
253	23475	visit.push_back(cn);
254		}
255		}
256		}
257		}
258	14158	else if (it->second.isNull())
259		{
260	25794	Node ret = cur;
261	12897	bool childChanged = false;
262	25794	std::vector<Node> children;
263	12897	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
264		{
265		children.push_back(cur.getOperator());
266		}
267	36372	for (const Node& cn : cur)
268		{
269	23475	it = visited.find(cn);
270	23475	Assert(it != visited.end());
271	23475	Assert(!it->second.isNull());
272	23475	childChanged = childChanged \|\| cn != it->second;
273	23475	children.push_back(it->second);
274		}
275	12897	if (childChanged)
276		{
277	6573	ret = nm->mkNode(cur.getKind(), children);
278		}
279	12897	visited[cur] = ret;
280		}
281	42057	} while (!visit.empty());
282	5685	Assert(visited.find(n) != visited.end());
283	5685	Assert(!visited.find(n)->second.isNull());
284	11370	return visited[n];
285		}
286
287	460	Node mkBounded(Node l, Node a, Node u)
288		{
289	460	NodeManager* nm = NodeManager::currentNM();
290	460	return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
291		}
292
293	1427	Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
294
295	59636	Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
296
297	88778	Node negateProofLiteral(TNode n)
298		{
299	88778	auto nm = NodeManager::currentNM();
300	88778	switch (n.getKind())
301		{
302		case Kind::GT:
303		{
304		return nm->mkNode(Kind::LEQ, n[0], n[1]);
305		}
306		case Kind::LT:
307		{
308		return nm->mkNode(Kind::GEQ, n[0], n[1]);
309		}
310	42653	case Kind::LEQ:
311		{
312	42653	return nm->mkNode(Kind::GT, n[0], n[1]);
313		}
314	41556	case Kind::GEQ:
315		{
316	41556	return nm->mkNode(Kind::LT, n[0], n[1]);
317		}
318	4569	case Kind::EQUAL:
319		case Kind::NOT:
320		{
321	4569	return n.negate();
322		}
323		default: Unhandled() << n;
324		}
325		}
326
327		} // namespace arith
328		} // namespace theory
329	28191	} // namespace cvc5