獨特的z3 SMT和python

Question

我的問題是，「獨特」在z3 python中工作嗎？我比較了下面的代碼，它似乎沒有給予同樣的結果：

(declare-const x Int) 
(declare-const y Int) 
(assert (distinct x y)) 
(check-sat) 
(get-model) 

結果是：

sat 

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

我加負說法只是爲了測試，結果是不飽和度是糾正：

(assert (= x y)) 

unsat 
Z3(6, 10): ERROR: model is not available 

但是當我使用的python Z3它給我總是坐在如下：

x = Int('x') 
y = Int('y') 
Distinct(x, y) 
s = Solver 
s = Solver() 
s.check() 

當我添加以下斷言它應該給我造成不滿意，但它返回坐下：

s.add(x == y) 
[y = 0, x = 0] 

這意味着，我用錯誤的語法？

Answer 1

「差別」功能只創建一個術語，它不會將其自身添加到解算器中。這是一個適用於我的例子：

x = Int('x') 
y = Int('y') 
d = Distinct(x, y) 

s = Solver() 
s.add(d) # SAT without this one, UNSAT with 
s.add(x == y) 
print s 
print s.check()