From b23a368e85a43d6bcb784e5f9da1e58fa1d913cc Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Thu, 29 Aug 2024 16:26:02 +0300 Subject: [PATCH] not good --- src/options/uf_options.toml | 23 +++++------ src/theory/uf/conversions_solver.cpp | 29 ++++++++----- src/theory/uf/theory_uf_rewriter.cpp | 41 ++++++++++++++++++- .../cli/regress0/bv-conv-value-refine.smt2 | 2 +- .../cli/regress0/bv2nat_lemma_ranges_1.smt2 | 6 +-- .../cli/regress0/bv2nat_reflection1.smt2 | 2 +- 6 files changed, 74 insertions(+), 29 deletions(-) diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index a133f14bc30..2415643fc07 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -84,17 +84,16 @@ name = "Uninterpreted Functions Theory" help = "eagerly expand bit-vector to arithmetic conversions during preprocessing" [[option]] - name = "bv2natPlusDistRR" + name = "arithBvConvMode" category = "expert" - long = "bv2nat-plus-dist-rr" - type = "bool" - default = "false" - help = "distribute bv2nat over addition in a rewrite rule" - -[[option]] - name = "modelBasedArithBvConv" - category = "expert" - long = "model-based-arith-bv-conv" - type = "bool" - default = "false" + long = "model-based-arith-bv-conv=MODE" + type = "ArithBVConvMode" + default = "VALUES" help = "model-based inferences for bit-vector to arithmetic conversions" + help_mode = "How to convert" +[[option.mode.VALUES]] + name = "values" + help = "model values" +[[option.mode.LEMMAS]] + name = "lemmas" + help = "lemmas" diff --git a/src/theory/uf/conversions_solver.cpp b/src/theory/uf/conversions_solver.cpp index 5d5a7cde09a..609c0720598 100644 --- a/src/theory/uf/conversions_solver.cpp +++ b/src/theory/uf/conversions_solver.cpp @@ -77,9 +77,9 @@ void ConversionsSolver::checkReduction(Node n) Trace("bv-convs") << "...already correct in model" << std::endl; return; } - if (options().uf.modelBasedArithBvConv) + NodeManager* nm = NodeManager::currentNM(); + if (options().uf.arithBvConvMode == options::ArithBVConvMode::VALUES) { - NodeManager* nm = NodeManager::currentNM(); Node argval = d_state.getModel()->getValue(n[0]); Trace("bv-convs-debug") << " arg value = " << argval << std::endl; Node eval = rewrite(nm->mkNode(n.getOperator(), argval)); @@ -87,18 +87,25 @@ void ConversionsSolver::checkReduction(Node n) Node lem = nm->mkNode(Kind::IMPLIES, n[0].eqNode(argval), n.eqNode(eval)); d_im.lemma(lem, InferenceId::UF_ARITH_BV_CONV_VALUE_REFINE); - if (n.getKind() == Kind::BITVECTOR_TO_NAT) { - Node zero = nm->mkConstInt(Rational(0)); - uint32_t k = n[0].getType().getBitVectorSize(); - Node max_val = nm->mkConstInt(Rational(Integer(2).pow(k))); - Node lower_bound = nm->mkNode(Kind::LEQ, zero, n); - Node upper_bound = nm->mkNode(Kind::LEQ, n, max_val); - Node range_lemma = nm->mkNode(Kind::AND, lower_bound, upper_bound); + return; + } + + + if ((options().uf.arithBvConvMode == options::ArithBVConvMode::LEMMAS) && n.getKind() == Kind::BITVECTOR_TO_NAT) { + Node zero = nm->mkConstInt(Rational(0)); + uint32_t k = n[0].getType().getBitVectorSize(); + Node max_val = nm->mkConstInt(Rational(Integer(2).pow(k))); + + Node lower_bound = nm->mkNode(Kind::LEQ, zero, n); + Node upper_bound = nm->mkNode(Kind::LEQ, n, max_val); + Node range_lemma = nm->mkNode(Kind::AND, lower_bound, upper_bound); + std::cout << "panda " << d_state.getModel()->getValue(range_lemma) << std::endl; + //if (d_state.getModel()->getValue(range_lemma) == nm->mkConst(false)) + { d_im.lemma(range_lemma, InferenceId::UF_ARITH_BV_CONV_RANGE); + return; } - - return; } Node lem; diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp index 5ca660e3698..c1301af4739 100644 --- a/src/theory/uf/theory_uf_rewriter.cpp +++ b/src/theory/uf/theory_uf_rewriter.cpp @@ -336,7 +336,7 @@ RewriteResponse TheoryUfRewriter::rewriteBVToNat(TNode node) return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } else if (node[0].getKind() == Kind::BITVECTOR_ADD) { - // if (options().uf.bv2natPlusDistRR) + //if (options().uf.bv2natDistRR) { std::vector bv2nats; for (Node child : node[0]) { @@ -350,6 +350,45 @@ RewriteResponse TheoryUfRewriter::rewriteBVToNat(TNode node) return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } } + else if (node[0].getKind() == Kind::BITVECTOR_MULT) { + //if (options().uf.bv2natDistRR) + { + std::vector bv2nats; + for (Node child : node[0]) { + Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child); + bv2nats.push_back(bv2nat); + } + const uint32_t size = node[0].getType().getBitVectorSize(); + Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size))); + Node multiplication = nm->mkNode(Kind::MULT, bv2nats); + Node resultNode = nm->mkNode(Kind::INTS_MODULUS_TOTAL, multiplication, twottsize); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } + else if (node[0].getKind() == Kind::BITVECTOR_NEG) { + //if (options().uf.bv2natDistRR) + { + Node child = node[0][0]; + Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child); + Node plusOne = nm->mkNode(Kind::ADD, bv2nat, nm->mkConstInt(Rational(Integer(2)))); + const uint32_t size = node[0].getType().getBitVectorSize(); + Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size))); + Node resultNode = nm->mkNode(Kind::SUB, twottsize, plusOne); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } + else if (node[0].getKind() == Kind::BITVECTOR_NOT) { + //if (options().uf.bv2natDistRR) + { + Node child = node[0][0]; + Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child); + const uint32_t size = node[0].getType().getBitVectorSize(); + Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size))); + Node sub = nm->mkNode(Kind::SUB, twottsize, bv2nat); + Node resultNode = nm->mkNode(Kind::INTS_MODULUS_TOTAL, sub, twottsize); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } return RewriteResponse(REWRITE_DONE, node); } diff --git a/test/regress/cli/regress0/bv-conv-value-refine.smt2 b/test/regress/cli/regress0/bv-conv-value-refine.smt2 index 00473b3af5c..9173c6858e8 100644 --- a/test/regress/cli/regress0/bv-conv-value-refine.smt2 +++ b/test/regress/cli/regress0/bv-conv-value-refine.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --model-based-arith-bv-conv +; COMMAND-LINE: --model-based-arith-bv-conv=values ; EXPECT: sat (set-logic ALL) (declare-fun x () (_ BitVec 8)) diff --git a/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 index f2b4349aa00..51840561c06 100644 --- a/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 +++ b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --model-based-arith-bv-conv +; COMMAND-LINE: --model-based-arith-bv-conv=lemmas ; EXPECT: unsat (set-logic ALL) -(declare-fun x () (_ BitVec 4000)) -(declare-fun y () (_ BitVec 4000)) +(declare-fun x () (_ BitVec 4)) +(declare-fun y () (_ BitVec 4)) (assert (< (bv2nat x) (bv2nat y) )) (assert (= (+ (bv2nat x) (bv2nat y)) 0)) (check-sat) diff --git a/test/regress/cli/regress0/bv2nat_reflection1.smt2 b/test/regress/cli/regress0/bv2nat_reflection1.smt2 index bdc9c16ceb5..22f54e1aa06 100644 --- a/test/regress/cli/regress0/bv2nat_reflection1.smt2 +++ b/test/regress/cli/regress0/bv2nat_reflection1.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --model-based-arith-bv-conv +; COMMAND-LINE: --model-based-arith-bv-conv=values (set-logic ALL) (declare-fun x () (_ BitVec 4000)) (declare-fun y () (_ BitVec 4000))