src/theory/bv/theory_bv_utils.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Dejan Jovanovic, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include <set>
  23 #include <vector>
  24 #include <sstream>
  25 #include "expr/node_manager.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace bv {
  30
  31 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
  32 typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
  33
  34 namespace utils {
  35
  36 inline uint32_t pow2(uint32_t power) {
  37   Assert (power < 32);
  38   uint32_t one = 1;
  39   return one << power;
  40 }
  41
  42 inline unsigned getExtractHigh(TNode node) {
  43   return node.getOperator().getConst<BitVectorExtract>().high;
  44 }
  45
  46 inline unsigned getExtractLow(TNode node) {
  47   return node.getOperator().getConst<BitVectorExtract>().low;
  48 }
  49
  50 inline unsigned getSize(TNode node) {
  51   return node.getType().getBitVectorSize();
  52 }
  53
  54 inline const bool getBit(TNode node, unsigned i) {
  55   Assert (i < utils::getSize(node) &&
  56           node.getKind() == kind::CONST_BITVECTOR);
  57   Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
  58   return (bit == 1u);
  59 }
  60
  61 inline Node mkTrue() {
  62   return NodeManager::currentNM()->mkConst<bool>(true);
  63 }
  64
  65 inline Node mkFalse() {
  66   return NodeManager::currentNM()->mkConst<bool>(false);
  67 }
  68
  69 inline Node mkVar(unsigned size) {
  70   NodeManager* nm =  NodeManager::currentNM();
  71
  72   return nm->mkSkolem("BVSKOLEM$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors");
  73 }
  74
  75
  76 inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
  77   Assert (kind == kind::BITVECTOR_AND ||
  78           kind == kind::BITVECTOR_OR ||
  79           kind == kind::BITVECTOR_XOR);
  80   Assert(children.size() > 0);
  81   if (children.size() == 1) {
  82     return children[0];
  83   }
  84   std::sort(children.begin(), children.end());
  85   return NodeManager::currentNM()->mkNode(kind, children);
  86 }
  87
  88
  89 inline Node mkNode(Kind kind, std::vector<Node>& children) {
  90   Assert (children.size() > 0);
  91   if (children.size() == 1) {
  92     return children[0];
  93   }
  94   return NodeManager::currentNM()->mkNode(kind, children);
  95 }
  96
  97 inline Node mkNode(Kind kind, TNode child) {
  98   return NodeManager::currentNM()->mkNode(kind, child);
  99 }
 100
 101 inline Node mkNode(Kind kind, TNode child1, TNode child2) {
 102   return NodeManager::currentNM()->mkNode(kind, child1, child2);
 103 }
 104
 105
 106 inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) {
 107   Assert (kind == kind::BITVECTOR_AND ||
 108           kind == kind::BITVECTOR_OR ||
 109           kind == kind::BITVECTOR_XOR);
 110
 111   if (child1 < child2) {
 112     return NodeManager::currentNM()->mkNode(kind, child1, child2);
 113   } else {
 114     return NodeManager::currentNM()->mkNode(kind, child2, child1);
 115   }
 116 }
 117
 118 inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
 119   return NodeManager::currentNM()->mkNode(kind, child1, child2, child3);
 120 }
 121
 122
 123 inline Node mkNot(Node child) {
 124   return NodeManager::currentNM()->mkNode(kind::NOT, child);
 125 }
 126
 127 inline Node mkAnd(TNode node1, TNode node2) {
 128   return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
 129 }
 130
 131 inline Node mkOr(TNode node1, TNode node2) {
 132   return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
 133 }
 134
 135 inline Node mkXor(TNode node1, TNode node2) {
 136   return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
 137 }
 138
 139
 140 inline Node mkSignExtend(TNode node, unsigned ammount) {
 141   NodeManager* nm = NodeManager::currentNM();
 142   Node signExtendOp = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount));
 143   return nm->mkNode(signExtendOp, node);
 144 }
 145
 146 inline Node mkExtract(TNode node, unsigned high, unsigned low) {
 147   Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
 148   std::vector<Node> children;
 149   children.push_back(node);
 150   return NodeManager::currentNM()->mkNode(extractOp, children);
 151 }
 152
 153 inline Node mkBitOf(TNode node, unsigned index) {
 154   Node bitOfOp = NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
 155   return NodeManager::currentNM()->mkNode(bitOfOp, node);
 156
 157 }
 158
 159
 160 inline Node mkConcat(TNode node, unsigned repeat) {
 161   Assert (repeat);
 162   if(repeat == 1) {
 163     return node;
 164   }
 165   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
 166   for (unsigned i = 0; i < repeat; ++i) {
 167     result << node;
 168   }
 169   Node resultNode = result;
 170   return resultNode;
 171 }
 172
 173 inline Node mkConcat(std::vector<Node>& children) {
 174   if (children.size() > 1)
 175     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
 176   else
 177     return children[0];
 178 }
 179
 180 inline Node mkConcat(TNode t1, TNode t2) {
 181     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
 182 }
 183
 184
 185 inline BitVector mkBitVectorOnes(unsigned size) {
 186   Assert(size > 0);
 187   return BitVector(1, Integer(1)).signExtend(size - 1);
 188 }
 189
 190 inline Node mkOnes(unsigned size) {
 191   BitVector val = mkBitVectorOnes(size);
 192   return NodeManager::currentNM()->mkConst<BitVector>(val);
 193 }
 194
 195 inline Node mkConst(unsigned size, unsigned int value) {
 196   BitVector val(size, value);
 197   return NodeManager::currentNM()->mkConst<BitVector>(val);
 198 }
 199
 200 inline Node mkConst(const BitVector& value) {
 201   return NodeManager::currentNM()->mkConst<BitVector>(value);
 202 }
 203
 204 inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) {
 205   if (node.getKind() != kind::AND) {
 206     conjuncts.insert(node);
 207   } else {
 208     for (unsigned i = 0; i < node.getNumChildren(); ++ i) {
 209       getConjuncts(node[i], conjuncts);
 210     }
 211   }
 212 }
 213
 214 inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) {
 215   for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) {
 216     getConjuncts(nodes[i], conjuncts);
 217   }
 218 }
 219
 220 inline Node mkConjunction(const std::set<TNode> nodes) {
 221   std::set<TNode> expandedNodes;
 222
 223   std::set<TNode>::const_iterator it = nodes.begin();
 224   std::set<TNode>::const_iterator it_end = nodes.end();
 225   while (it != it_end) {
 226     TNode current = *it;
 227     if (current != mkTrue()) {
 228       Assert(current.getKind() == kind::EQUAL || (current.getKind() == kind::NOT && current[0].getKind() == kind::EQUAL));
 229       expandedNodes.insert(current);
 230     }
 231     ++ it;
 232   }
 233
 234   Assert(expandedNodes.size() > 0);
 235   if (expandedNodes.size() == 1) {
 236     return *expandedNodes.begin();
 237   }
 238
 239   NodeBuilder<> conjunction(kind::AND);
 240
 241   it = expandedNodes.begin();
 242   it_end = expandedNodes.end();
 243   while (it != it_end) {
 244     conjunction << *it;
 245     ++ it;
 246   }
 247
 248   return conjunction;
 249 }
 250
 251 inline unsigned isPow2Const(TNode node) {
 252   if (node.getKind() != kind::CONST_BITVECTOR) {
 253     return false;
 254   }
 255
 256   BitVector bv = node.getConst<BitVector>();
 257   return bv.isPow2();
 258 }
 259
 260 inline Node mkOr(const std::vector<Node>& nodes) {
 261   std::set<TNode> all;
 262   all.insert(nodes.begin(), nodes.end());
 263
 264   if (all.size() == 0) {
 265     return mkTrue();
 266   }
 267
 268   if (all.size() == 1) {
 269     // All the same, or just one
 270     return nodes[0];
 271   }
 272
 273
 274   NodeBuilder<> disjunction(kind::OR);
 275   std::set<TNode>::const_iterator it = all.begin();
 276   std::set<TNode>::const_iterator it_end = all.end();
 277   while (it != it_end) {
 278     disjunction << *it;
 279     ++ it;
 280   }
 281
 282   return disjunction;
 283 }/* mkOr() */
 284
 285
 286 inline Node mkAnd(const std::vector<TNode>& conjunctions) {
 287   std::set<TNode> all;
 288   all.insert(conjunctions.begin(), conjunctions.end());
 289
 290   if (all.size() == 0) {
 291     return mkTrue();
 292   }
 293
 294   if (all.size() == 1) {
 295     // All the same, or just one
 296     return conjunctions[0];
 297   }
 298
 299
 300   NodeBuilder<> conjunction(kind::AND);
 301   std::set<TNode>::const_iterator it = all.begin();
 302   std::set<TNode>::const_iterator it_end = all.end();
 303   while (it != it_end) {
 304     conjunction << *it;
 305     ++ it;
 306   }
 307
 308   return conjunction;
 309 }/* mkAnd() */
 310
 311 inline Node mkAnd(const std::vector<Node>& conjunctions) {
 312   std::set<TNode> all;
 313   all.insert(conjunctions.begin(), conjunctions.end());
 314
 315   if (all.size() == 0) {
 316     return mkTrue();
 317   }
 318
 319   if (all.size() == 1) {
 320     // All the same, or just one
 321     return conjunctions[0];
 322   }
 323
 324
 325   NodeBuilder<> conjunction(kind::AND);
 326   std::set<TNode>::const_iterator it = all.begin();
 327   std::set<TNode>::const_iterator it_end = all.end();
 328   while (it != it_end) {
 329     conjunction << *it;
 330     ++ it;
 331   }
 332
 333   return conjunction;
 334 }/* mkAnd() */
 335
 336 inline bool isZero(TNode node) {
 337   if (!node.isConst()) return false;
 338   return node == utils::mkConst(utils::getSize(node), 0u);
 339 }
 340
 341 inline Node flattenAnd(std::vector<TNode>& queue) {
 342   TNodeSet nodes;
 343   while(!queue.empty()) {
 344     TNode current = queue.back();
 345     queue.pop_back();
 346     if (current.getKind() ==  kind::AND) {
 347       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
 348         if (nodes.count(current[i]) == 0) {
 349           queue.push_back(current[i]);
 350         }
 351       }
 352     } else {
 353       nodes.insert(current);
 354     }
 355   }
 356   std::vector<TNode> children;
 357   for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) {
 358     children.push_back(*it);
 359   }
 360   return mkAnd(children);
 361 }
 362
 363
 364 // need a better name, this is not technically a ground term
 365 inline bool isBVGroundTerm(TNode node) {
 366   if (node.getNumChildren() == 0) {
 367     return node.isConst();
 368   }
 369
 370   for (size_t i = 0; i < node.getNumChildren(); ++i) {
 371     if(! node[i].isConst()) {
 372       return false;
 373     }
 374   }
 375   return true;
 376 }
 377
 378 inline bool isBVPredicate(TNode node) {
 379   if (node.getKind() == kind::EQUAL ||
 380       node.getKind() == kind::BITVECTOR_ULT ||
 381       node.getKind() == kind::BITVECTOR_SLT ||
 382       node.getKind() == kind::BITVECTOR_UGT ||
 383       node.getKind() == kind::BITVECTOR_UGE ||
 384       node.getKind() == kind::BITVECTOR_SGT ||
 385       node.getKind() == kind::BITVECTOR_SGE ||
 386       node.getKind() == kind::BITVECTOR_ULE ||
 387       node.getKind() == kind::BITVECTOR_SLE ||
 388       node.getKind() == kind::BITVECTOR_REDOR ||
 389       node.getKind() == kind::BITVECTOR_REDAND ||
 390       ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL ||
 391                                         node[0].getKind() == kind::BITVECTOR_ULT ||
 392                                         node[0].getKind() == kind::BITVECTOR_SLT ||
 393                                         node[0].getKind() == kind::BITVECTOR_UGT ||
 394                                         node[0].getKind() == kind::BITVECTOR_UGE ||
 395                                         node[0].getKind() == kind::BITVECTOR_SGT ||
 396                                         node[0].getKind() == kind::BITVECTOR_SGE ||
 397                                         node[0].getKind() == kind::BITVECTOR_ULE ||
 398                                         node[0].getKind() == kind::BITVECTOR_SLE ||
 399                                         node[0].getKind() == kind::BITVECTOR_REDOR ||
 400                                         node[0].getKind() == kind::BITVECTOR_REDAND)))
 401     {
 402       return true;
 403     }
 404   else
 405     {
 406       return false;
 407     }
 408 }
 409
 410 inline Node mkConjunction(const std::vector<TNode>& nodes) {
 411   std::vector<TNode> expandedNodes;
 412
 413   std::vector<TNode>::const_iterator it = nodes.begin();
 414   std::vector<TNode>::const_iterator it_end = nodes.end();
 415   while (it != it_end) {
 416     TNode current = *it;
 417
 418     if (current != mkTrue()) {
 419       Assert(isBVPredicate(current));
 420       expandedNodes.push_back(current);
 421     }
 422     ++ it;
 423   }
 424
 425   if (expandedNodes.size() == 0) {
 426     return mkTrue();
 427   }
 428
 429   if (expandedNodes.size() == 1) {
 430     return *expandedNodes.begin();
 431   }
 432
 433   NodeBuilder<> conjunction(kind::AND);
 434
 435   it = expandedNodes.begin();
 436   it_end = expandedNodes.end();
 437   while (it != it_end) {
 438     conjunction << *it;
 439     ++ it;
 440   }
 441
 442   return conjunction;
 443 }
 444
 445
 446
 447 // Turn a set into a string
 448 inline std::string setToString(const std::set<TNode>& nodeSet) {
 449   std::stringstream out;
 450   out << "[";
 451   std::set<TNode>::const_iterator it = nodeSet.begin();
 452   std::set<TNode>::const_iterator it_end = nodeSet.end();
 453   bool first = true;
 454   while (it != it_end) {
 455     if (!first) {
 456       out << ",";
 457     }
 458     first = false;
 459     out << *it;
 460     ++ it;
 461   }
 462   out << "]";
 463   return out.str();
 464 }
 465
 466 // Turn a vector into a string
 467 inline std::string vectorToString(const std::vector<Node>& nodes) {
 468   std::stringstream out;
 469   out << "[";
 470   for (unsigned i = 0; i < nodes.size(); ++ i) {
 471     if (i > 0) {
 472       out << ",";
 473     }
 474     out << nodes[i];
 475   }
 476   out << "]";
 477   return out.str();
 478 }
 479
 480 // FIXME: dumb code
 481 inline void intersect(const std::vector<uint32_t>& v1,
 482                       const std::vector<uint32_t>& v2,
 483                       std::vector<uint32_t>& intersection) {
 484   for (unsigned i = 0; i < v1.size(); ++i) {
 485     bool found = false;
 486     for (unsigned j = 0; j < v2.size(); ++j) {
 487       if (v2[j] == v1[i]) {
 488         found = true;
 489         break;
 490       }
 491     }
 492     if (found) {
 493       intersection.push_back(v1[i]);
 494     }
 495   }
 496 }
 497
 498 template <class T>
 499 inline T gcd(T a, T b) {
 500   while (b != 0) {
 501     T t = b;
 502     b = a % t;
 503     a = t;
 504   }
 505   return a;
 506 }
 507
 508 typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
 509
 510 bool isCoreTerm(TNode term, TNodeBoolMap& cache);
 511 bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
 512 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 513
 514 uint64_t numNodes(TNode node, NodeSet& seen);
 515
 516 void collectVariables(TNode node, NodeSet& vars);
 517
 518 }
 519 }
 520 }
 521 }