Z3解決方案Z3_parse_smtlib2_file - Z3 C API推動彈出

如何在使用Z3_parse_smtlib2_file API讀取基準測試時使用（推送）和（彈出）。如何使用Z3_parse_smtlib2_file API獲取（assert（not（= o2_s o2_i）））和（assert（not（= o1_s o1_i）））約束的結果。我得到的結果爲（斷言（不是（= o1_s o1_i）））只，而在C.Z3解決方案Z3_parse_smtlib2_file - Z3 C API推動彈出

(declare-fun i_s() Int) 
(declare-fun t_s() Int) 
(declare-fun o1_s() Int) 
(declare-fun o2_s() Int) 
(declare-fun i_i() Int) 
(declare-fun t_i() Int) 
(declare-fun o1_i() Int) 
(declare-fun o2_i() Int) 

(assert(= i_s 10)) 
(assert(>= (+ (- 5) (* 1 i_s)) 0)) 
(assert(= t_s (+ 1 (* 1 i_s)))) 
(assert(< (+ (- 20) (* 1 t_s)) 0)) 
(assert(= o1_s (+ 1 (* 1 t_s)))) 
(assert(= o2_s (+ 0 (* 1 t_s)))) 

(assert(= i_i 10)) 
(assert(>= (+ (- 5) (* 1 i_i)) 0)) 
(assert(= t_i (+ 2 (* 1 i_i)))) 
(assert(< (+ (- 21) (* 1 t_i)) 0)) 
(assert(= o1_i (+ 0 (* 1 t_i)))) 
(assert(= o2_i (+ 0 (* 1 t_i)))) 

(push) 

(assert(not(= o2_s o2_i))) 
(pop) 
(assert(not(= o1_s o1_i)))

來源

2017-09-01 user2468460

一旦你從公式堆棧中彈出一些東西，它就消失了。如果可以將多個文件逐步解析到相同的上下文中，那麼您應該將文件拆分爲3：「公用」文件部分，「第一推」部分和「第二推」部分;然後解析'common'部分，手動推送，解析'1st push'部分，檢查可滿足性，手動彈出+手動推送，解析'2nd push'部分，檢查可滿足性，手動彈出。 –

閱讀使用Z3_parse_smtlib2_file API基準這是目前不支持。 Z3_parse_smtlib2_file僅提取文件中的斷言並忽略大多數其他SMT2命令。 Z3目前不支持提取可以稍後修改的一組SMT2命令。

來源

2017-09-07 13:34:12

Z3解決方案Z3_parse_smtlib2_file - Z3 C API推動彈出

回答

相關問題