- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
下面的 smt2 代码给出了与类型相关的错误。
( declare-datatypes ( ( List 1 ) )
( ( par ( T ) ( ( cons ( hd T ) ( tl ( List T ) ) )
( nil )
) )
) )
(declare-sort Ty 0)
(define-fun-rec func ((x (List Ty) ) (y (List Ty))) (List Ty)
(match x ( ((cons xt xts) ( cons xt (func xts y)) )
( nil nil )
)
)
)
(error "Both branches of the ITE must be a subtype of a common type.
then branch: ((lambda ((xt Ty) (xts (List Ty))) (cons xt (func xts y))) (hd x) (tl x))
its type : (List Ty)
else branch: nil
its type : (List T)
")
(nil (as nil (List Ty)) )
这解决了错误但我不想在程序中的每个 nil 处指定返回类型。
最佳答案
这是设计使然。 SMTLib 的类型系统不是为了进行任何类型的推理而设计的,目的是让求解器轻松明确地加载规范。参见 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 3.6 节其中讨论了排序良好的要求。所以 CVC4 理所当然地拒绝了你的程序。
但是你是对的,这在实践中相当烦人。典型的解决方案是简单地在您感兴趣的类型上一劳永逸地定义所需的常量:
(define-fun nilTy () (List Ty) (as nil (List Ty)))
nil
在适当的上下文中:
(define-fun-rec func ((x (List Ty) ) (y (List Ty))) (List Ty)
(match x ( ((cons xt xts) ( cons xt (func xts y)) )
( nil nilTy)
)
)
)
nilTy
应该用在。
关于smt - smt2 中的类型不匹配,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59207529/
我想在另一个模型中使用一个模型的输出(在我的例子中只有 sat 和 unsat)。在这里,模型是对一组逻辑公式(在本例中为 Z3 表达式)中涉及的常量的令人满意的赋值。我的目标可以简要解释如下。 我的
我想在另一个模型中使用一个模型的输出(在我的例子中只有 sat 和 unsat)。在这里,模型是对一组逻辑公式(在本例中为 Z3 表达式)中涉及的常量的令人满意的赋值。我的目标可以简要解释如下。 我的
我正在尝试 a Z3 tutorial 的一些示例涉及递归函数。我已经尝试了以下示例。 Fibonacci (第 8.3 节) IsNat (第 8.3 节) Inductive (第 10.5 节)
下面的 smt2 代码给出了与类型相关的错误。 ( declare-datatypes ( ( List 1 ) ) ( ( par ( T ) ( ( cons ( hd T ) ( tl (
我有一个关于 MaxSat 的想法,并且已经使用 MSU3 以及使用 minisat API 的顺序编码实现了一个朴素的 Maxsat 求解器 我想知道是否有办法加速这个求解器。 我带来了这篇论文:
我在以下看似微不足道的基准测试中尝试了几种 SMT 求解器(CVC3、CVC4 和 Z3): (set-logic LIA) (set-info :smt-lib-version 2.0) (asse
最近,我开始研究形式验证技术。在文献中,模型检查器和求解器可以以某种方式互换使用。 但是,模型检查器和求解器如何相互连接? p.s.如果建议提供一些论文或链接,我将不胜感激。 最佳答案 为了执行模型检
我一直在研究各种 SMT 求解器,主要是 Z3、CVC4 和 VeriT。他们都对自己用量词解决 SMT 问题的能力有模糊的描述。他们的文档主要基于示例 (Z3),或由学术论文组成,描述可能会或可能不
我想构造一个 SMT 公式,其中包含对整数线性算术和 bool 变量的多个断言,以及对实数非线性算术和 bool 变量的一些断言。对整数和实数的断言仅共享 bool 变量。例如,请考虑以下公式: (d
解决优化问题的一种方法是使用 SMT 求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足。例如,http://www.lsi.upc.edu/~oliveras/es
我有一个 SMT 应用程序(基于 Haskell SBV 库构建),它针对单个 s 求解一些复杂的方程式使用 Z3 的实逻辑变量。就我而言,找到解决方案大约需要 30 秒。 为了加快速度,我添加了额外
在 previous post使用Z3Py在线解决了一些涉及运算放大器的问题。但是现在 Z3Py online 已停止服务,我正在尝试使用 Z3 SMT-LIB online 解决此类问题。 示例 1
我尝试了一段时间来完成一个相当简单的要求: 我声明了一个新的数据类型 (declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))
HT/SMT 背后的主要思想是,当一个线程停顿时,同一内核上的另一个线程可以选择该内核的其余空闲时间并透明地运行它。 In 2013 Intel dropped SMT in favor of out
我正在使用 Microsoft 的 Z3 SMT 求解器,并且我正在尝试定义自定义类型的常量。默认情况下,这些常量似乎并不不平等。假设您有以下程序: (declare-sort S 0) (decla
我正在考虑做一些验证工作,其中我有常规的树语法作为基础理论。 Z3 允许您使用未解释的函数定义自己的东西,但是当您的决策过程是递归的时,这往往不会很好地工作。他们曾经允许使用插件,但我认为这已经被贬低
是否有增量 SMT 求解器或某些增量 SMT 求解器的 API,我可以在其中增量添加约束,我可以通过某个标签/名称唯一标识每个约束? 我想唯一标识约束的原因是我以后可以通过指定该标签/名称来删除它们。
我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验,并且想知道使用哪个求解器;看着例如SMT 竞赛参赛者只选择开源系统,将范围缩小到 Beaver、Boolector、CVC3、O
我用 Haskell 编写了一个应用程序,它调用 Z3 求解器来解决一些复杂公式的约束。感谢 Haskell,我可以快速切换正在使用的数据类型。 当使用 SBV 的 AlgReal 类型进行计算时,我
我正在使用Z3的Java API。在检查“满意度”(s.status)时,我遇到了段错误。有人可以帮忙调试这个问题吗?有什么方法可以转储消息以便我可以调试这个问题。我尝试使用 Log.open(),但
我是一名优秀的程序员,十分优秀!