小编Moo*_*ody的帖子

我有一个Alloy模型,其中包含以下内容:

abstract sig person{}

one sig john,Steve extends person  {Gender: man} 

sig man{}

fact {
  all name: person, Gender: man | 
      name.Gender = name.Gender => person =person}

如何在两个签名之间取得平等？

我的问题是“Distinct”在 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()

当我添加以下断言时，它应该给我 unsat 但它返回 sat：

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

这是否意味着我使用了错误的语法？