1 /******************************************************************************
2 * Top contributors (to current version):
3 * Tim King, Andrew Reynolds, Andres Noetzli
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Common functions for dealing with nodes.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
19 #define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
21 #include <unordered_map>
22 #include <unordered_set>
25 #include "context/cdhashset.h"
26 #include "expr/node.h"
27 #include "expr/subs.h"
28 #include "theory/arith/arithvar.h"
29 #include "util/dense_map.h"
30 #include "util/integer.h"
31 #include "util/rational.h"
38 typedef std::unordered_set
<Node
> NodeSet
;
39 typedef std::unordered_set
<TNode
> TNodeSet
;
40 typedef context::CDHashSet
<Node
> CDNodeSet
;
42 //Maps from Nodes -> ArithVars, and vice versa
43 typedef std::unordered_map
<Node
, ArithVar
> NodeToArithVarMap
;
44 typedef DenseMap
<Node
> ArithVarToNodeMap
;
46 inline Node
mkRationalNode(const Rational
& q
){
47 return NodeManager::currentNM()->mkConst
<Rational
>(q
);
50 inline Node
mkBoolNode(bool b
){
51 return NodeManager::currentNM()->mkConst
<bool>(b
);
54 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
55 inline bool isRelationOperator(Kind k
){
71 * Given a relational kind, k, return the kind k' s.t.
72 * swapping the lefthand and righthand side is equivalent.
74 * The following equivalence should hold,
75 * (k l r) <=> (k' r l)
77 inline Kind
reverseRelationKind(Kind k
){
83 case EQUAL
: return EQUAL
;
92 inline bool evaluateConstantPredicate(Kind k
, const Rational
& left
, const Rational
& right
){
96 case LT
: return left
< right
;
97 case LEQ
: return left
<= right
;
98 case EQUAL
: return left
== right
;
99 case GEQ
: return left
>= right
;
100 case GT
: return left
> right
;
108 * Returns the appropriate coefficient for the infinitesimal given the kind
109 * for an arithmetic atom inorder to represent strict inequalities as inequalities.
110 * x < c becomes x <= c + (-1) * \f$ \delta \f$
111 * x > c becomes x >= x + ( 1) * \f$ \delta \f$
112 * Non-strict inequalities have a coefficient of zero.
114 inline int deltaCoeff(Kind k
){
126 * Given a literal to TheoryArith return a single kind to
127 * to indicate its underlying structure.
128 * The function returns the following in each case:
129 * - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
130 * - (NOT (EQUAL left right)) -> DISTINCT
131 * - (NOT (LEQ left right)) -> GT
132 * - (NOT (GEQ left right)) -> LT
133 * - (NOT (LT left right)) -> GEQ
134 * - (NOT (GT left right)) -> LEQ
135 * If none of these match, it returns UNDEFINED_KIND.
137 inline Kind
oldSimplifiedKind(TNode literal
){
138 switch(literal
.getKind()){
144 return literal
.getKind();
147 TNode atom
= literal
[0];
148 switch(atom
.getKind()){
149 case kind::LEQ
: //(not (LEQ x c)) <=> (GT x c)
151 case kind::GEQ
: //(not (GEQ x c)) <=> (LT x c)
153 case kind::LT
: //(not (LT x c)) <=> (GEQ x c)
155 case kind::GT
: //(not (GT x c) <=> (LEQ x c)
158 return kind::DISTINCT
;
161 return kind::UNDEFINED_KIND
;
166 return kind::UNDEFINED_KIND
;
170 inline Kind
negateKind(Kind k
){
172 case kind::LT
: return kind::GEQ
;
173 case kind::GT
: return kind::LEQ
;
174 case kind::LEQ
: return kind::GT
;
175 case kind::GEQ
: return kind::LT
;
176 case kind::EQUAL
: return kind::DISTINCT
;
177 case kind::DISTINCT
: return kind::EQUAL
;
179 return kind::UNDEFINED_KIND
;
183 inline Node
negateConjunctionAsClause(TNode conjunction
){
184 Assert(conjunction
.getKind() == kind::AND
);
185 NodeBuilder
orBuilder(kind::OR
);
187 for(TNode::iterator i
= conjunction
.begin(), end
=conjunction
.end(); i
!= end
; ++i
){
189 Node negatedChild
= NodeBuilder(kind::NOT
) << (child
);
190 orBuilder
<< negatedChild
;
195 inline Node
maybeUnaryConvert(NodeBuilder
& builder
)
197 Assert(builder
.getKind() == kind::OR
|| builder
.getKind() == kind::AND
198 || builder
.getKind() == kind::PLUS
|| builder
.getKind() == kind::MULT
);
199 Assert(builder
.getNumChildren() >= 1);
200 if(builder
.getNumChildren() == 1){
207 inline void flattenAnd(Node n
, std::vector
<TNode
>& out
){
208 Assert(n
.getKind() == kind::AND
);
209 for(Node::iterator i
=n
.begin(), i_end
=n
.end(); i
!= i_end
; ++i
){
211 if(curr
.getKind() == kind::AND
){
212 flattenAnd(curr
, out
);
219 inline Node
flattenAnd(Node n
){
220 std::vector
<TNode
> out
;
222 return NodeManager::currentNM()->mkNode(kind::AND
, out
);
225 // Returns an node that is the identity of a select few kinds.
226 inline Node
getIdentity(Kind k
){
229 return mkBoolNode(true);
231 return mkRationalNode(0);
233 case kind::NONLINEAR_MULT
:
234 return mkRationalNode(1);
235 default: Unreachable(); return Node::null(); // silence warning
239 inline Node
safeConstructNary(NodeBuilder
& nb
)
241 switch (nb
.getNumChildren()) {
243 return getIdentity(nb
.getKind());
251 inline Node
safeConstructNary(Kind k
, const std::vector
<Node
>& children
) {
252 switch (children
.size()) {
254 return getIdentity(k
);
258 return NodeManager::currentNM()->mkNode(k
, children
);
262 // Returns the multiplication of a and b.
263 inline Node
mkMult(Node a
, Node b
) {
264 return NodeManager::currentNM()->mkNode(kind::MULT
, a
, b
);
267 // Return a constraint that is equivalent to term being is in the range
268 // [start, end). This includes start and excludes end.
269 inline Node
mkInRange(Node term
, Node start
, Node end
) {
270 NodeManager
* nm
= NodeManager::currentNM();
271 Node above_start
= nm
->mkNode(kind::LEQ
, start
, term
);
272 Node below_end
= nm
->mkNode(kind::LT
, term
, end
);
273 return nm
->mkNode(kind::AND
, above_start
, below_end
);
276 // Creates an expression that constrains q to be equal to one of two expressions
277 // when n is 0 or not. Useful for division by 0 logic.
278 // (ite (= n 0) (= q if_zero) (= q not_zero))
279 inline Node
mkOnZeroIte(Node n
, Node q
, Node if_zero
, Node not_zero
) {
280 Node zero
= mkRationalNode(0);
281 return n
.eqNode(zero
).iteNode(q
.eqNode(if_zero
), q
.eqNode(not_zero
));
286 return NodeManager::currentNM()->mkNullaryOperator(
287 NodeManager::currentNM()->realType(), kind::PI
);
289 /** Join kinds, where k1 and k2 are arithmetic relations returns an
290 * arithmetic relation ret such that
291 * if (a <k1> b) and (a <k2> b), then (a <ret> b).
293 Kind
joinKinds(Kind k1
, Kind k2
);
295 /** Transitive kinds, where k1 and k2 are arithmetic relations returns an
296 * arithmetic relation ret such that
297 * if (a <k1> b) and (b <k2> c) then (a <ret> c).
299 Kind
transKinds(Kind k1
, Kind k2
);
301 /** Is k a transcendental function kind? */
302 bool isTranscendentalKind(Kind k
);
304 * Get a lower/upper approximation of the constant r within the given
305 * level of precision. In other words, this returns a constant c' such that
306 * c' <= c <= c' + 1/(10^prec) if isLower is true, or
307 * c' + 1/(10^prec) <= c <= c' if isLower is false.
308 * where c' is a rational of the form n/d for some n and d <= 10^prec.
310 Node
getApproximateConstant(Node c
, bool isLower
, unsigned prec
);
312 /** print rational approximation of cr with precision prec on trace c */
313 void printRationalApprox(const char* c
, Node cr
, unsigned prec
= 5);
315 /** Arithmetic substitute
317 * This computes the substitution n { subs }, but with the caveat
318 * that subterms of n that belong to a theory other than arithmetic are
319 * not traversed. In other words, terms that belong to other theories are
320 * treated as atomic variables. For example:
321 * (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3.
323 Node
arithSubstitute(Node n
, const Subs
& sub
);
325 /** Make the node u >= a ^ a >= l */
326 Node
mkBounded(Node l
, Node a
, Node u
);
328 Rational
leastIntGreaterThan(const Rational
&);
330 Rational
greatestIntLessThan(const Rational
&);
332 /** Negates a node in arithmetic proof normal form. */
333 Node
negateProofLiteral(TNode n
);
336 } // namespace theory
339 #endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */