在 Z3 超时中实现数组

Question

我正在尝试在 Z3 中实现我自己的数组版本，称为“记录”。它们只是由字符串索引的数组。我不断收到下面代码的超时，我不知道为什么。我知道我可以只使用普通数组，但我想确定这段代码的问题。

我对每个基本数组选择/存储公理都有一个断言。有什么问题吗？

(declare-sort Record)

(declare-fun storeR (Record String Int) Record)
(declare-fun selectR (Record String) Int)

;selct/store axioms for records
(assert (forall ((r Record)(s String)(i Int)) 
  (= (selectR (storeR r s i) s) i)))
(assert (forall ((r Record)(s String)(q String) (i Int)) 
  (or (= s q) (= (selectR (storeR r s i) q) (selectR r q) ))))
(assert (forall ((r Record)(q Record))
  (=> (forall ((s String)) (= (selectR r s) (selectR q s)))  (= r q))))


 (declare-const r Record)
 (assert (= (selectR r "number") 1))
 (check-sat)

Answer 1

文件以以下两行开始：

   (set-option :smt.auto_config false)
   (set-option :smt.mbqi       false)

然后 Z3 返回“未知”。使用 mbqi，z3 尝试（但失败）找到模型。