src/theory/bv/theory_bv_utils.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bv_utils.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Liana Hadarean, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Util functions for theory BV.
  13  **
  14  ** Util functions for theory BV.
  15  **/
  16
  17 #include "theory/bv/theory_bv_utils.h"
  18
  19 #include <vector>
  20
  21 #include "options/theory_options.h"
  22 #include "theory/theory.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace bv {
  27 namespace utils {
  28
  29 /* ------------------------------------------------------------------------- */
  30
  31 unsigned getSize(TNode node)
  32 {
  33   return node.getType().getBitVectorSize();
  34 }
  35
  36 const bool getBit(TNode node, unsigned i)
  37 {
  38   Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
  39   return node.getConst<BitVector>().extract(i, i).getValue() == 1u;
  40 }
  41
  42 /* ------------------------------------------------------------------------- */
  43
  44 unsigned getExtractHigh(TNode node)
  45 {
  46   return node.getOperator().getConst<BitVectorExtract>().d_high;
  47 }
  48
  49 unsigned getExtractLow(TNode node)
  50 {
  51   return node.getOperator().getConst<BitVectorExtract>().d_low;
  52 }
  53
  54 unsigned getSignExtendAmount(TNode node)
  55 {
  56   return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
  57 }
  58
  59 /* ------------------------------------------------------------------------- */
  60
  61 bool isOnes(TNode node)
  62 {
  63   if (!node.isConst()) return false;
  64   return node == mkOnes(getSize(node));
  65 }
  66
  67 bool isZero(TNode node)
  68 {
  69   if (!node.isConst()) return false;
  70   return node == mkZero(getSize(node));
  71 }
  72
  73 bool isOne(TNode node)
  74 {
  75   if (!node.isConst()) return false;
  76   return node == mkOne(getSize(node));
  77 }
  78
  79 unsigned isPow2Const(TNode node, bool& isNeg)
  80 {
  81   if (node.getKind() != kind::CONST_BITVECTOR)
  82   {
  83     return false;
  84   }
  85
  86   BitVector bv = node.getConst<BitVector>();
  87   unsigned p = bv.isPow2();
  88   if (p != 0)
  89   {
  90     isNeg = false;
  91     return p;
  92   }
  93   BitVector nbv = -bv;
  94   p = nbv.isPow2();
  95   if (p != 0)
  96   {
  97     isNeg = true;
  98     return p;
  99   }
 100   return false;
 101 }
 102
 103 bool isBvConstTerm(TNode node)
 104 {
 105   if (node.getNumChildren() == 0)
 106   {
 107     return node.isConst();
 108   }
 109
 110   for (const TNode& n : node)
 111   {
 112     if (!n.isConst()) { return false; }
 113   }
 114   return true;
 115 }
 116
 117 bool isBVPredicate(TNode node)
 118 {
 119   Kind k = node.getKind();
 120   if (k == kind::NOT)
 121   {
 122     node = node[0];
 123     k = node.getKind();
 124   }
 125   return k == kind::EQUAL
 126          || k == kind::BITVECTOR_ULT
 127          || k == kind::BITVECTOR_SLT
 128          || k == kind::BITVECTOR_UGT
 129          || k == kind::BITVECTOR_UGE
 130          || k == kind::BITVECTOR_SGT
 131          || k == kind::BITVECTOR_SGE
 132          || k == kind::BITVECTOR_ULE
 133          || k == kind::BITVECTOR_SLE
 134          || k == kind::BITVECTOR_REDOR
 135          || k == kind::BITVECTOR_REDAND;
 136 }
 137
 138 static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
 139 {
 140   TNode t = term.getKind() == kind::NOT ? term[0] : term;
 141
 142   std::vector<TNode> stack;
 143   std::unordered_map<TNode, bool, TNodeHashFunction> visited;
 144   stack.push_back(t);
 145
 146   while (!stack.empty())
 147   {
 148     TNode n = stack.back();
 149     stack.pop_back();
 150
 151     if (cache.find(n) != cache.end()) continue;
 152
 153     if (n.getNumChildren() == 0)
 154     {
 155       cache[n] = true;
 156       visited[n] = true;
 157       continue;
 158     }
 159
 160     if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
 161         == theory::THEORY_BV)
 162     {
 163       Kind k = n.getKind();
 164       Assert(k != kind::CONST_BITVECTOR);
 165       if (k != kind::EQUAL
 166           && (iseq || k != kind::BITVECTOR_CONCAT)
 167           && (iseq || k != kind::BITVECTOR_EXTRACT)
 168           && n.getMetaKind() != kind::metakind::VARIABLE)
 169       {
 170         cache[n] = false;
 171         continue;
 172       }
 173     }
 174
 175     if (!visited[n])
 176     {
 177       visited[n] = true;
 178       stack.push_back(n);
 179       stack.insert(stack.end(), n.begin(), n.end());
 180     }
 181     else
 182     {
 183       bool iseqt = true;
 184       for (const Node& c : n)
 185       {
 186         Assert(cache.find(c) != cache.end());
 187         if (!cache[c])
 188         {
 189           iseqt = false;
 190           break;
 191         }
 192       }
 193       cache[n] = iseqt;
 194     }
 195   }
 196   Assert(cache.find(t) != cache.end());
 197   return cache[t];
 198 }
 199
 200 bool isCoreTerm(TNode term, TNodeBoolMap& cache)
 201 {
 202   return isCoreEqTerm(false, term, cache);
 203 }
 204
 205 bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
 206 {
 207   return isCoreEqTerm(true, term, cache);
 208 }
 209
 210 bool isBitblastAtom(Node lit)
 211 {
 212   TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit;
 213   return atom.getKind() != kind::EQUAL || atom[0].getType().isBitVector();
 214 }
 215
 216 /* ------------------------------------------------------------------------- */
 217
 218 Node mkTrue()
 219 {
 220   return NodeManager::currentNM()->mkConst<bool>(true);
 221 }
 222
 223 Node mkFalse()
 224 {
 225   return NodeManager::currentNM()->mkConst<bool>(false);
 226 }
 227
 228 Node mkZero(unsigned size)
 229 {
 230   Assert(size > 0);
 231   return mkConst(size, 0u);
 232 }
 233
 234 Node mkOne(unsigned size)
 235 {
 236   Assert(size > 0);
 237   return mkConst(size, 1u);
 238 }
 239
 240 Node mkOnes(unsigned size)
 241 {
 242   Assert(size > 0);
 243   return mkConst(BitVector::mkOnes(size));
 244 }
 245
 246 Node mkMinSigned(unsigned size)
 247 {
 248   Assert(size > 0);
 249   return mkConst(BitVector::mkMinSigned(size));
 250 }
 251
 252 Node mkMaxSigned(unsigned size)
 253 {
 254   Assert(size > 0);
 255   return mkConst(BitVector::mkMaxSigned(size));
 256 }
 257
 258 /* ------------------------------------------------------------------------- */
 259
 260 Node mkConst(unsigned size, unsigned int value)
 261 {
 262   BitVector val(size, value);
 263   return NodeManager::currentNM()->mkConst<BitVector>(val);
 264 }
 265
 266 Node mkConst(unsigned size, Integer& value)
 267 {
 268   return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
 269 }
 270
 271 Node mkConst(const BitVector& value)
 272 {
 273   return NodeManager::currentNM()->mkConst<BitVector>(value);
 274 }
 275
 276 /* ------------------------------------------------------------------------- */
 277
 278 Node mkVar(unsigned size)
 279 {
 280   NodeManager* nm = NodeManager::currentNM();
 281
 282   return nm->mkSkolem("BVSKOLEM$$",
 283                       nm->mkBitVectorType(size),
 284                       "is a variable created by the theory of bitvectors");
 285 }
 286
 287 /* ------------------------------------------------------------------------- */
 288
 289 Node mkSortedNode(Kind kind, TNode child1, TNode child2)
 290 {
 291   Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
 292          || kind == kind::BITVECTOR_XOR);
 293
 294   if (child1 < child2)
 295   {
 296     return NodeManager::currentNM()->mkNode(kind, child1, child2);
 297   }
 298   else
 299   {
 300     return NodeManager::currentNM()->mkNode(kind, child2, child1);
 301   }
 302 }
 303
 304 Node mkSortedNode(Kind kind, std::vector<Node>& children)
 305 {
 306   Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
 307          || kind == kind::BITVECTOR_XOR);
 308   Assert(children.size() > 0);
 309   if (children.size() == 1)
 310   {
 311     return children[0];
 312   }
 313   std::sort(children.begin(), children.end());
 314   return NodeManager::currentNM()->mkNode(kind, children);
 315 }
 316
 317 /* ------------------------------------------------------------------------- */
 318
 319 Node mkNot(Node child)
 320 {
 321   return NodeManager::currentNM()->mkNode(kind::NOT, child);
 322 }
 323
 324 Node mkAnd(TNode node1, TNode node2)
 325 {
 326   return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
 327 }
 328
 329 Node mkOr(TNode node1, TNode node2)
 330 {
 331   return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
 332 }
 333
 334 Node mkXor(TNode node1, TNode node2)
 335 {
 336   return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
 337 }
 338
 339 /* ------------------------------------------------------------------------- */
 340
 341 Node mkSignExtend(TNode node, unsigned amount)
 342 {
 343   NodeManager* nm = NodeManager::currentNM();
 344   Node signExtendOp =
 345       nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount));
 346   return nm->mkNode(signExtendOp, node);
 347 }
 348
 349 /* ------------------------------------------------------------------------- */
 350
 351 Node mkExtract(TNode node, unsigned high, unsigned low)
 352 {
 353   NodeManager *nm = NodeManager::currentNM();
 354   Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
 355   return nm->mkNode(extractOp, node);
 356 }
 357
 358 Node mkBitOf(TNode node, unsigned index)
 359 {
 360   NodeManager *nm = NodeManager::currentNM();
 361   Node bitOfOp = nm->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
 362   return nm->mkNode(bitOfOp, node);
 363 }
 364
 365 /* ------------------------------------------------------------------------- */
 366
 367 Node mkConcat(TNode t1, TNode t2)
 368 {
 369   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
 370 }
 371
 372 Node mkConcat(std::vector<Node>& children)
 373 {
 374   if (children.size() > 1)
 375     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
 376   else
 377     return children[0];
 378 }
 379
 380 Node mkConcat(TNode node, unsigned repeat)
 381 {
 382   Assert(repeat);
 383   if (repeat == 1)
 384   {
 385     return node;
 386   }
 387   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
 388   for (unsigned i = 0; i < repeat; ++i)
 389   {
 390     result << node;
 391   }
 392   Node resultNode = result;
 393   return resultNode;
 394 }
 395
 396 /* ------------------------------------------------------------------------- */
 397
 398 Node mkInc(TNode t)
 399 {
 400   return NodeManager::currentNM()->mkNode(
 401       kind::BITVECTOR_PLUS, t, mkOne(getSize(t)));
 402 }
 403
 404 Node mkDec(TNode t)
 405 {
 406   return NodeManager::currentNM()->mkNode(
 407       kind::BITVECTOR_SUB, t, mkOne(getSize(t)));
 408 }
 409
 410 /* ------------------------------------------------------------------------- */
 411
 412 Node mkUmulo(TNode t1, TNode t2)
 413 {
 414   unsigned w = getSize(t1);
 415   if (w == 1) return mkFalse();
 416
 417   NodeManager* nm = NodeManager::currentNM();
 418   Node uppc;
 419   std::vector<Node> tmp;
 420
 421   uppc = mkExtract(t1, w - 1, w - 1);
 422   for (size_t i = 1; i < w; ++i)
 423   {
 424     tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
 425     uppc = nm->mkNode(
 426         kind::BITVECTOR_OR, mkExtract(t1, w - 1 - i, w - 1 - i), uppc);
 427   }
 428   Node zext_t1 = mkConcat(mkZero(1), t1);
 429   Node zext_t2 = mkConcat(mkZero(1), t2);
 430   Node mul = nm->mkNode(kind::BITVECTOR_MULT, zext_t1, zext_t2);
 431   tmp.push_back(mkExtract(mul, w, w));
 432   return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1));
 433 }
 434
 435 /* ------------------------------------------------------------------------- */
 436
 437 Node flattenAnd(std::vector<TNode>& queue)
 438 {
 439   TNodeSet nodes;
 440   while (!queue.empty())
 441   {
 442     TNode current = queue.back();
 443     queue.pop_back();
 444     if (current.getKind() == kind::AND)
 445     {
 446       for (const TNode& n : current)
 447       {
 448         if (nodes.count(n) == 0) { queue.push_back(n); }
 449       }
 450     }
 451     else
 452     {
 453       nodes.insert(current);
 454     }
 455   }
 456   std::vector<TNode> children(nodes.begin(), nodes.end());
 457   return mkAnd(children);
 458 }
 459
 460 /* ------------------------------------------------------------------------- */
 461
 462 Node eliminateBv2Nat(TNode node)
 463 {
 464   const unsigned size = utils::getSize(node[0]);
 465   NodeManager* const nm = NodeManager::currentNM();
 466   const Node z = nm->mkConst(Rational(0));
 467   const Node bvone = utils::mkOne(1);
 468
 469   Integer i = 1;
 470   std::vector<Node> children;
 471   for (unsigned bit = 0; bit < size; ++bit, i *= 2)
 472   {
 473     Node cond =
 474         nm->mkNode(kind::EQUAL,
 475                    nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
 476                    bvone);
 477     children.push_back(
 478         nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
 479   }
 480   // avoid plus with one child
 481   return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
 482 }
 483
 484 Node eliminateInt2Bv(TNode node)
 485 {
 486   const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
 487   NodeManager* const nm = NodeManager::currentNM();
 488   const Node bvzero = utils::mkZero(1);
 489   const Node bvone = utils::mkOne(1);
 490
 491   std::vector<Node> v;
 492   Integer i = 2;
 493   while (v.size() < size)
 494   {
 495     Node cond = nm->mkNode(
 496         kind::GEQ,
 497         nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
 498         nm->mkConst(Rational(i, 2)));
 499     v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
 500     i *= 2;
 501   }
 502   if (v.size() == 1)
 503   {
 504     return v[0];
 505   }
 506   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
 507   result.append(v.rbegin(), v.rend());
 508   return Node(result);
 509 }
 510
 511 }/* CVC4::theory::bv::utils namespace */
 512 }/* CVC4::theory::bv namespace */
 513 }/* CVC4::theory namespace */
 514 }/* CVC4 namespace */