Z3公式無法合成檢查

以下SMT公式無法在rise4fun站點進行句法檢查，此時x13被帶有箭頭的行中的av5替換。Z3公式無法合成檢查

(set-info :status unknown) 
;(set-logic QF_BV) 
(declare-fun in3() (_ BitVec 16)) 
(assert 
(let ((x8 ((_ zero_extend 16) in3))) 
(let ((x13 (ite (not (= x8 (_ bv00000000 32))) (_ bv00045069 32) (_ bv00000174 32)))) 
(let ((av5 (= x13 (_ bv00045069 32)))) 
(= x13 (_ bv4294967295 32)))))) <--------- 
(assert true) 
(check-sat)

的錯誤消息是

Z3（8,26）：錯誤：無效的功能應用，在位置2

在參數排序不匹配任何想法，我可能我是做錯了什麼？

來源

2013-02-14 Venkatesh-Prasad Ranganath

你能舉一個你的rise4fun例子的鏈接嗎？ – GManNickG 2013-02-14 21:51:53

該示例的固定鏈接是http://rise4fun.com/Z3/on1pl。 – 2013-02-15 02:37:19

你使用的是哪個版本？我無法使用版本4.3.x重現此問題，也無法使用unstable（正在進行中）分支。在這兩種情況下，我得到了unsat。在rise4fun上我也得到unsat。

來源

2013-02-14 20:47:47

我目前正在rise4fun上試用它。而且，我在http://rise4fun.com/z3/tutorial/guide和rise4fun.com/Z3/on1pl上遇到同樣的問題。順便說一句，rise4fun是在便箋式模式下的理想選擇。它讓我想起IPython筆記本。我認爲這將有助於擴大與筆記本電腦支持rise4fun。試試http://nbviewer.ipython.org/上的筆記本。 – 2013-02-15 02:43:06

在鏈接：rise4fun.com/Z3/on1pl中，av5是一個布爾值。這就是爲什麼你在'（= av5（_ bv4294967295 32））'處出現「排序不匹配」的原因。 – 2013-02-15 18:58:18

關於Rise4Fun，我同意擁有類似筆記本的支持會很棒。如果我們可以使用基於wiki的界面在線創建教程和內容，那將會很棒。 – 2013-02-15 19:00:06

Z3公式無法合成檢查

回答

相關問題