From dfdcc4c68d8716b4587fd0316818c319ef7cff20 Mon Sep 17 00:00:00 2001 From: makaimann Date: Mon, 6 Dec 2021 18:16:09 -0800 Subject: [PATCH] Add bitwise option to IntBlaster (#7721) This is part of a series of PRs by @yoni206 to add full int-blasting support to the master branch of `cvc5`. This adds support for the bitwise encoding to `IntBlaster`. Future PRs would unify the `bv2int` and `IntBlaster` helper functions. --- src/options/smt_options.toml | 3 ++ src/preprocessing/passes/bv_to_int.cpp | 6 +++ src/theory/bv/int_blaster.cpp | 37 ++++++++++++++++ .../theory/theory_bv_int_blaster_white.cpp | 42 ++++++++++++++++++- 4 files changed, 87 insertions(+), 1 deletion(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 2e2742e73..026c8f494 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -395,6 +395,9 @@ name = "SMT Layer" [[option.mode.BV]] name = "bv" help = "Translate bvand back to bit-vectors" +[[option.mode.BITWISE]] + name = "bitwise" + help = "Introduce a UF operator for bvand, and eagerly add bitwise lemmas" [[option]] name = "BVAndIntegerGranularity" diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 33f3dd445..f106f1ccf 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -27,6 +27,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" #include "expr/skolem_manager.h" +#include "options/option_exception.h" #include "options/smt_options.h" #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" @@ -938,6 +939,11 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext) d_nm = NodeManager::currentNM(); d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); + + if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BITWISE) + { + throw OptionException("bitwise option is not supported currently"); + } }; PreprocessingPassResult BVToInt::applyInternal( diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 649be5aab..0109649f0 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -547,6 +547,11 @@ Node IntBlaster::translateWithChildren( case kind::BOUND_VAR_LIST: { returnNode = d_nm->mkNode(oldKind, translated_children); + if (d_mode == options::SolveBVAsIntMode::BITWISE) + { + throw OptionException( + "--solve-bv-as-int=bitwise does not support quantifiers"); + } break; } case kind::FORALL: @@ -1008,6 +1013,38 @@ Node IntBlaster::createBVAndNode(Node x, // Construct a sum of ites, based on granularity. returnNode = d_iandUtils.createSumNode(x, y, bvsize, d_granularity); } + else + { + Assert(d_mode == options::SolveBVAsIntMode::BITWISE); + // Enforce semantics over individual bits with iextract and ites + uint64_t granularity = options::BVAndIntegerGranularity(); + + Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); + Node iAnd = d_nm->mkNode(kind::IAND, iAndOp, x, y); + // get a skolem so the IAND solver knows not to do work + returnNode = d_nm->getSkolemManager()->mkPurifySkolem( + iAnd, + "__intblast__iand", + "skolem for an IAND node in bitwise mode " + iAnd.toString()); + addRangeConstraint(returnNode, bvsize, lemmas); + + // eagerly add bitwise lemmas according to the provided granularity + uint64_t high_bit; + for (uint64_t j = 0; j < bvsize; j += granularity) + { + high_bit = j + granularity - 1; + // don't let high_bit pass bvsize + if (high_bit >= bvsize) + { + high_bit = bvsize - 1; + } + Node extractedReturnNode = d_iandUtils.iextract(high_bit, j, returnNode); + addBitwiseConstraint( + extractedReturnNode.eqNode( + d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j)), + lemmas); + } + } return returnNode; } diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 2ad8695de..0412fdabb 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -130,7 +130,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) } /** Check all cases of the translation. - * This is a sanity check, that noly verifies + * This is a sanity check, that only verifies * the expected type, and that there were no * failures. */ @@ -280,5 +280,45 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) ASSERT_TRUE(result.getType().isInteger()); } +/** Check AND translation for bitwise option. + * This is a sanity check, that only verifies + * the expected kind, and that there were no + * failures. + */ +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise) +{ + // place holders for lemmas and skolem + std::vector lemmas; + std::map skolems; + Options opts; + Env env(d_nodeManager, &opts); + env.d_logic.setLogicString("QF_UFBV"); + env.d_logic.lock(); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1, true); + + // bit-vector variables + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + Node v1 = d_nodeManager->mkVar("v1", bvType); + Node v2 = d_nodeManager->mkVar("v2", bvType); + + // translated integer variables + Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems); + Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems); + + // if original is BV, result should be Int. + // Otherwise, they should have the same type. + Node original; + Node result; + + // bvand + original = d_nodeManager->mkNode(BITVECTOR_AND, v1, v2); + size_t orig_num_lemmas = lemmas.size(); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + // should have kind skolem, would use bitwise comparisons to refine + ASSERT_TRUE(result.getKind() == kind::SKOLEM); + // check that a lemma was added + ASSERT_TRUE(lemmas.size() > orig_num_lemmas); +} + } // namespace test } // namespace cvc5 -- 2.30.2