Z3求解器學習（一）

2021-10-09 10:44:49 字數 1195 閱讀 1919

安裝成功後在命令列輸入z3 -h可以檢視幫助學習如何使用，下面用幾個簡單的例子熟悉z3求解器的基本命令（這裡我們例子都使用z3 -in的輸入形式從標準輸入讀取表示式）：

例子1：首先寫乙個簡單的可滿足條件的例子

(declare-const a int)


(assert (> a 10))


(check-sat)


(get-model)
declare-const申明乙個給定型別的常量（int型的a)；

assert將乙個公式新增到z3內部堆疊中（a > 10);

check-sat判斷堆疊中的公式是否滿足。若滿足，為返回sat，並且可以通過get-model命令給出乙個使得所有公式為真的解釋模型；若不滿足，則返回unsat。

執行結果為：

sat

(model

(define-fun a () int

11))

表示找到乙個滿足公式的解釋a為11。具體格式為：

(define-fun a () int [val])
表示模型中的a值為[val]。

例子2：乙個約束不滿足的例子

(declare-const a int)


(assert (> a 10))


(assert (< a 10))


(check-sat)
執行結果為：

unsat

例子3：乙個約束無法求解的例子

(declare-const a int)


(assert (> (* a a) 3))


(declare-const b real)


(declare-const c real)


(assert (= (+ (* b b b) (* b c)) (* a 1000000))) 


(check-sat)
unknow

求解器Z3（未完，更新中）

首先解釋下 求解器 求解器 本為smt solver，翻譯成中文為求解器。顧名思義，求解就是解方程，但這裡不僅僅是一般的方程，這裡包括各種條件的廣義上的方程，例如不等於 位運算等。定義a b，條件a b,b 1。那麼它就會告訴你有解，a 3，b 2是乙個解。定義a b，條件a b,b a。那麼它就會...

z3安裝與學習

233333，聽說直接pip安裝的不太讓人愉悅。那就直接用原始碼安裝了。跟angr中的安裝相仿，先建立個虛擬環境 virtualenv z3 cd z3 source 路徑 z3 bin activate git clone cd z3 python scripts mk make.py pytho...

安裝z3模組

z3是microsoft research開發的高效能的定理證明工具。z3常常被用在許多應用中，如 軟體 硬體的驗證和測試，約束求解問題，混合系統分析，安全領域，生物學和幾何問題。使用的是國內的映象，秒下！迫不及待想感受一下z3的魅力了，下面有乙個數學題 花費100美元，購買正好100只動物。狗花費...