Z3 QBVFの質問

Question

前の議論をフォローアップ：

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

そして限りZ3に関しては

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

：Z3: Extracting existential model-values

は違いはありますか？つまり、後者のQBVFソルバーは自動的に取得されますか？ （素晴らしいです）

(eval (sx #x8000)) 

(check-sat)呼び出した後、それが正常に動作します：

また、実験時に私が発行することがわかりました。

(eval (sx (get-value (y)))) 

ああ、Z3はそれはinvalid function applicationだと文句を言い、そのクエリのために：私も言うことができるならばどのような方が良いだろうことです。そのようにしてeval関数を使用する方法はありますか？

ありがとうございます！

Answer 1

スクリプト

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

と

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

は等価ではありません。第二は、evalコマンドについて

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y)))) 

に実際equisatisfiableである、あなたは任意の未解釈の定数と関数シンボルを参照することができます。したがって、あなたが書くことができます。

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 
(check-sat) 
(eval (sx y)) 

yは普遍変数であるため、コマンド(eval (sx y))は、最初のスクリプトは動作しません。