Closed keyboardDrummer closed 3 years ago
What happens if you don't have the rlimit
line? Also, just to check: do you mean Z3 itself times-out, or that you mean the instance doesn't finish in some time-limit you're controlling from the outside?
Just to make sure you know: 0
for rlimit
means "unlimited" (or, at least, it should do, but maybe your issue is saying it doesn't).
Thanks :)
What happens if you don't have the rlimit line?
I've removed the rlimit, it doesn't seem to affect the result.
Also, just to check: do you mean Z3 itself times-out, or that you mean the instance doesn't finish in some time-limit you're controlling from the outside?
The latter, I was running it on: https://rise4fun.com/Z3/slU9o
Running it in Z3 directly with (set-option :timeout 0)
causes Z3 to hang indefinitely and not return any output. If I configure (set-option :timeout 1000)
then it returns unknown
.
Is that expected behavior? The input I'm giving it seems pretty simple to solve.
Removing the not
causes it to return sat
as expected:
(declare-fun |byte#0| () Int)
(set-option :timeout 0)
(assert
(let ((anon0_correct (= (concat #x000000000000000000000000000000 ((_ int2bv 8) |byte#0|)) ((_ int2bv 128) |byte#0|))))
(=> (and (<= 0 |byte#0|) (<= |byte#0| 255)) anon0_correct))
)
(check-sat)
Okay, so the "easy" answer is that some problems are hard for an SMT solver and some are easy -- the size of the instance doesn't mean if something will be hard or easy (I have 3 line files that can take weeks to solve, even though they only use 32-bit numbers).
Your example creates two 128-bit values via int2bv
(which isn't actually in SMTLIB, it a Z3 extension); maybe this is just some case that Z3 isn't optimised to solve easily.
Given your original instance (the one with the not
) is UNSAT (based on your updated second comment), then it is possible that Z3 has to explore a search-space of ~2^128, which might just be extremely costly to show UNSAT.
Alright, thank you very much. As you correctly assessed I don't have a lot of context in this space but this was very educational :)
Given the condition (and (<= 0 |byte#0|) (<= |byte#0| 255))
, I would hope Z3 only iterates over 256 values. Is this something I could file a bug/feature-request for? I don't think I'm ready to solve this myself any time soon but maybe in time :)
So that's the more difficult part; I would guess that things are "going wrong" because of the int2bv
call, which impedes Z3's ability to apply simplifications/reductions/search tactics.
One way to test this would be to declare |byte#0|
as either a 128-bit BV or an 8 bit one, adjust your problem with either concat
or extract
, and then see how quick Z3 solves it ... but, if you do this, you're then solving a very different instance (it would be QF_BV vs. something like QF_BVLIA which your current instance probably is).
int2bv and bv2int are not part of SMTLIB standards. It is generally fairly expensive to use. I have added a helper axiom that could be useful generally and helps with this example. I might have to revert it if it introduces regressions.
it does now
Hey, thanks for reading.
Z3 doesn't terminate, at least not within minutes, on the following input:
Is this a bug or am I using it incorrectly?