Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_utilities.h	Lines:	74	111	66.7 %
Date:	2021-09-10	Branches:	52	139	37.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Andrew Reynolds, 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.
 * ****************************************************************************
 *
 * Common functions for dealing with nodes.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
#define CVC5__THEORY__ARITH__ARITH_UTILITIES_H

#include <unordered_map>
#include <unordered_set>
#include <vector>

#include "context/cdhashset.h"
#include "expr/node.h"
#include "theory/arith/arithvar.h"
#include "util/dense_map.h"
#include "util/integer.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace arith {

//Sets of Nodes
typedef std::unordered_set<Node> NodeSet;
typedef std::unordered_set<TNode> TNodeSet;
typedef context::CDHashSet<Node> CDNodeSet;

//Maps from Nodes -> ArithVars, and vice versa
typedef std::unordered_map<Node, ArithVar> NodeToArithVarMap;
typedef DenseMap<Node> ArithVarToNodeMap;

inline Node mkRationalNode(const Rational& q){
  return NodeManager::currentNM()->mkConst<Rational>(q);
}

inline Node mkBoolNode(bool b){
  return NodeManager::currentNM()->mkConst<bool>(b);
}

/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
inline bool isRelationOperator(Kind k){
  using namespace kind;

  switch(k){
  case LT:
  case LEQ:
  case EQUAL:
  case GEQ:
  case GT:
    return true;
  default:
    return false;
  }
}

/**
 * Given a relational kind, k, return the kind k' s.t.
 * swapping the lefthand and righthand side is equivalent.
 *
 * The following equivalence should hold,
 *   (k l r) <=> (k' r l)
 */
inline Kind reverseRelationKind(Kind k){
  using namespace kind;

  switch(k){
  case LT:    return GT;
  case LEQ:   return GEQ;
  case EQUAL: return EQUAL;
  case GEQ:   return LEQ;
  case GT:    return LT;

  default:
    Unreachable();
  }
}

inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
  using namespace kind;

  switch(k){
  case LT:    return left <  right;
  case LEQ:   return left <= right;
  case EQUAL: return left == right;
  case GEQ:   return left >= right;
  case GT:    return left >  right;
  default:
    Unreachable();
    return true;
  }
}

/**
 * Returns the appropriate coefficient for the infinitesimal given the kind
 * for an arithmetic atom inorder to represent strict inequalities as inequalities.
 *   x < c  becomes  x <= c + (-1) * \f$ \delta \f$
 *   x > c  becomes  x >= x + ( 1) * \f$ \delta \f$
 * Non-strict inequalities have a coefficient of zero.
 */
inline int deltaCoeff(Kind k){
  switch(k){
  case kind::LT:
    return -1;
  case kind::GT:
    return 1;
  default:
    return 0;
  }
}

/**
 * Given a literal to TheoryArith return a single kind to
 * to indicate its underlying structure.
 * The function returns the following in each case:
 * - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
 * - (NOT (EQUAL left right)) -> DISTINCT
 * - (NOT (LEQ left right))   -> GT
 * - (NOT (GEQ left right))   -> LT
 * - (NOT (LT left right))    -> GEQ
 * - (NOT (GT left right))    -> LEQ
 * If none of these match, it returns UNDEFINED_KIND.
 */
inline Kind oldSimplifiedKind(TNode literal){
  switch(literal.getKind()){
  case kind::LT:
  case kind::GT:
  case kind::LEQ:
  case kind::GEQ:
  case kind::EQUAL:
    return literal.getKind();
  case  kind::NOT:
    {
      TNode atom = literal[0];
      switch(atom.getKind()){
      case  kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
        return  kind::GT;
      case  kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
        return  kind::LT;
      case  kind::LT: //(not (LT x c)) <=> (GEQ x c)
        return  kind::GEQ;
      case  kind::GT: //(not (GT x c) <=> (LEQ x c)
        return  kind::LEQ;
      case  kind::EQUAL:
        return  kind::DISTINCT;
      default:
        Unreachable();
        return  kind::UNDEFINED_KIND;
      }
    }
  default:
    Unreachable();
    return kind::UNDEFINED_KIND;
  }
}

inline Kind negateKind(Kind k){
  switch(k){
  case kind::LT:       return kind::GEQ;
  case kind::GT:       return kind::LEQ;
  case kind::LEQ:      return kind::GT;
  case kind::GEQ:      return kind::LT;
  case kind::EQUAL:    return kind::DISTINCT;
  case kind::DISTINCT: return kind::EQUAL;
  default:
    return kind::UNDEFINED_KIND;
  }
}

inline Node negateConjunctionAsClause(TNode conjunction){
  Assert(conjunction.getKind() == kind::AND);
  NodeBuilder orBuilder(kind::OR);

  for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
    TNode child = *i;
    Node negatedChild = NodeBuilder(kind::NOT) << (child);
    orBuilder << negatedChild;
  }
  return orBuilder;
}

inline Node maybeUnaryConvert(NodeBuilder& builder)
{
  Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
         || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT);
  Assert(builder.getNumChildren() >= 1);
  if(builder.getNumChildren() == 1){
    return builder[0];
  }else{
    return builder;
  }
}

inline void flattenAnd(Node n, std::vector<TNode>& out){
  Assert(n.getKind() == kind::AND);
  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
    Node curr = *i;
    if(curr.getKind() == kind::AND){
      flattenAnd(curr, out);
    }else{
      out.push_back(curr);
    }
  }
}

inline Node flattenAnd(Node n){
  std::vector<TNode> out;
  flattenAnd(n, out);
  return NodeManager::currentNM()->mkNode(kind::AND, out);
}

// Returns an node that is the identity of a select few kinds.
inline Node getIdentity(Kind k){
  switch(k){
  case kind::AND:
    return mkBoolNode(true);
  case kind::PLUS:
    return mkRationalNode(0);
  case kind::MULT:
  case kind::NONLINEAR_MULT:
    return mkRationalNode(1);
  default: Unreachable(); return Node::null();  // silence warning
  }
}

inline Node safeConstructNary(NodeBuilder& nb)
{
  switch (nb.getNumChildren()) {
    case 0:
      return getIdentity(nb.getKind());
    case 1:
      return nb[0];
    default:
      return (Node)nb;
  }
}

inline Node safeConstructNary(Kind k, const std::vector<Node>& children) {
  switch (children.size()) {
    case 0:
      return getIdentity(k);
    case 1:
      return children[0];
    default:
      return NodeManager::currentNM()->mkNode(k, children);
  }
}

// Returns the multiplication of a and b.
inline Node mkMult(Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::MULT, a, b);
}

// Return a constraint that is equivalent to term being is in the range
// [start, end). This includes start and excludes end.
inline Node mkInRange(Node term, Node start, Node end) {
  NodeManager* nm = NodeManager::currentNM();
  Node above_start = nm->mkNode(kind::LEQ, start, term);
  Node below_end = nm->mkNode(kind::LT, term, end);
  return nm->mkNode(kind::AND, above_start, below_end);
}

// Creates an expression that constrains q to be equal to one of two expressions
// when n is 0 or not. Useful for division by 0 logic.
//   (ite (= n 0) (= q if_zero) (= q not_zero))
inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) {
  Node zero = mkRationalNode(0);
  return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero));
}

inline Node mkPi()
{
  return NodeManager::currentNM()->mkNullaryOperator(
      NodeManager::currentNM()->realType(), kind::PI);
}
/** Join kinds, where k1 and k2 are arithmetic relations returns an
 * arithmetic relation ret such that
 * if (a <k1> b) and (a <k2> b), then (a <ret> b).
 */
Kind joinKinds(Kind k1, Kind k2);

/** Transitive kinds, where k1 and k2 are arithmetic relations returns an
 * arithmetic relation ret such that
 * if (a <k1> b) and (b <k2> c) then (a <ret> c).
 */
Kind transKinds(Kind k1, Kind k2);

/** Is k a transcendental function kind? */
bool isTranscendentalKind(Kind k);
/**
 * Get a lower/upper approximation of the constant r within the given
 * level of precision. In other words, this returns a constant c' such that
 *   c' <= c <= c' + 1/(10^prec) if isLower is true, or
 *   c' + 1/(10^prec) <= c <= c' if isLower is false.
 * where c' is a rational of the form n/d for some n and d <= 10^prec.
 */
Node getApproximateConstant(Node c, bool isLower, unsigned prec);

/** print rational approximation of cr with precision prec on trace c */
void printRationalApprox(const char* c, Node cr, unsigned prec = 5);

/** Arithmetic substitute
 *
 * This computes the substitution n { vars -> subs }, but with the caveat
 * that subterms of n that belong to a theory other than arithmetic are
 * not traversed. In other words, terms that belong to other theories are
 * treated as atomic variables. For example:
 *   (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3.
 */
Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs);

/** Make the node u >= a ^ a >= l */
Node mkBounded(Node l, Node a, Node u);

Rational leastIntGreaterThan(const Rational&);

Rational greatestIntLessThan(const Rational&);

/** Negates a node in arithmetic proof normal form. */
Node negateProofLiteral(TNode n);

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

#endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Andrew Reynolds, 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		* Common functions for dealing with nodes.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
19		#define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
20
21		#include <unordered_map>
22		#include <unordered_set>
23		#include <vector>
24
25		#include "context/cdhashset.h"
26		#include "expr/node.h"
27		#include "theory/arith/arithvar.h"
28		#include "util/dense_map.h"
29		#include "util/integer.h"
30		#include "util/rational.h"
31
32		namespace cvc5 {
33		namespace theory {
34		namespace arith {
35
36		//Sets of Nodes
37		typedef std::unordered_set<Node> NodeSet;
38		typedef std::unordered_set<TNode> TNodeSet;
39		typedef context::CDHashSet<Node> CDNodeSet;
40
41		//Maps from Nodes -> ArithVars, and vice versa
42		typedef std::unordered_map<Node, ArithVar> NodeToArithVarMap;
43		typedef DenseMap<Node> ArithVarToNodeMap;
44
45	154940363	inline Node mkRationalNode(const Rational& q){
46	154940363	return NodeManager::currentNM()->mkConst<Rational>(q);
47		}
48
49	9025	inline Node mkBoolNode(bool b){
50	9025	return NodeManager::currentNM()->mkConst<bool>(b);
51		}
52
53		/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
54	236876542	inline bool isRelationOperator(Kind k){
55		using namespace kind;
56
57	236876542	switch(k){
58	13166912	case LT:
59		case LEQ:
60		case EQUAL:
61		case GEQ:
62		case GT:
63	13166912	return true;
64	223709630	default:
65	223709630	return false;
66		}
67		}
68
69		/**
70		* Given a relational kind, k, return the kind k' s.t.
71		* swapping the lefthand and righthand side is equivalent.
72		*
73		* The following equivalence should hold,
74		* (k l r) <=> (k' r l)
75		*/
76	44146	inline Kind reverseRelationKind(Kind k){
77		using namespace kind;
78
79	44146	switch(k){
80	2943	case LT: return GT;
81	387	case LEQ: return GEQ;
82	9721	case EQUAL: return EQUAL;
83	25443	case GEQ: return LEQ;
84	5652	case GT: return LT;
85
86		default:
87		Unreachable();
88		}
89		}
90
91	342039	inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
92		using namespace kind;
93
94	342039	switch(k){
95		case LT: return left < right;
96	28050	case LEQ: return left <= right;
97	194945	case EQUAL: return left == right;
98	119044	case GEQ: return left >= right;
99		case GT: return left > right;
100		default:
101		Unreachable();
102		return true;
103		}
104		}
105
106		/**
107		* Returns the appropriate coefficient for the infinitesimal given the kind
108		* for an arithmetic atom inorder to represent strict inequalities as inequalities.
109		* x < c becomes x <= c + (-1) * \f$ \delta \f$
110		* x > c becomes x >= x + ( 1) * \f$ \delta \f$
111		* Non-strict inequalities have a coefficient of zero.
112		*/
113	1082088	inline int deltaCoeff(Kind k){
114	1082088	switch(k){
115	285720	case kind::LT:
116	285720	return -1;
117		case kind::GT:
118		return 1;
119	796368	default:
120	796368	return 0;
121		}
122		}
123
124		/**
125		* Given a literal to TheoryArith return a single kind to
126		* to indicate its underlying structure.
127		* The function returns the following in each case:
128		* - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
129		* - (NOT (EQUAL left right)) -> DISTINCT
130		* - (NOT (LEQ left right)) -> GT
131		* - (NOT (GEQ left right)) -> LT
132		* - (NOT (LT left right)) -> GEQ
133		* - (NOT (GT left right)) -> LEQ
134		* If none of these match, it returns UNDEFINED_KIND.
135		*/
136	1641	inline Kind oldSimplifiedKind(TNode literal){
137	1641	switch(literal.getKind()){
138	1641	case kind::LT:
139		case kind::GT:
140		case kind::LEQ:
141		case kind::GEQ:
142		case kind::EQUAL:
143	1641	return literal.getKind();
144		case kind::NOT:
145		{
146		TNode atom = literal[0];
147		switch(atom.getKind()){
148		case kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
149		return kind::GT;
150		case kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
151		return kind::LT;
152		case kind::LT: //(not (LT x c)) <=> (GEQ x c)
153		return kind::GEQ;
154		case kind::GT: //(not (GT x c) <=> (LEQ x c)
155		return kind::LEQ;
156		case kind::EQUAL:
157		return kind::DISTINCT;
158		default:
159		Unreachable();
160		return kind::UNDEFINED_KIND;
161		}
162		}
163		default:
164		Unreachable();
165		return kind::UNDEFINED_KIND;
166		}
167		}
168
169	40964	inline Kind negateKind(Kind k){
170	40964	switch(k){
171		case kind::LT: return kind::GEQ;
172		case kind::GT: return kind::LEQ;
173	15418	case kind::LEQ: return kind::GT;
174	25535	case kind::GEQ: return kind::LT;
175	11	case kind::EQUAL: return kind::DISTINCT;
176		case kind::DISTINCT: return kind::EQUAL;
177		default:
178		return kind::UNDEFINED_KIND;
179		}
180		}
181
182		inline Node negateConjunctionAsClause(TNode conjunction){
183		Assert(conjunction.getKind() == kind::AND);
184		NodeBuilder orBuilder(kind::OR);
185
186		for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
187		TNode child = *i;
188		Node negatedChild = NodeBuilder(kind::NOT) << (child);
189		orBuilder << negatedChild;
190		}
191		return orBuilder;
192		}
193
194		inline Node maybeUnaryConvert(NodeBuilder& builder)
195		{
196		Assert(builder.getKind() == kind::OR \|\| builder.getKind() == kind::AND
197		\|\| builder.getKind() == kind::PLUS \|\| builder.getKind() == kind::MULT);
198		Assert(builder.getNumChildren() >= 1);
199		if(builder.getNumChildren() == 1){
200		return builder[0];
201		}else{
202		return builder;
203		}
204		}
205
206	5131	inline void flattenAnd(Node n, std::vector<TNode>& out){
207	5131	Assert(n.getKind() == kind::AND);
208	19559	for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
209	28856	Node curr = *i;
210	14428	if(curr.getKind() == kind::AND){
211	3028	flattenAnd(curr, out);
212		}else{
213	11400	out.push_back(curr);
214		}
215		}
216	5131	}
217
218	2103	inline Node flattenAnd(Node n){
219	4206	std::vector<TNode> out;
220	2103	flattenAnd(n, out);
221	4206	return NodeManager::currentNM()->mkNode(kind::AND, out);
222		}
223
224		// Returns an node that is the identity of a select few kinds.
225	1569	inline Node getIdentity(Kind k){
226	1569	switch(k){
227		case kind::AND:
228		return mkBoolNode(true);
229		case kind::PLUS:
230		return mkRationalNode(0);
231	1569	case kind::MULT:
232		case kind::NONLINEAR_MULT:
233	1569	return mkRationalNode(1);
234		default: Unreachable(); return Node::null(); // silence warning
235		}
236		}
237
238	3315736	inline Node safeConstructNary(NodeBuilder& nb)
239		{
240	3315736	switch (nb.getNumChildren()) {
241		case 0:
242		return getIdentity(nb.getKind());
243	2684778	case 1:
244	2684778	return nb[0];
245	630958	default:
246	630958	return (Node)nb;
247		}
248		}
249
250	37345	inline Node safeConstructNary(Kind k, const std::vector<Node>& children) {
251	37345	switch (children.size()) {
252	1569	case 0:
253	1569	return getIdentity(k);
254	16389	case 1:
255	16389	return children[0];
256	19387	default:
257	19387	return NodeManager::currentNM()->mkNode(k, children);
258		}
259		}
260
261		// Returns the multiplication of a and b.
262		inline Node mkMult(Node a, Node b) {
263		return NodeManager::currentNM()->mkNode(kind::MULT, a, b);
264		}
265
266		// Return a constraint that is equivalent to term being is in the range
267		// [start, end). This includes start and excludes end.
268	84	inline Node mkInRange(Node term, Node start, Node end) {
269	84	NodeManager* nm = NodeManager::currentNM();
270	168	Node above_start = nm->mkNode(kind::LEQ, start, term);
271	168	Node below_end = nm->mkNode(kind::LT, term, end);
272	168	return nm->mkNode(kind::AND, above_start, below_end);
273		}
274
275		// Creates an expression that constrains q to be equal to one of two expressions
276		// when n is 0 or not. Useful for division by 0 logic.
277		// (ite (= n 0) (= q if_zero) (= q not_zero))
278		inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) {
279		Node zero = mkRationalNode(0);
280		return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero));
281		}
282
283	1656	inline Node mkPi()
284		{
285		return NodeManager::currentNM()->mkNullaryOperator(
286	1656	NodeManager::currentNM()->realType(), kind::PI);
287		}
288		/** Join kinds, where k1 and k2 are arithmetic relations returns an
289		* arithmetic relation ret such that
290		* if (a <k1> b) and (a <k2> b), then (a <ret> b).
291		*/
292		Kind joinKinds(Kind k1, Kind k2);
293
294		/** Transitive kinds, where k1 and k2 are arithmetic relations returns an
295		* arithmetic relation ret such that
296		* if (a <k1> b) and (b <k2> c) then (a <ret> c).
297		*/
298		Kind transKinds(Kind k1, Kind k2);
299
300		/** Is k a transcendental function kind? */
301		bool isTranscendentalKind(Kind k);
302		/**
303		* Get a lower/upper approximation of the constant r within the given
304		* level of precision. In other words, this returns a constant c' such that
305		* c' <= c <= c' + 1/(10^prec) if isLower is true, or
306		* c' + 1/(10^prec) <= c <= c' if isLower is false.
307		* where c' is a rational of the form n/d for some n and d <= 10^prec.
308		*/
309		Node getApproximateConstant(Node c, bool isLower, unsigned prec);
310
311		/** print rational approximation of cr with precision prec on trace c */
312		void printRationalApprox(const char* c, Node cr, unsigned prec = 5);
313
314		/** Arithmetic substitute
315		*
316		* This computes the substitution n { vars -> subs }, but with the caveat
317		* that subterms of n that belong to a theory other than arithmetic are
318		* not traversed. In other words, terms that belong to other theories are
319		* treated as atomic variables. For example:
320		* (5f(x) + 7x ){ x -> 3 } returns 5f(x) + 73.
321		*/
322		Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs);
323
324		/** Make the node u >= a ^ a >= l */
325		Node mkBounded(Node l, Node a, Node u);
326
327		Rational leastIntGreaterThan(const Rational&);
328
329		Rational greatestIntLessThan(const Rational&);
330
331		/** Negates a node in arithmetic proof normal form. */
332		Node negateProofLiteral(TNode n);
333
334		} // namespace arith
335		} // namespace theory
336		} // namespace cvc5
337
338		#endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */