z3 数据日志中的否定表示最优性

Question

我使用 Z3 并将 :fixedpoint.engine 设置为 datalog。 我有一个枚举过滤器关系(f pos min max)。假设我们有(f #x10 #x100000 #x200000)、(f #x20 #x150000 #x200000) 和(f #x20 #x300000 #x500000)。

对于给定的x，我搜索最大的pos，使得(f pos min max) 和min <= x <= max（这里我使用间隔，但过滤器可以任意复杂）。优先级（排序t）和值（排序s）是位向量，但x、min 和max 位于相当大的空间（例如24 位）。

; configuration 
(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 match (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)
; Facts (EDB)
(rule (f #x10 #x100000 #x200000))
(rule (f #x20 #x150000 #x200000))
(rule (f #x20 #x300000 #x500000))
; Rules
(rule (=> (and (f p xmin xmax) (bvule xmin x) (bvule x xmax))
          (match p x)))
(rule (=> (and (match q x) (bvugt q p))
          (better p x)))
(rule (=> (and (match p x) (not (better p x)))
          (best p x)))
; Queries
(rule (=> (match p #x170000) (a p)))
(rule (=> (better #x10 #x170000) b))
(rule (=> (best #x10 #x170000) c))
; output: sat
; (or (= (:var 0) #x20) (= (:var 0) #x10))
(query (a p) :print-answer true)
; output: sat
(query b)
; Output 'WARNING: creating large table of size 16777216 for relation better' and fails
(query c)

• (match p x) 表示优先级过滤器p 过滤x。
• (better p x) 如果优先级高于 p 的规则过滤 x。
• (best p x) 与x 匹配的最佳过滤器具有优先级p 的代码。

如果我查询(match p #x170000)，我很快就会得到#x10 和#x20。如果我问(better #x10 #x170000) 我很快就会得到 优先级#20 的答案相同。但是(best p #x170000)上的查询未能在合理的时间和合理的空间内执行。

似乎(not (better p x)) 是独立于(match p x) 计算的，因此由一个非常大的表表示（x 的可能值不会被转发）。在某些情况下，我可以通过一些更好的技巧来限制x（有时我知道我只对明确出现在其他关系中的x 感兴趣），这样可以减少空间，但这是不是真正的通用解决方案，有时我被卡住了。

我应该如何重新表述这个问题，或者我应该使用哪些选项来避免这个问题？

Answer 1

Z3 的默认 Datalog 表超过了具体值，因此如果您使用较大的位向量，Z3 最终可能会创建巨大的表。 您可以尝试一个更简单的表数据结构，它支持较少的操作但它是稀疏的（使用“不关心”位）。 你可以试试：z3 fixedpoint.engine=datalog fixedpoint.datalog.default_relation=doc file.smt2