1 /********************* */
2 /*! \file int_to_bv.cpp
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
12 ** \brief The IntToBV preprocessing pass
14 ** Converts integer operations into bitvector operations. The width of the
15 ** bitvectors is controlled through the `--solve-int-as-bv` command line
19 #include "preprocessing/passes/int_to_bv.h"
22 #include <unordered_map>
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"
33 namespace preprocessing
{
37 using namespace CVC4::theory
;
39 using NodeMap
= std::unordered_map
<Node
, Node
, NodeHashFunction
>;
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
)) {
55 Node
intToBVMakeBinary(TNode n
, NodeMap
& cache
)
57 for (TNode current
: NodeDfsIterable(n
, VisitOrder::POSTORDER
,
58 [&cache
](TNode nn
) { return cache
.count(nn
) > 0; }))
61 NodeManager
* nm
= NodeManager::currentNM();
62 if (current
.getNumChildren() == 0)
66 else if (current
.getNumChildren() > 2
67 && (current
.getKind() == kind::PLUS
68 || current
.getKind() == kind::MULT
))
70 Assert(cache
.find(current
[0]) != cache
.end());
71 result
= cache
[current
[0]];
72 for (unsigned i
= 1; i
< current
.getNumChildren(); ++i
)
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
);
82 NodeBuilder
<> builder(current
.getKind());
83 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
84 builder
<< current
.getOperator();
87 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
)
89 Assert(cache
.find(current
[i
]) != cache
.end());
90 builder
<< cache
[current
[i
]];
94 cache
[current
] = result
;
99 Node
intToBV(TNode n
, NodeMap
& cache
)
101 int size
= options::solveIntAsBV();
102 AlwaysAssert(size
> 0);
103 AlwaysAssert(!options::incrementalSolving());
106 Node n_binary
= intToBVMakeBinary(n
, binaryCache
);
108 for (TNode current
: NodeDfsIterable(n_binary
, VisitOrder::POSTORDER
,
109 [&cache
](TNode nn
) { return cache
.count(nn
) > 0; }))
111 NodeManager
* nm
= NodeManager::currentNM();
112 if (current
.getNumChildren() > 0)
115 vector
<Node
> children
;
117 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
)
119 Assert(cache
.find(current
[i
]) != cache
.end());
120 TNode childRes
= cache
[current
[i
]];
121 TypeNode type
= childRes
.getType();
122 if (type
.isBitVector())
124 unsigned bvsize
= type
.getBitVectorSize();
130 children
.push_back(childRes
);
133 kind::Kind_t newKind
= current
.getKind();
139 Assert(children
.size() == 2);
140 newKind
= kind::BITVECTOR_PLUS
;
144 Assert(children
.size() == 2);
145 newKind
= kind::BITVECTOR_MULT
;
149 Assert(children
.size() == 2);
150 newKind
= kind::BITVECTOR_SUB
;
154 Assert(children
.size() == 1);
155 newKind
= kind::BITVECTOR_NEG
;
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;
163 case kind::ITE
: break;
165 if (childrenTypesChanged(current
, cache
)) {
166 throw TypeCheckingException(
168 string("Cannot translate to BV: ") + current
.toString());
172 for (unsigned i
= 0; i
< children
.size(); ++i
)
174 TypeNode type
= children
[i
].getType();
175 if (!type
.isBitVector())
179 unsigned bvsize
= type
.getBitVectorSize();
183 Node signExtendOp
= nm
->mkConst
<BitVectorSignExtend
>(
184 BitVectorSignExtend(max
- bvsize
));
185 children
[i
] = nm
->mkNode(signExtendOp
, children
[i
]);
189 NodeBuilder
<> builder(newKind
);
190 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
191 builder
<< current
.getOperator();
193 for (unsigned i
= 0; i
< children
.size(); ++i
)
195 builder
<< children
[i
];
197 // Mark the substitution and continue
198 Node result
= builder
;
200 result
= Rewriter::rewrite(result
);
201 cache
[current
] = result
;
205 // It's a leaf: could be a variable or a numeral
206 Node result
= current
;
209 if (current
.getType() == nm
->integerType())
211 result
= nm
->mkSkolem("__intToBV_var",
212 nm
->mkBitVectorType(size
),
213 "Variable introduced in intToBV pass");
216 else if (current
.isConst())
218 switch (current
.getKind())
220 case kind::CONST_RATIONAL
:
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())
228 throw TypeCheckingException(
230 string("Not enough bits for constant in intToBV: ")
231 + current
.toString());
233 result
= nm
->mkConst(bv
);
242 throw TypeCheckingException(
244 string("Cannot translate to BV: ") + current
.toString());
246 cache
[current
] = result
;
249 return cache
[n_binary
];
253 IntToBV::IntToBV(PreprocessingPassContext
* preprocContext
)
254 : PreprocessingPass(preprocContext
, "int-to-bv"){};
256 PreprocessingPassResult
IntToBV::applyInternal(
257 AssertionPipeline
* assertionsToPreprocess
)
260 for (unsigned i
= 0; i
< assertionsToPreprocess
->size(); ++i
)
262 assertionsToPreprocess
->replace(
263 i
, intToBV((*assertionsToPreprocess
)[i
], cache
));
265 return PreprocessingPassResult::NO_CONFLICT
;
269 } // namespace passes
270 } // namespace preprocessing