代码之家 › 专栏 › 技术社区 › vijrox

Z3模式匹配语法

smt z3 pattern-matching syntax

vijrox · 技术社区 · 6 年前

我尝试在Z3中使用模式匹配来处理代数数据类型。我完全按照 SMTLib standard 在第27页,但是Z3给了我一个语法错误。例如,在以下程序中:

(declare-datatype Dyn ((a) (b)))
(define-fun foo ((x Dyn)) Int (
  match x (
    (a 1)
    (b 2)
  )
))
(assert (= (foo a) (1)))
(check-sat)

它给出了错误“第4行第7列:需要变量符号”。据我所知,我完全遵循指定的语法。我该怎么解决这个问题?

1 回复 | 直到 6 年前

alias 6 年前

我认为你没有做错什么!看起来这是一个应该报告的Z3错误 https://github.com/Z3Prover/z3/issues/

你有一个小问题 assert 声明就在前面 (check-sat) . 应该阅读:

(assert (= (foo a) 1))

也就是说,周围没有括号 1 . 但你的使用 match 命令语法正确,应报告为Z3错误。

推荐文章

suisqa · 我是新来的

2 年前

Robert Munroe · “If X!=A、B或C”的Python语法[重复]

3 年前

tomm · 谷歌表格-将两列相乘,复制第三列

3 年前

ziemsterr · 无法在SQL SELECT语句中找出此语法错误

3 年前

AndrÃ©s BolÃvar · AJAX请求未收到我想要的属性

3 年前

clarkk · 当声明向量时,(1)是什么意思?

3 年前

NMOLL · python_数据['division']中的语法无效。追加(int(拆分[3]))

3 年前

Mike C. · Bash错误[:检查文件是否存在时缺少“]”

3 年前

Aleix · 错误代码:1064。您的SQL语法有错误;在2号线的“”附近

3 年前

michael · 错误的脚本和语法问题

3 年前