QF_UFBV performance

[LeventErkok]

For the attached UFBV benchmark, Z3 is performing rather badly compared to other solvers I tried:

• ABC: 0.194378s
• Boolector: 15.364773s
• Yices: 49.521083s
• MathSAT: 578.125045s

I killed the process after 10 minutes where z3 failed to produce unsat. (CVC4 was also part of my tests, which also failed to produce a result in 10 minutes.)

I understand going after individual benchmarks can be a never ending goose-chase, but thought you guys might want to look at this one given the compared performance with other tools.

test.smt2.txt

[wintersteiger]

Just to confirm: this is QF_UFBV (no quantifiers). Of course, it's completely expected that Z3 does not perform as good as other tools on at least one of the benchmarks. Does it also outperform the other tools on at least one benchmark?

Further, in the presence of UFs, Z3 is forced to use the oldest, slowest solver and it can't use the pure, new, fast SAT solver. We'd be very happy about improvements on that end, but afaik nobody is currently working on this.

[LeventErkok]

@wintersteiger Yes, QF_UFBV, no quantifiers are present.

I'm not quite sure how Z3 compares to others on QF_UFBV; but this test case stood out in my test suite. (I usually only test with Z3, unless there's a case that seems to be a bottleneck. Then I try others.)

Use of UFs: Unfortunately UF's are part of the general story for me. I guess it can also be coded using arrays, but that's not what the backend generates currently. (And I had better luck with UFs compared to Arrays in the past.) In essence, any time there's a table-lookup I end up creating UFs. Would be really nice if the new solver supported UFs!

[delcypher]

@LeventErkok Just to note the ackermannize_bv tactic might be able to help you here.

I started experiment with a custom tactic that tries to reduce the problem to QF_BV in simple cases for KLEE ( see klee/klee#653 ). I haven't found time to properly evaluate this yet but you might find this useful.

[delcypher]

@LeventErkok Sorry looks like this doesn't help. Using

(apply (and-then simplify bvarray2uf ackermannize_bv (using-params simplify :elim_and true)) :print-benchmark true :print false)

doesn't remove the UF function.

It would be nice if there was a Z3 tactic that could replace all applications of table0 with a nested ite expression that would branch on the constant argument values and introduce the number of fresh variables required to be sound for the cases that the argument to table0 is outside the defined table values (To be sound I'm guessing the upper bound on the number of fresh variables would be the number of applications of the table0 function in the query. Might not work if there are recursive functions because then we don't know the upper bound on the applications of table0).

@wintersteiger @NikolajBjorner Does a tactic doing what I describe exist?

[NikolajBjorner]

Thanks for the example.

It is a very good case for bit-width reduction as the 64 bits can be reduced to 8 with some analysis. Even the bvule tests with #000...000100 should be possible to eliminate with a suitable strong analysis (because bit-wise and with #0000...000ff always produces 8 bits worth). After manual bit-width reduction it solves in 0.05s, but of course you could use something automatic and reusable.

[wintersteiger]

@delcypher : Indeed, you can use the ackermannization for this type of query, but you don't need bvarray2uf. The reason that ackermannize_bv didn't have the intended result is that it is limited to introducing only a very limited number of additional constraints (by default) and you had no way to guess the magic option name to change that limit (yeah, we need to clean that up...):

(apply (using-params ackermannize_bv :div0_ackermann_limit 1000000))

And, using that information to build a sat checking tactic:

(check-sat-using (then (using-params ackermannize_bv :div0_ackermann_limit 1000000) simplify bit-blast sat))

yields unsat in 21 seconds on my machine.

[delcypher]

@wintersteiger

@delcypher : Indeed, you can use the ackermannization for this type of query, but you don't need bvarray2uf. The reason that ackermannize_bv didn't have the intended result is that it is limited to introducing only a very limited number of additional constraints (by default) and you had no way to guess the magic option name to change that limit (yeah, we need to clean that up...):

Thanks that's good to know. I saw the option

- ackermannize_bv A tactic for performing full Ackermannization on bv instances.               
    div0_ackermann_limit (unsigned int) a bound for number of congruence Ackermann lemmas for div0 modelling (default: 1000)  

but I ignored it because I thought it was related to division. To be honest even if it didn't say div0 I still wouldn't know what it did because it uses terminology I'm not familiar with.

[LeventErkok]

@wintersteiger Fantastic! I can confirm that on my rather old Mac the proof gets completed in 21 seconds as well with your magic incantation!

[delcypher]

@LeventErkok If you want to this more robust you could combine this with a probe. Something like this might do it.

(check-sat-using
  (or-else
    (and-then
      simplify
      (using-params ackermannize_bv :div0_ackermann_limit 1000000)
      (if is-qfbv qfbv fail)
    )
    qfaufbv
  )
)

After applying ackermannize_bv the probe checks if the constraints are now in the qfbv logic. If so it applies qfbv (you could replace this @wintersteiger 's additional steps to invoke the SAT solver) otherwise it falls back to the qfaufbv tactic.

[LeventErkok]

@delcypher Thanks! I'm still quite new to the tactic language, but the above is definitely helpful. Maybe these recipes can be added to the tutorial somehow?

Also @NikolajBjorner mentioned he can get this benchmark to run in half a second here: #1150 (comment), but I think that was a manual tweak as opposed to a tactic. I wonder if it's possible to achieve the same with a tactic too.

[NikolajBjorner]

There is at this point no tactic to perform the simplifications I did by hand (and the ones I did could easily have been unsound). Examples like these are useful to learn from.