0

x div y == 2andの充足可能性をチェックしようとしましx / y == 2たが、両方とも間違った結果が得られました。Z3はまだこれらをサポートしていないようですか？ 

(declare-fun x () Int)
(declare-fun y () Int)

(assert (=  (div x y ) 2))

(check-sat)
(get-model)
(exit)

sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    38)
)



(declare-fun x () Int)
(declare-fun y () Int)

(assert (=  (/ x y ) 2))

(check-sat)
(get-model)
(exit)

sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    1)
)
4

1 に答える 1

1

整数除算がサポートされています。参照: http://smtlib.cs.uiowa.edu/theories/Ints.smt2

実数除算もサポートされています (ここから: http://smtlib.cs.uiowa.edu/theories/Reals.smt2 )。あなたが言及したゼロによる除算の問題はカバーされています:「SMT-LIB ロジックではすべての関数シンボルが(/ t 0)の形式の項は,実数のすべてのインスタンスで意味を持つ. しかし, 宣言はそれらの値に何の制約も課さない. これは特に, - すべてのインスタンス理論 T に対して, - すべての閉じた項に対してある種実数の t1 と t2、(= t1 (/ t2 0)) を満たす T のモデルが存在します。」

除数がゼロに等しくないというアサーションを追加する必要があります。

(assert (not (= y 0)))

例を次に示します (rise4fun リンク: http://rise4fun.com/Z3/IUDE ):

(declare-fun x () Int)
(declare-fun y () Int)

(assert (not (= y 0)))

(push)
(assert (=  (div x y ) 2))
(check-sat)
(get-model) ; gives x = 2, y = 1
(pop)

(push)
(assert (=  (/ x y ) 2))
(check-sat)
(get-model) ; gives x = -2, y = -1
(pop)
于 2013-11-12T16:05:12.617 に答える