src/theory/arith/arith_utilities.cpp

   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-2022 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::internal::kind;
  21
  22 namespace cvc5::internal {
  23 namespace theory {
  24 namespace arith {
  25
  26 Kind joinKinds(Kind k1, Kind k2)
  27 {
  28   if (k2 < k1)
  29   {
  30     return joinKinds(k2, k1);
  31   }
  32   else if (k1 == k2)
  33   {
  34     return k1;
  35   }
  36   Assert(isRelationOperator(k1));
  37   Assert(isRelationOperator(k2));
  38   if (k1 == EQUAL)
  39   {
  40     if (k2 == LEQ || k2 == GEQ)
  41     {
  42       return k1;
  43     }
  44   }
  45   else if (k1 == LT)
  46   {
  47     if (k2 == LEQ)
  48     {
  49       return k1;
  50     }
  51   }
  52   else if (k1 == LEQ)
  53   {
  54     if (k2 == GEQ)
  55     {
  56       return EQUAL;
  57     }
  58   }
  59   else if (k1 == GT)
  60   {
  61     if (k2 == GEQ)
  62     {
  63       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 bool isTranscendentalKind(Kind k)
 103 {
 104   // many operators are eliminated during rewriting
 105   Assert(k != TANGENT && k != COSINE && k != COSECANT
 106          && k != SECANT && k != COTANGENT);
 107   return k == EXPONENTIAL || k == SINE || k == PI;
 108 }
 109
 110 Node getApproximateConstant(Node c, bool isLower, unsigned prec)
 111 {
 112   if (!c.isConst())
 113   {
 114     Assert(false) << "getApproximateConstant: non-constant input " << c;
 115     return Node::null();
 116   }
 117   Rational cr = c.getConst<Rational>();
 118
 119   unsigned lower = 0;
 120   unsigned upper = std::pow(10, prec);
 121
 122   Rational den = Rational(upper);
 123   if (cr.getDenominator() < den.getNumerator())
 124   {
 125     // denominator is not more than precision, we return it
 126     return c;
 127   }
 128
 129   int csign = cr.sgn();
 130   Assert(csign != 0);
 131   if (csign == -1)
 132   {
 133     cr = -cr;
 134   }
 135   Rational one = Rational(1);
 136   Rational ten = Rational(10);
 137   Rational pow_ten = Rational(1);
 138   // inefficient for large numbers
 139   while (cr >= one)
 140   {
 141     cr = cr / ten;
 142     pow_ten = pow_ten * ten;
 143   }
 144   Rational allow_err = one / den;
 145
 146   // now do binary search
 147   Rational two = Rational(2);
 148   NodeManager* nm = NodeManager::currentNM();
 149   Node cret;
 150   do
 151   {
 152     unsigned curr = (lower + upper) / 2;
 153     Rational curr_r = Rational(curr) / den;
 154     Rational err = cr - curr_r;
 155     int esign = err.sgn();
 156     if (err.abs() <= allow_err)
 157     {
 158       if (esign == 1 && !isLower)
 159       {
 160         curr_r = Rational(curr + 1) / den;
 161       }
 162       else if (esign == -1 && isLower)
 163       {
 164         curr_r = Rational(curr - 1) / den;
 165       }
 166       curr_r = curr_r * pow_ten;
 167       cret = nm->mkConst(CONST_RATIONAL, csign == 1 ? curr_r : -curr_r);
 168     }
 169     else
 170     {
 171       Assert(esign != 0);
 172       // update lower/upper
 173       if (esign == -1)
 174       {
 175         upper = curr;
 176       }
 177       else if (esign == 1)
 178       {
 179         lower = curr;
 180       }
 181     }
 182   } while (cret.isNull());
 183   return cret;
 184 }
 185
 186 void printRationalApprox(const char* c, Node cr, unsigned prec)
 187 {
 188   if (!cr.isConst())
 189   {
 190     Assert(false) << "printRationalApprox: non-constant input " << cr;
 191     Trace(c) << cr;
 192     return;
 193   }
 194   Node ca = getApproximateConstant(cr, true, prec);
 195   if (ca != cr)
 196   {
 197     Trace(c) << "(+ ";
 198   }
 199   Trace(c) << ca;
 200   if (ca != cr)
 201   {
 202     Trace(c) << " [0,10^" << prec << "])";
 203   }
 204 }
 205
 206 Node arithSubstitute(Node n, const Subs& sub)
 207 {
 208   NodeManager* nm = NodeManager::currentNM();
 209   std::unordered_map<TNode, Node> visited;
 210   std::vector<TNode> visit;
 211   visit.push_back(n);
 212   do
 213   {
 214     TNode cur = visit.back();
 215     visit.pop_back();
 216     auto it = visited.find(cur);
 217
 218     if (it == visited.end())
 219     {
 220       visited[cur] = Node::null();
 221       Kind ck = cur.getKind();
 222       auto s = sub.find(cur);
 223       if (s)
 224       {
 225         visited[cur] = *s;
 226       }
 227       else if (cur.getNumChildren() == 0)
 228       {
 229         visited[cur] = cur;
 230       }
 231       else
 232       {
 233         TheoryId ctid = theory::kindToTheoryId(ck);
 234         if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
 235              && ctid != THEORY_BUILTIN)
 236             || 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           visited[cur] = cur;
 242         }
 243         else
 244         {
 245           visit.push_back(cur);
 246           for (const Node& cn : cur)
 247           {
 248             visit.push_back(cn);
 249           }
 250         }
 251       }
 252     }
 253     else if (it->second.isNull())
 254     {
 255       Node ret = cur;
 256       bool childChanged = false;
 257       std::vector<Node> children;
 258       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
 259       {
 260         children.push_back(cur.getOperator());
 261       }
 262       for (const Node& cn : cur)
 263       {
 264         it = visited.find(cn);
 265         Assert(it != visited.end());
 266         Assert(!it->second.isNull());
 267         childChanged = childChanged || cn != it->second;
 268         children.push_back(it->second);
 269       }
 270       if (childChanged)
 271       {
 272         ret = nm->mkNode(cur.getKind(), children);
 273       }
 274       visited[cur] = ret;
 275     }
 276   } while (!visit.empty());
 277   Assert(visited.find(n) != visited.end());
 278   Assert(!visited.find(n)->second.isNull());
 279   return visited[n];
 280 }
 281
 282 Node mkBounded(Node l, Node a, Node u)
 283 {
 284   NodeManager* nm = NodeManager::currentNM();
 285   return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
 286 }
 287
 288 Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
 289
 290 Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
 291
 292 Node negateProofLiteral(TNode n)
 293 {
 294   auto nm = NodeManager::currentNM();
 295   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     case Kind::LEQ:
 306     {
 307       return nm->mkNode(Kind::GT, n[0], n[1]);
 308     }
 309     case Kind::GEQ:
 310     {
 311       return nm->mkNode(Kind::LT, n[0], n[1]);
 312     }
 313     case Kind::EQUAL:
 314     case Kind::NOT:
 315     {
 316       return n.negate();
 317     }
 318     default: Unhandled() << n;
 319   }
 320 }
 321
 322 Node multConstants(const Node& c1, const Node& c2)
 323 {
 324   Assert(!c1.isNull() && c1.isConst());
 325   Assert(!c2.isNull() && c2.isConst());
 326   NodeManager* nm = NodeManager::currentNM();
 327   // real type if either has type real
 328   TypeNode tn = c1.getType();
 329   if (tn.isInteger())
 330   {
 331     tn = c2.getType();
 332   }
 333   Assert(tn.isRealOrInt());
 334   return nm->mkConstRealOrInt(
 335       tn, Rational(c1.getConst<Rational>() * c2.getConst<Rational>()));
 336 }
 337
 338 }  // namespace arith
 339 }  // namespace theory
 340 }  // namespace cvc5::internal