不带量词的 z3 数据类型匹配
z3 datatype matching without a quantifier
假设我在 z3 中创建了一个数据类型 A:
(declare-datatypes () ((A (b (bx Int)) (c (cx Int)))))
现在，我可以声明一个变量 t，然后断言 t 是一个 c 类型：
(declare-fun t () A)
(assert (exists ((x Int)) (= t (c x))))
但是，这需要存在量词。我的问题是：是否可以 不使用 量词？
具体来说，我想要一个表达式，例如 is_c t 之类的，它相当于 (exists ((x Int)) (= t (c x))).
我原以为这会很简单，因为在大多数具有求和类型的函数式编程语言中，它们都有一个消除形式，通常是模式匹配，例如 match t of b x => false; c x => true。但我无法在 z3 文档中找到任何此类性质的内容。有什么我想念的吗？
您会自动获得一个测试器，作为索引标识符：(_ is c) 每个构造函数 c。
参见 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.2.3 节。相关部分在第61页（第二段）：
On successfully executing this command, for each constructor c in a
declared datatype δ, the solver will also automatically declare a
tester with rank δ Bool. The tester’s name is an indexed identifier
(see Section 3.3) of the form (_ is c).
假设我在 z3 中创建了一个数据类型 A:
(declare-datatypes () ((A (b (bx Int)) (c (cx Int)))))
现在，我可以声明一个变量 t，然后断言 t 是一个 c 类型：
(declare-fun t () A)
(assert (exists ((x Int)) (= t (c x))))
但是，这需要存在量词。我的问题是：是否可以 不使用 量词？
具体来说，我想要一个表达式，例如 is_c t 之类的，它相当于 (exists ((x Int)) (= t (c x))).
我原以为这会很简单，因为在大多数具有求和类型的函数式编程语言中，它们都有一个消除形式，通常是模式匹配，例如 match t of b x => false; c x => true。但我无法在 z3 文档中找到任何此类性质的内容。有什么我想念的吗？
您会自动获得一个测试器，作为索引标识符：(_ is c) 每个构造函数 c。
参见 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.2.3 节。相关部分在第61页（第二段）：
On successfully executing this command, for each constructor c in a declared datatype δ, the solver will also automatically declare a tester with rank δ Bool. The tester’s name is an indexed identifier (see Section 3.3) of the form (_ is c).