Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_utilities.cpp	Lines:	127	157	80.9 %
Date:	2021-11-07	Branches:	233	634	36.8 %


/******************************************************************************
 * 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, const Subs& sub)
{
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, Node> visited;
  std::vector<TNode> visit;
  visit.push_back(n);
  do
  {
    TNode cur = visit.back();
    visit.pop_back();
    auto it = visited.find(cur);

    if (it == visited.end())
    {
      visited[cur] = Node::null();
      Kind ck = cur.getKind();
      auto s = sub.find(cur);
      if (s)
      {
        visited[cur] = *s;
      }
      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	8176	Kind joinKinds(Kind k1, Kind k2)
27		{
28	8176	if (k2 < k1)
29		{
30	2508	return joinKinds(k2, k1);
31		}
32	5668	else if (k1 == k2)
33		{
34		return k1;
35		}
36	5668	Assert(isRelationOperator(k1));
37	5668	Assert(isRelationOperator(k2));
38	5668	if (k1 == EQUAL)
39		{
40	1106	if (k2 == LEQ \|\| k2 == GEQ)
41		{
42	1106	return k1;
43		}
44		}
45	4562	else if (k1 == LT)
46		{
47	982	if (k2 == LEQ)
48		{
49	982	return k1;
50		}
51		}
52	3580	else if (k1 == LEQ)
53		{
54	12	if (k2 == GEQ)
55		{
56	12	return EQUAL;
57		}
58		}
59	3568	else if (k1 == GT)
60		{
61	3568	if (k2 == GEQ)
62		{
63	3568	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	54242	bool isTranscendentalKind(Kind k)
103		{
104		// many operators are eliminated during rewriting
105	54242	Assert(k != TANGENT && k != COSINE && k != COSECANT
106		&& k != SECANT && k != COTANGENT);
107	54242	return k == EXPONENTIAL \|\| k == SINE \|\| k == PI;
108		}
109
110	2007	Node getApproximateConstant(Node c, bool isLower, unsigned prec)
111		{
112	2007	if (!c.isConst())
113		{
114		Assert(false) << "getApproximateConstant: non-constant input " << c;
115		return Node::null();
116		}
117	4014	Rational cr = c.getConst<Rational>();
118
119	2007	unsigned lower = 0;
120	2007	unsigned upper = std::pow(10, prec);
121
122	4014	Rational den = Rational(upper);
123	2007	if (cr.getDenominator() < den.getNumerator())
124		{
125		// denominator is not more than precision, we return it
126	972	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	2007	void printRationalApprox(const char* c, Node cr, unsigned prec)
187		{
188	2007	if (!cr.isConst())
189		{
190		Assert(false) << "printRationalApprox: non-constant input " << cr;
191		Trace(c) << cr;
192		return;
193		}
194	4014	Node ca = getApproximateConstant(cr, true, prec);
195	2007	if (ca != cr)
196		{
197	1035	Trace(c) << "(+ ";
198		}
199	2007	Trace(c) << ca;
200	2007	if (ca != cr)
201		{
202	1035	Trace(c) << " [0,10^" << prec << "])";
203		}
204		}
205
206	8164	Node arithSubstitute(Node n, const Subs& sub)
207		{
208	8164	NodeManager* nm = NodeManager::currentNM();
209	16328	std::unordered_map<TNode, Node> visited;
210	16328	std::vector<TNode> visit;
211	8164	visit.push_back(n);
212	53968	do
213		{
214	124264	TNode cur = visit.back();
215	62132	visit.pop_back();
216	62132	auto it = visited.find(cur);
217
218	62132	if (it == visited.end())
219		{
220	40839	visited[cur] = Node::null();
221	40839	Kind ck = cur.getKind();
222	81678	auto s = sub.find(cur);
223	40839	if (s)
224		{
225	8653	visited[cur] = *s;
226		}
227	32186	else if (cur.getNumChildren() == 0)
228		{
229	12038	visited[cur] = cur;
230		}
231		else
232		{
233	20148	TheoryId ctid = theory::kindToTheoryId(ck);
234	26033	if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
235	2547	&& ctid != THEORY_BUILTIN)
236	40143	\|\| isTranscendentalKind(ck))
237		{
238		// Do not traverse beneath applications that belong to another theory
239		// besides (core) arithmetic. Notice that transcendental function
240		// applications are also not traversed here.
241	1177	visited[cur] = cur;
242		}
243		else
244		{
245	18971	visit.push_back(cur);
246	53968	for (const Node& cn : cur)
247		{
248	34997	visit.push_back(cn);
249		}
250		}
251		}
252		}
253	21293	else if (it->second.isNull())
254		{
255	37942	Node ret = cur;
256	18971	bool childChanged = false;
257	37942	std::vector<Node> children;
258	18971	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
259		{
260		children.push_back(cur.getOperator());
261		}
262	53968	for (const Node& cn : cur)
263		{
264	34997	it = visited.find(cn);
265	34997	Assert(it != visited.end());
266	34997	Assert(!it->second.isNull());
267	34997	childChanged = childChanged \|\| cn != it->second;
268	34997	children.push_back(it->second);
269		}
270	18971	if (childChanged)
271		{
272	12592	ret = nm->mkNode(cur.getKind(), children);
273		}
274	18971	visited[cur] = ret;
275		}
276	62132	} while (!visit.empty());
277	8164	Assert(visited.find(n) != visited.end());
278	8164	Assert(!visited.find(n)->second.isNull());
279	16328	return visited[n];
280		}
281
282	466	Node mkBounded(Node l, Node a, Node u)
283		{
284	466	NodeManager* nm = NodeManager::currentNM();
285	466	return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
286		}
287
288	281	Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
289
290	4075	Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
291
292	87028	Node negateProofLiteral(TNode n)
293		{
294	87028	auto nm = NodeManager::currentNM();
295	87028	switch (n.getKind())
296		{
297		case Kind::GT:
298		{
299		return nm->mkNode(Kind::LEQ, n[0], n[1]);
300		}
301		case Kind::LT:
302		{
303		return nm->mkNode(Kind::GEQ, n[0], n[1]);
304		}
305	43123	case Kind::LEQ:
306		{
307	43123	return nm->mkNode(Kind::GT, n[0], n[1]);
308		}
309	43097	case Kind::GEQ:
310		{
311	43097	return nm->mkNode(Kind::LT, n[0], n[1]);
312		}
313	808	case Kind::EQUAL:
314		case Kind::NOT:
315		{
316	808	return n.negate();
317		}
318		default: Unhandled() << n;
319		}
320		}
321
322		} // namespace arith
323		} // namespace theory
324	31137	} // namespace cvc5