（声明关系）的大表警告答案

【问题标题】：large table warning for (declare-relation)（声明关系）的大表警告
【发布时间】：2022-01-17 10:38:51
【问题描述】：

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

原始 sat.smt 文件：

; (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)

如何解决问题，为什么？ z3 的版本是 Z3 版本 4.8.13 - 64 位。以及如何添加所有声明和查询以便示例可以运行。

【问题讨论】：

您使用的是什么版本的 z3。对我来说，它产生unsat。我正在运行版本 4.8.14。如果您使用的是旧版本，则可能需要升级。
我之前对Queries的定义是错误的，我又修改了代码。警告未解决。

标签： z3 datalog

【解决方案1】：

除了减少使用的位向量大小之外，您无能为力。引用https://github.com/Z3Prover/z3/issues/1698#issuecomment-399577761:

这是一个设计决定。使用哈希表的自下而上数据日志引擎最多可以保存几百万个条目的关系。所以对那个引擎使用大的位向量并不是一个很好的匹配。

您的问题需要 z3 构建非常大的内部表，这非常昂贵。问题是为什么需要这么大的位向量？你能摆脱更小的位向量大小吗？你还没有说你想要建模的东西，所以很难猜测。看看您是否可以“抽象”掉这些数字并使用更小的位向量来对问题进行建模。

【讨论】：