large table warning for (declare-relation)

Question

$ z3 sat.smt2
WARNING: creating large table of size 16777216 for relation match1

The raw sat.smt file:

; (set-option :fixedpoint.engine datalog)
; sorts
(define-sort s () (_ BitVec 24))
(define-sort t () (_ BitVec 8))
; Relations 
(declare-rel f (t s s))
(declare-rel match1 (t s))
(declare-rel better (t s))
(declare-rel best (t s))
(declare-rel a (t))
(declare-rel b ())
(declare-rel c ())
(declare-var x s)
(declare-var xmin s)
(declare-var xmax s)
(declare-var p t)
(declare-var q t)

; Rules
(rule (=> (and (f p xmin xmax) (bvsle xmin x) (bvsle x xmax)) 
      (match1 p x)))
(rule (=> (and (match1 q x) (bvslt q p))
      (better p x)))
(rule (=> (and (not (better p x)) (match1 p x))
     (best p x)))
; Facts (EDB)
(rule (f #x10 #x100000 #x200000))
(rule (f #x20 #x150000 #x200000))
(rule (f #x20 #x300000 #x500000))

; Queries 
(rule (=> (best #x10 #x170000) c))

; Output 'WARNING: creating large table of size 16777216 for relation better' and fails
(query c)

How to solve the problem and why? The version of z3 is Z3 version 4.8.13 - 64 bit. And how to add all the declarations and queries so that the example can be run.

Answer 1

There isn't much you can do, other than reducing the bit-vector sizes you use. Quoting from https://github.com/Z3Prover/z3/issues/1698#issuecomment-399577761:

It is a design decision. The bottom up data log engine that uses hash tables can at most hold relations with a few million entries. So using large bit vectors for that engine is not a good match.

Your problem requires z3 to build extremely large internal tables, which is extremely expensive. The question is why do you need such large bit vectors? Can you get away with a much smaller bit-vector size? You haven't said anything about what you're trying to model, so it's hard to hazard a guess. See if you can "abstract" away these numbers and use much smaller bit-vectors to model the problem to start with.