diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-23 06:00:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-23 08:00:59 -0500 |
commit | 9967954ba1b7b405b6d92d83ebc0adc43f6623b9 (patch) | |
tree | d2c08b4b644a23e1092f31a4d242949f3c5a293f /src/preprocessing/passes | |
parent | cfe0fc1346c41048fa76f7e0fc582afbe95364a2 (diff) |
bv2int: new options for bvand translation (#5096)
Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):
bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 42 |
1 files changed, 36 insertions, 6 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index aa1b5ac5b..9ee4e2b7d 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -169,7 +169,8 @@ Node BVToInt::eliminationPass(Node n) { current = toVisit.back(); // assert that the node is binarized - kind::Kind_t k = current.getKind(); + // The following variable is only used in assertions + CVC4_UNUSED kind::Kind_t k = current.getKind(); uint64_t numChildren = current.getNumChildren(); Assert((numChildren == 2) || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT @@ -350,7 +351,8 @@ Node BVToInt::translateWithChildren(Node original, // ultbv and sltbv were supposed to be eliminated before this point. Assert(oldKind != kind::BITVECTOR_ULTBV); Assert(oldKind != kind::BITVECTOR_SLTBV); - uint64_t originalNumChildren = original.getNumChildren(); + // The following variable will only be used in assertions. + CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren(); Node returnNode; switch (oldKind) { @@ -414,15 +416,43 @@ Node BVToInt::translateWithChildren(Node original, } case kind::BITVECTOR_AND: { - // Construct an ite, based on granularity. + // We support three configurations: + // 1. translating to IAND + // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV + // operators) + // 3. translating into a sum uint64_t bvsize = original[0].getType().getBitVectorSize(); - Assert(translated_children.size() == 2); - Node newNode = createBitwiseNode(translated_children[0], + if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND) + { + Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); + returnNode = d_nm->mkNode( + kind::IAND, iAndOp, translated_children[0], translated_children[1]); + } + else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV) + { + // translate the children back to BV + Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); + Node x = translated_children[0]; + Node y = translated_children[1]; + Node bvx = d_nm->mkNode(intToBVOp, x); + Node bvy = d_nm->mkNode(intToBVOp, y); + // perform bvand on the bit-vectors + Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy); + // translate the result to integers + returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); + } + else + { + Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM); + // Construct a sum of ites, based on granularity. + Assert(translated_children.size() == 2); + Node newNode = createBitwiseNode(translated_children[0], translated_children[1], bvsize, options::BVAndIntegerGranularity(), &oneBitAnd); - returnNode = newNode; + returnNode = newNode; + } break; } case kind::BITVECTOR_SHL: |