2017-09-01 18 views
1

Z3_parse_smtlib2_file APIを使用してベンチマークを読み取る際に(プッシュ)と(ポップ)を使用する方法。 Z3_parse_smtlib2_file APIを使用して(assert(not(= o2_s o2_i)))および(assert(not(= 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))) 
+0

数式スタックから何かをポップしたら、それはなくなります。複数のファイルを同じ文脈にインクリメンタルに解析することができる場合は、ファイルを 'common'ファイル部分、' 1st push'部分と '2nd push'部分の3つに分割する必要があります。手動でプッシュし、手動でプッシュし、手動でプッシュし、第2プッシュ部分を解析し、充足可能性をチェックし、手動でポップします。 –

答えて

0

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