src/preprocessing/passes/int_to_bv.cpp

   1 /*********************                                                        */
   2 /*! \file int_to_bv.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Yoni Zohar, Alex Ozdemir
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 The IntToBV preprocessing pass
  13  **
  14  ** Converts integer operations into bitvector operations. The width of the
  15  ** bitvectors is controlled through the `--solve-int-as-bv` command line
  16  ** option.
  17  **/
  18
  19 #include "preprocessing/passes/int_to_bv.h"
  20
  21 #include <string>
  22 #include <unordered_map>
  23 #include <vector>
  24
  25 #include "expr/node.h"
  26 #include "expr/node_traversal.h"
  27 #include "options/smt_options.h"
  28 #include "preprocessing/assertion_pipeline.h"
  29 #include "theory/rewriter.h"
  30 #include "theory/theory.h"
  31
  32 namespace CVC4 {
  33 namespace preprocessing {
  34 namespace passes {
  35
  36 using namespace std;
  37 using namespace CVC4::theory;
  38
  39 using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
  40
  41 namespace {
  42
  43 bool childrenTypesChanged(Node n, NodeMap& cache) {
  44   for (Node child : n) {
  45     TypeNode originalType = child.getType();
  46     TypeNode newType = cache[child].getType();
  47     if (! newType.isSubtypeOf(originalType)) {
  48       return true;
  49     }
  50   }
  51   return false;
  52 }
  53
  54
  55 Node intToBVMakeBinary(TNode n, NodeMap& cache)
  56 {
  57   for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER,
  58            [&cache](TNode nn) { return cache.count(nn) > 0; }))
  59   {
  60     Node result;
  61     NodeManager* nm = NodeManager::currentNM();
  62     if (current.getNumChildren() == 0)
  63     {
  64       result = current;
  65     }
  66     else if (current.getNumChildren() > 2
  67              && (current.getKind() == kind::PLUS
  68                  || current.getKind() == kind::MULT))
  69     {
  70       Assert(cache.find(current[0]) != cache.end());
  71       result = cache[current[0]];
  72       for (unsigned i = 1; i < current.getNumChildren(); ++i)
  73       {
  74         Assert(cache.find(current[i]) != cache.end());
  75         Node child = current[i];
  76         Node childRes = cache[current[i]];
  77         result = nm->mkNode(current.getKind(), result, childRes);
  78       }
  79     }
  80     else
  81     {
  82       NodeBuilder<> builder(current.getKind());
  83       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
  84         builder << current.getOperator();
  85       }
  86
  87       for (unsigned i = 0; i < current.getNumChildren(); ++i)
  88       {
  89         Assert(cache.find(current[i]) != cache.end());
  90         builder << cache[current[i]];
  91       }
  92       result = builder;
  93     }
  94     cache[current] = result;
  95   }
  96   return cache[n];
  97 }
  98
  99 Node intToBV(TNode n, NodeMap& cache)
 100 {
 101   int size = options::solveIntAsBV();
 102   AlwaysAssert(size > 0);
 103   AlwaysAssert(!options::incrementalSolving());
 104
 105   NodeMap binaryCache;
 106   Node n_binary = intToBVMakeBinary(n, binaryCache);
 107
 108   for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
 109            [&cache](TNode nn) { return cache.count(nn) > 0; }))
 110   {
 111     NodeManager* nm = NodeManager::currentNM();
 112     if (current.getNumChildren() > 0)
 113     {
 114       // Not a leaf
 115       vector<Node> children;
 116       unsigned max = 0;
 117       for (unsigned i = 0; i < current.getNumChildren(); ++i)
 118       {
 119         Assert(cache.find(current[i]) != cache.end());
 120         TNode childRes = cache[current[i]];
 121         TypeNode type = childRes.getType();
 122         if (type.isBitVector())
 123         {
 124           unsigned bvsize = type.getBitVectorSize();
 125           if (bvsize > max)
 126           {
 127             max = bvsize;
 128           }
 129         }
 130         children.push_back(childRes);
 131       }
 132
 133       kind::Kind_t newKind = current.getKind();
 134       if (max > 0)
 135       {
 136         switch (newKind)
 137         {
 138           case kind::PLUS:
 139             Assert(children.size() == 2);
 140             newKind = kind::BITVECTOR_PLUS;
 141             max = max + 1;
 142             break;
 143           case kind::MULT:
 144             Assert(children.size() == 2);
 145             newKind = kind::BITVECTOR_MULT;
 146             max = max * 2;
 147             break;
 148           case kind::MINUS:
 149             Assert(children.size() == 2);
 150             newKind = kind::BITVECTOR_SUB;
 151             max = max + 1;
 152             break;
 153           case kind::UMINUS:
 154             Assert(children.size() == 1);
 155             newKind = kind::BITVECTOR_NEG;
 156             max = max + 1;
 157             break;
 158           case kind::LT: newKind = kind::BITVECTOR_SLT; break;
 159           case kind::LEQ: newKind = kind::BITVECTOR_SLE; break;
 160           case kind::GT: newKind = kind::BITVECTOR_SGT; break;
 161           case kind::GEQ: newKind = kind::BITVECTOR_SGE; break;
 162           case kind::EQUAL:
 163           case kind::ITE: break;
 164           default:
 165             if (childrenTypesChanged(current, cache)) {
 166               throw TypeCheckingException(
 167                 current.toExpr(),
 168                 string("Cannot translate to BV: ") + current.toString());
 169             }
 170             break;
 171         }
 172         for (unsigned i = 0; i < children.size(); ++i)
 173         {
 174           TypeNode type = children[i].getType();
 175           if (!type.isBitVector())
 176           {
 177             continue;
 178           }
 179           unsigned bvsize = type.getBitVectorSize();
 180           if (bvsize < max)
 181           {
 182             // sign extend
 183             Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
 184                 BitVectorSignExtend(max - bvsize));
 185             children[i] = nm->mkNode(signExtendOp, children[i]);
 186           }
 187         }
 188       }
 189       NodeBuilder<> builder(newKind);
 190       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 191         builder << current.getOperator();
 192       }
 193       for (unsigned i = 0; i < children.size(); ++i)
 194       {
 195         builder << children[i];
 196       }
 197       // Mark the substitution and continue
 198       Node result = builder;
 199
 200       result = Rewriter::rewrite(result);
 201       cache[current] = result;
 202     }
 203     else
 204     {
 205       // It's a leaf: could be a variable or a numeral
 206       Node result = current;
 207       if (current.isVar())
 208       {
 209         if (current.getType() == nm->integerType())
 210         {
 211           result = nm->mkSkolem("__intToBV_var",
 212                                 nm->mkBitVectorType(size),
 213                                 "Variable introduced in intToBV pass");
 214         }
 215       }
 216       else if (current.isConst())
 217       {
 218         switch (current.getKind())
 219         {
 220           case kind::CONST_RATIONAL:
 221           {
 222             Rational constant = current.getConst<Rational>();
 223             if (constant.isIntegral()) {
 224               AlwaysAssert(constant >= 0);
 225               BitVector bv(size, constant.getNumerator());
 226               if (bv.toSignedInteger() != constant.getNumerator())
 227               {
 228                 throw TypeCheckingException(
 229                     current.toExpr(),
 230                     string("Not enough bits for constant in intToBV: ")
 231                         + current.toString());
 232               }
 233               result = nm->mkConst(bv);
 234             }
 235             break;
 236           }
 237           default: break;
 238         }
 239       }
 240       else
 241       {
 242         throw TypeCheckingException(
 243             current.toExpr(),
 244             string("Cannot translate to BV: ") + current.toString());
 245       }
 246       cache[current] = result;
 247     }
 248   }
 249   return cache[n_binary];
 250 }
 251 }  // namespace
 252
 253 IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
 254     : PreprocessingPass(preprocContext, "int-to-bv"){};
 255
 256 PreprocessingPassResult IntToBV::applyInternal(
 257     AssertionPipeline* assertionsToPreprocess)
 258 {
 259   NodeMap cache;
 260   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
 261   {
 262     assertionsToPreprocess->replace(
 263         i, intToBV((*assertionsToPreprocess)[i], cache));
 264   }
 265   return PreprocessingPassResult::NO_CONFLICT;
 266 }
 267
 268
 269 }  // namespace passes
 270 }  // namespace preprocessing
 271 }  // namespace CVC4