我将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
)是BitVectors,但是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
感兴趣),以减少空间,但这不是真正的通用解决方案,有时我被困住了。我应该如何改写该问题,或者应该使用哪些选项来避免此问题?
最佳答案
Z3的默认Datalog表超出了具体值,因此,如果使用大的位向量,Z3可能最终会创建巨大的表。
您可以尝试使用更简单的表数据结构,该结构支持较少的操作,但稀疏(使用“无关”位)。
您可以使用以下方法进行尝试:z3 fixedpoint.engine = datalog fixedpoint.datalog.default_relation = doc file.smt2
关于z3 - z3数据日志中的否定表示最优性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/49372849/