Z3 SMT求解器中的常数相等 [英] Equality for constants in Z3 SMT solver

问题描述

我正在使用Microsoft的Z3 SMT求解器，并且试图定义自定义类型的常量.默认情况下，此类常量似乎并非不相等.假设您有以下程序:

I am using the Z3 SMT solver by Microsoft, and I am trying to define constants of a custom sort. It seems like such constants are not unequal by default. Suppose you have the following program:

(declare-sort S 0)

(declare-const x S)
(declare-const y S)

(assert (= x y))
(check-sat)

这将给出"sat"，因为相同类型的两个常量当然完全有可能相等.由于我正在建立常量必须彼此不同的模型，因此这意味着我需要添加形式的公理

This will give "sat", because it is of course perfectly possible that two constants of the same sort are equal. Since I am making model in which constants have to be different from each other, this means that I would need to add an axiom of the form

(assert (not (= x y)))

用于相同种类的每对常量.我想知道是否有某种方法可以实现这种通用性，以便默认情况下排序中的每个常量都是唯一的.

for every pair of constants of the same sort. I was wondering if there is some way to do this generic, so that each constant of a sort is unique by default.

推荐答案

您可以使用数据类型对许多编程语言中的枚举类型进行编码.在下面的示例中，排序S具有三个元素，并且它们彼此不同.

You can use datatypes to encode enumeration types found in many programming languages. In the following example, the sort S has three elements and they are different from each other.

(declare-datatypes () ((S a b c)))

这是一个完整的示例: http://rise4fun.com/Z3/ncPc

Here is a complete example: http://rise4fun.com/Z3/ncPc

(declare-datatypes () ((S a b c)))

(echo "a and b are different")
(simplify (= a b))

; x must be equal to a, b or c
(declare-const x S)

; since x != a, then it must be b or c
(assert (not (= x a)))
(check-sat)
(get-model)
; in the next check-sat x must be c
(assert (not (= x b)))
(check-sat)
(get-model)

另一种可能性是使用distinct.

(assert (distinct a b c d e))

这篇关于Z3 SMT求解器中的常数相等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！