search

cvc5 / cvc5-projects

1 stars 0 forks source link

range of multiplication with bitvectors #335

Open kanigsson opened 3 years ago

kanigsson commented 3 years ago

Describe the bug

bv2nat.smt2.txt bvextend.smt2.txt

Not really a bug, more a question/discussion/feature request. I have attached two different formulations of a simple goal that states that if (a-b) is smaller than some large constant divided by idx, then (a-b)*idx is smaller than the large constant. The first formulation checks against the large constant in mathematical integers, the second file does everything in bitvectors using extend. Neither is currently proved by cvc4 in a reasonable amount of time.

Is there anything that can be done to prove any of the two goals? Thanks in advance.

CVC4 version/commit: cvc4 1.8 Operating system: linux

mpreiner commented 3 years ago

Hi @kanigsson, what is a reasonable amount of time? When I run current master it is solved within ~3min:

$ time bin/cvc5 bvextend.smt2 --bitblast=eager --bv-sat-solver=cadical
unsat

real    2m56.550s
user    2m56.277s
sys     0m0.067s

Note: You have to change the logic to QF_BV to make this work.

kanigsson commented 3 years ago

Hello, thanks for your answer. I hadn't really tried to play around with these options, in particular --bv-sat-solver, so it's good to know they exist, and that they help in this case. I had hoped for something more in the range of "a few seconds" for this simple consequence of monotonicity of multiplication/division. The issue is that the prover uses bitblasting I guess, instead of some built-in rules. We can't really set a restrictive logic such as QF_BV, as I showed to you the minimized version of the goal with all irrelevant context stripped. The context contains symbols that are not in QF_BV, and there is no simple method to remove the context (it's not easy to see it is irrelevant in an automatic way). Also, we can't really set command line options that are specific to a certain type of goal as we run the prover on many different goals, and they will not all benefit from these options. But I will try what these options do to our other goals.

mpreiner commented 3 years ago

The default for --bv-sat-solver will change soon to use the new bit-blasting solver, so runtime should improve, but it will still be minutes instead of seconds. I can take a look at possible word-level simplifications but this will take some time.

kanigsson commented 3 years ago

Thanks for looking into this. The new default sat-solver sounds promising. Just for the record, I'm not expecting any quick solutions, just want you to be aware of these use cases.