在Z3中實現數組超時

我想在Z3中實現我自己的數組版本，名爲「記錄」。他們只是由字符串索引的數組。我不斷收到下面的代碼超時，我不明白爲什麼。我知道我可以使用正常的數組，但我想確定這個代碼的問題。在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)

來源

2016-04-21 user3712482

與以下兩行啓動文件：

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

然後Z3返回「未知」。隨着mbqi，z3嘗試（並失敗）找到一個模型。

來源

2016-04-21 02:54:42

嗯，你有什麼想法爲什麼會失敗？這些不僅僅是規範的數組選擇/存儲公理？ – user3712482

在Z3中實現數組超時

回答

相關問題