Z3ソルバーZ3_parse_smtlib2_file - Z3 C APIプッシュポップ

Question

Z3_parse_smtlib2_file APIを使用してベンチマークを読み取る際に（プッシュ）と（ポップ）を使用する方法。 Z3_parse_smtlib2_file APIを使用して（assert（not（= o2_s o2_i）））および（assert（not（= o1_s o1_i）））制約の結果を取得するにはどうすればよいですか。 C.

(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))) 

Answer 1

にZ3_parse_smtlib2_fileのAPIを使用してベンチマークを読んでいる間だけ私は結果を取得しています（アサート（（= o1_s o1_i））ではない）これは、現在サポートされていません。 Z3_parse_smtlib2_fileはファイルからアサーションのみを抽出し、その他のほとんどのSMT2コマンドは無視します。 Z3は現在、後で変更できるSMT2コマンドのセットの抽出をサポートしていません。