diff options
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 68 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 22 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int_elim_err.smt2 | 7 |
4 files changed, 54 insertions, 46 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index e2a38b028..5b125b4b6 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -184,43 +184,41 @@ Node BVToInt::eliminationPass(Node n) (d_eliminationCache.find(current) != d_eliminationCache.end()); bool inRebuildCache = (d_rebuildCache.find(current) != d_rebuildCache.end()); - if (!inRebuildCache) + if (!inEliminationCache) { - // current is not the elimination of any previously-visited node - if (!inEliminationCache) - { - // current hasn't been eliminated yet. - // eliminate operators from it - Node currentEliminated = - FixpointRewriteStrategy<RewriteRule<UdivZero>, - RewriteRule<SdivEliminate>, - RewriteRule<SremEliminate>, - RewriteRule<SmodEliminate>, - RewriteRule<RepeatEliminate>, - RewriteRule<ZeroExtendEliminate>, - RewriteRule<SignExtendEliminate>, - RewriteRule<RotateRightEliminate>, - RewriteRule<RotateLeftEliminate>, - RewriteRule<CompEliminate>, - RewriteRule<SleEliminate>, - RewriteRule<SltEliminate>, - RewriteRule<SgtEliminate>, - RewriteRule<SgeEliminate>, - RewriteRule<ShlByConst>, - RewriteRule<LshrByConst> >::apply(current); - // save in the cache - d_eliminationCache[current] = currentEliminated; - // put the eliminated node in the rebuild cache, but mark that it hasn't - // yet been rebuilt by assigning null. - d_rebuildCache[currentEliminated] = Node(); - // Push the eliminated node to the stack - toVisit.push_back(currentEliminated); - // Add the children to the stack for future processing. - toVisit.insert( - toVisit.end(), currentEliminated.begin(), currentEliminated.end()); - } + // current hasn't been eliminated yet. + // eliminate operators from it + Node currentEliminated = + FixpointRewriteStrategy<RewriteRule<UdivZero>, + RewriteRule<SdivEliminate>, + RewriteRule<SremEliminate>, + RewriteRule<SmodEliminate>, + RewriteRule<RepeatEliminate>, + RewriteRule<ZeroExtendEliminate>, + RewriteRule<SignExtendEliminate>, + RewriteRule<RotateRightEliminate>, + RewriteRule<RotateLeftEliminate>, + RewriteRule<CompEliminate>, + RewriteRule<SleEliminate>, + RewriteRule<SltEliminate>, + RewriteRule<SgtEliminate>, + RewriteRule<SgeEliminate>, + RewriteRule<ShlByConst>, + RewriteRule<LshrByConst> >::apply(current); + // save in the cache + d_eliminationCache[current] = currentEliminated; + // also assign the eliminated now to itself to avoid revisiting. + d_eliminationCache[currentEliminated] = currentEliminated; + // put the eliminated node in the rebuild cache, but mark that it hasn't + // yet been rebuilt by assigning null. + d_rebuildCache[currentEliminated] = Node(); + // Push the eliminated node to the stack + toVisit.push_back(currentEliminated); + // Add the children to the stack for future processing. + toVisit.insert( + toVisit.end(), currentEliminated.begin(), currentEliminated.end()); } - else + if (inRebuildCache) { // current was already added to the rebuild cache. if (d_rebuildCache[current].isNull()) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bb09a6dc0..e3b1163fc 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -357,6 +357,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } } + + if (options::solveBVAsInt() > 0) + { + /** + * Operations on 1 bits are better handled as Boolean operations + * than as integer operations. + * Therefore, we enable bv-to-bool, which runs before + * the translation to integers. + */ + options::bitvectorToBool.set(true); + } + // Disable options incompatible with unsat cores and proofs or output an // error if enabled explicitly if (options::unsatCores() || options::proof()) @@ -413,16 +425,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) options::preSkolemQuant.set(false); } - if (options::solveBVAsInt() > 0) - { - /** - * Operations on 1 bits are better handled as Boolean operations - * than as integer operations. - * Therefore, we enable bv-to-bool, which runs before - * the translation to integers. - */ - options::bitvectorToBool.set(true); - } if (options::bitvectorToBool()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5ae66f203..690135b54 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -215,8 +215,9 @@ set(regress_0_tests regress0/bv/bv_to_int2.smt2 regress0/bv/bv_to_int_bvmul1.smt2 regress0/bv/bv_to_int_bvmul2.smt2 - regress0/bv/bv_to_int_zext.smt2 regress0/bv/bv_to_int_bitwise.smt2 + regress0/bv/bv_to_int_elim_err.smt2 + regress0/bv/bv_to_int_zext.smt2 regress0/bv/bvuf_to_intuf.smt2 regress0/bv/bvuf_to_intuf_smtlib.smt2 regress0/bv/bvuf_to_intuf_sorts.smt2 diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 new file mode 100644 index 000000000..16731b01e --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models +; EXPECT: sat +(set-logic QF_BV) +(declare-fun _substvar_183_ () (_ BitVec 32)) +(assert (let ((?x15 ((_ sign_extend 0) _substvar_183_))) (bvsle ((_ zero_extend 24) ((_ extract 15 8) (bvadd ?x15 (_ bv4294966758 32)))) (bvadd ?x15 ?x15)))) +(check-sat) +(exit) |