src/theory/arith/arith_utilities.h

   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 "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"
  32
  33 namespace cvc5 {
  34 namespace theory {
  35 namespace arith {
  36
  37 //Sets of Nodes
  38 typedef std::unordered_set<Node> NodeSet;
  39 typedef std::unordered_set<TNode> TNodeSet;
  40 typedef context::CDHashSet<Node> CDNodeSet;
  41
  42 //Maps from Nodes -> ArithVars, and vice versa
  43 typedef std::unordered_map<Node, ArithVar> NodeToArithVarMap;
  44 typedef DenseMap<Node> ArithVarToNodeMap;
  45
  46 inline Node mkRationalNode(const Rational& q){
  47   return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, q);
  48 }
  49
  50 inline Node mkBoolNode(bool b){
  51   return NodeManager::currentNM()->mkConst<bool>(b);
  52 }
  53
  54 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
  55 inline bool isRelationOperator(Kind k){
  56   using namespace kind;
  57
  58   switch(k){
  59   case LT:
  60   case LEQ:
  61   case EQUAL:
  62   case GEQ:
  63   case GT:
  64     return true;
  65   default:
  66     return false;
  67   }
  68 }
  69
  70 /**
  71  * Given a relational kind, k, return the kind k' s.t.
  72  * swapping the lefthand and righthand side is equivalent.
  73  *
  74  * The following equivalence should hold,
  75  *   (k l r) <=> (k' r l)
  76  */
  77 inline Kind reverseRelationKind(Kind k){
  78   using namespace kind;
  79
  80   switch(k){
  81   case LT:    return GT;
  82   case LEQ:   return GEQ;
  83   case EQUAL: return EQUAL;
  84   case GEQ:   return LEQ;
  85   case GT:    return LT;
  86
  87   default:
  88     Unreachable();
  89   }
  90 }
  91
  92 inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
  93   using namespace kind;
  94
  95   switch(k){
  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;
 101   default:
 102     Unreachable();
 103     return true;
 104   }
 105 }
 106
 107 /**
 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.
 113  */
 114 inline int deltaCoeff(Kind k){
 115   switch(k){
 116   case kind::LT:
 117     return -1;
 118   case kind::GT:
 119     return 1;
 120   default:
 121     return 0;
 122   }
 123 }
 124
 125 /**
 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.
 136  */
 137 inline Kind oldSimplifiedKind(TNode literal){
 138   switch(literal.getKind()){
 139   case kind::LT:
 140   case kind::GT:
 141   case kind::LEQ:
 142   case kind::GEQ:
 143   case kind::EQUAL:
 144     return literal.getKind();
 145   case  kind::NOT:
 146     {
 147       TNode atom = literal[0];
 148       switch(atom.getKind()){
 149       case  kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
 150         return  kind::GT;
 151       case  kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
 152         return  kind::LT;
 153       case  kind::LT: //(not (LT x c)) <=> (GEQ x c)
 154         return  kind::GEQ;
 155       case  kind::GT: //(not (GT x c) <=> (LEQ x c)
 156         return  kind::LEQ;
 157       case  kind::EQUAL:
 158         return  kind::DISTINCT;
 159       default:
 160         Unreachable();
 161         return  kind::UNDEFINED_KIND;
 162       }
 163     }
 164   default:
 165     Unreachable();
 166     return kind::UNDEFINED_KIND;
 167   }
 168 }
 169
 170 inline Kind negateKind(Kind k){
 171   switch(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;
 178   default:
 179     return kind::UNDEFINED_KIND;
 180   }
 181 }
 182
 183 inline Node negateConjunctionAsClause(TNode conjunction){
 184   Assert(conjunction.getKind() == kind::AND);
 185   NodeBuilder orBuilder(kind::OR);
 186
 187   for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
 188     TNode child = *i;
 189     Node negatedChild = NodeBuilder(kind::NOT) << (child);
 190     orBuilder << negatedChild;
 191   }
 192   return orBuilder;
 193 }
 194
 195 inline Node maybeUnaryConvert(NodeBuilder& builder)
 196 {
 197   Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
 198          || builder.getKind() == kind::ADD || builder.getKind() == kind::MULT);
 199   Assert(builder.getNumChildren() >= 1);
 200   if(builder.getNumChildren() == 1){
 201     return builder[0];
 202   }else{
 203     return builder;
 204   }
 205 }
 206
 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){
 210     Node curr = *i;
 211     if(curr.getKind() == kind::AND){
 212       flattenAnd(curr, out);
 213     }else{
 214       out.push_back(curr);
 215     }
 216   }
 217 }
 218
 219 inline Node flattenAnd(Node n){
 220   std::vector<TNode> out;
 221   flattenAnd(n, out);
 222   return NodeManager::currentNM()->mkNode(kind::AND, out);
 223 }
 224
 225 // Returns an node that is the identity of a select few kinds.
 226 inline Node getIdentityType(const TypeNode& tn, Kind k)
 227 {
 228   switch (k)
 229   {
 230     case kind::ADD: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0);
 231     case kind::MULT:
 232     case kind::NONLINEAR_MULT:
 233       return NodeManager::currentNM()->mkConstRealOrInt(tn, 1);
 234     default: Unreachable(); return Node::null();  // silence warning
 235   }
 236 }
 237
 238 inline Node mkAndFromBuilder(NodeBuilder& nb)
 239 {
 240   Assert(nb.getKind() == kind::AND);
 241   switch (nb.getNumChildren()) {
 242     case 0: return mkBoolNode(true);
 243     case 1:
 244       return nb[0];
 245     default:
 246       return (Node)nb;
 247   }
 248 }
 249
 250 inline Node safeConstructNaryType(const TypeNode& tn,
 251                                   Kind k,
 252                                   const std::vector<Node>& children)
 253 {
 254   switch (children.size())
 255   {
 256     case 0: return getIdentityType(tn, k);
 257     case 1: return children[0];
 258     default: return NodeManager::currentNM()->mkNode(k, children);
 259   }
 260 }
 261
 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);
 265 }
 266
 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);
 274 }
 275
 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 = NodeManager::currentNM()->mkConstRealOrInt(n.getType(), 0);
 281   return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero));
 282 }
 283
 284 inline Node mkPi()
 285 {
 286   return NodeManager::currentNM()->mkNullaryOperator(
 287       NodeManager::currentNM()->realType(), kind::PI);
 288 }
 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).
 292  */
 293 Kind joinKinds(Kind k1, Kind k2);
 294
 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).
 298  */
 299 Kind transKinds(Kind k1, Kind k2);
 300
 301 /** Is k a transcendental function kind? */
 302 bool isTranscendentalKind(Kind k);
 303 /**
 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.
 309  */
 310 Node getApproximateConstant(Node c, bool isLower, unsigned prec);
 311
 312 /** print rational approximation of cr with precision prec on trace c */
 313 void printRationalApprox(const char* c, Node cr, unsigned prec = 5);
 314
 315 /** Arithmetic substitute
 316  *
 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.
 322  */
 323 Node arithSubstitute(Node n, const Subs& sub);
 324
 325 /** Make the node u >= a ^ a >= l */
 326 Node mkBounded(Node l, Node a, Node u);
 327
 328 Rational leastIntGreaterThan(const Rational&);
 329
 330 Rational greatestIntLessThan(const Rational&);
 331
 332 /** Negates a node in arithmetic proof normal form. */
 333 Node negateProofLiteral(TNode n);
 334
 335 /**
 336  * Return the result of multiplying constant integer or real nodes c1 and c2.
 337  * The returned type is real if either have type real.
 338  */
 339 Node multConstants(const Node& c1, const Node& c2);
 340
 341 }  // namespace arith
 342 }  // namespace theory
 343 }  // namespace cvc5
 344
 345 #endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */