程序员经验分享-hwhale

z3 中的函数声明

2024-04-09

在 z3 中是否可以声明一个以另一个函数作为参数的函数？例如，这个

(declare-fun foo ( ((Int) Bool) ) Int)

似乎不太管用。谢谢。


正如 Leonardo 提到的，SMT-Lib 确实not允许高阶函数。这不仅仅是语法限制：使用高阶函数进行推理（通常）超出了 SMT 求解器的处理能力。 （尽管在某些特殊情况下可以使用未解释的函数。）

如果您确实需要reason对于高阶函数，那么交互式定理证明器是主要的选择武器：Isabelle http://www.cl.cam.ac.uk/research/hvg/isabelle/, HOL http://hol.sourceforge.net/, Coq http://coq.inria.fr/是其中的一些例子。

但是，有时您需要高阶函数not推理它们，而不仅仅是简化编程任务。 SMT-Lib 输入语言不适合最终用户在实际情况中通常需要的高级编程。如果这是您的用例，那么我建议不要直接使用 SMT-Lib，而是使用可让您访问 Z3（或其他 SMT 求解器）的编程语言。有多种选择，具体取决于最适合您的用例的主机语言：

  • 如果你是Python用户，Z3Py http://rise4fun.com/z3py刚刚随 Z3 4.0 一起发布的就是这样的方法，
  • 如果您是 Scala 用户，请查看Scala^Z3 http://lara.epfl.ch/w/jniz3-scala-examples.
  • 如果 Haskell 是您的首选语言，请查看SBV http://hackage.haskell.org/package/sbv.

每个绑定都有自己的功能集，Z3Py 可能是最通用的，因为它直接受到 Z3 人员的支持。 （它还提供对 Z3 内部结构的访问，而其他选项则无法访问这些内部结构，至少目前是这样。）

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

z3

z3 中的函数声明 的相关文章

  • 如何在z3py中表示对数公式

    我对 z3py 很陌生 我正在尝试在 z3py 中编写以下对数表达式 log x y 我确实经常搜索堆栈溢出并遇到类似的问题 但不幸的是我无法得到足够满意的答案 请帮我 更一般地说 我们如何使用 Z3 定义日志 我获得任何吸引力的唯一方法是

  • Z3 Solver Java API：意外行为

    通过向求解器添加条件 我想使用 solver check 检查是否存在解 因此 我创建了一个简单的示例来寻找 t1 的解决方案 我知道 t1 有一个解 即 t1 0 然而 求解器的状态不是 SATISFIABLE public static

  • 检索 Z3Py 中的值会产生意外结果

    我想找到一个表达式的最大间隔e对所有人来说都是如此x 编写这样的公式的方法应该是 Exists d ForAll x in d d e and ForAll x not in d d e 为了得到这样一个d 公式f在 Z3 中 看上面的 可

  • Z3中数组的理论：（1）模型很难理解，（2）不知道如何实现功能，（3）与序列的区别

    继发布于的问题之后Z3 Py 中的数组的表现力如何 一个例子 https stackoverflow com questions 73778513 how expressive can we be with arrays in z3py a

  • Z3 返回型号不可用

    如果可能的话 我想要对我的代码有第二意见 问题的约束条件是 a b c d e f是非零整数 s1 a b c and s2 d e f 是集合 The sum s1 i s2 j for i j 0 2必须是一个完美的正方形 我不明白为什

  • 哪里可以找到 z3py 教程

    由于某些安全问题 rise4fun z3py 将在几周内不可用 我试图找到一些学习z3py的资源但徒劳无功 请推荐一些学习z3py的资源 我使用 Z3Py 教程源创建了一个 zip 文件 它基本上是一些 HTML 页面和一堆 python

  • 在 Z3 中使用 SMT 约束时获取合法范围信息的（次）最佳方法

    这个问题与我之前的问题相关 在 Z3 中使用 SMT 约束时是否可以获得合法的范围信息 https stackoverflow com questions 53676016 is it possible to get a legit ran

  • 正确 Dafny 方法的 Z3 模型

    对于正确的方法 Z3能否找到该方法验证条件的模型 我原以为不会 但这里有一个例子 该方法是正确的 但验证发现了一个模型 这是 Dafny 1 9 7 的情况 Malte 所说的是正确的 我发现它也得到了很好的解释 Dafny 是健全的 因为

  • Z3/SMT：我什么时候应该选择推送/弹出来重置？

    我使用 Z3 来解决符号执行器产生的路径条件 该执行器以深度优先顺序探索状态空间 与 CUTE DART 或 可能 SAGE 非常相似 我们正在尝试使用 Z3 的不同方式 在一种极端情况下 我们将每个查询发送到 Z3 并在之后立即 重置 它

  • 如何将 Z3 与 C++ 结合使用

    我想将 Z3 与 C 一起使用 并且我遵循了安装指南 使用 Visual Studio 命令提示符在 Windows 上构建 Z3 https github com Z3Prover z3 building z3 on windows us

  • z3 中使用哪些技术来处理非线性整数实数问题？

    以下是 a 的 z3 统计数据problem http www ccs neu edu home jaideep example smt2在非线性整数实数片段中 我的许多问题与此类似 add rows 11062574 added eqs

  • 在 SMTLIB v2 输入中使用 :pattern 不断获得“未知”结果

    我在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题 通过以下输入 我不断得到 未知 结果 declare datatypes L L0 L1 declare fun path List L declare fun checkTr

  • Z3 的参考资料 - 它是如何工作的[内部理论]？

    我有兴趣阅读 Z3 背后的内部理论 具体来说 我想了解 Z3 SMT 求解器的工作原理 以及它如何找到不正确模型的反例 我希望能够手动计算出一些非常简单的示例的跟踪 然而 所有 Z3 参考文献似乎都是如何在其中编码 或对其算法的非常高级的描

  • 有人尝试过用Z3本身来证明Z3吗？

    有没有人尝试证明Z3 http research microsoft com en us um redmond projects z3 与Z3本身 是否有可能使用 Z3 来证明 Z3 是正确的 更理论化的是 是否有可能使用 X 本身来证明工

  • 如何从 Z3 中的 Seq 类型中提取元素作为基本类型？

    如何将序列中的元素提取到基本类型 以便以下内容正常工作 define sort ISeq Seq Int define const x ISeq seq unit 5 define const y ISeq seq unit 6 asser

  • 在 Z3 中证明归纳事实

    我试图在 Microsoft 的 SMT 求解器 Z3 中证明一个归纳事实 我知道 Z3 一般不提供此功能 如Z3 guide http rise4fun com z3 tutorial guide 第 8 节 数据类型 但是当我们限制要证

  • Z3 求解器中 MAxSMT 和用户定义成本函数的组合

    我正在使用 Z3 来优化带有一些软约束 带有加权 MaxSMT 的成本函数 我很好奇 MaxSMT 和用户定义的成本函数如何交互 求解器是否最小化 MaxSMT 成本和目标函数两者 是否有优先级机制 我找不到这方面的任何文档 如果我遗漏了什

  • (Z3Py) 声明函数

    我想在简单的 result x t c 公式中找到一些给定结果 x 对的 c 和 t 系数 from z3 import x Int x c Int c t Int t s Solver f Function f IntSort IntSo

  • Z3 C API 在运行时更改超时

    是否可以使用 C API 在运行时更改求解器的超时值 为了设置超时 可以执行以下操作 Z3 config cfg Z3 mk config Z3 set param value cfg SOFT TIMEOUT 10000 set time

  • 如何解决 Z3 中的最小化约束？

    谁能告诉我如何通过 Z3py 实现最小化整数问题 如下所示 我如何定义所有语句 这里所有的变量都是int排序的 Z3中有没有专门的求解器可以解决此类问题 如果有的话 我该如何设置该解算器的配置 Thanks 以下是一些相关 类似的问题和答案

随机推荐

  • MySQL 通过在非索引列上执行删除语句时锁定整个表来尝试防止什么现象

    使用可重复读的 MySQL 隔离级别 给定表test具有非索引列quantity id quantity 1 10 2 20 3 30 Tx1执行第一个 注意它还没有提交 这意味着所有获取的锁还没有释放 Tx1 START TRANSACT

  • 如何使用PHP获取用户的屏幕分辨率[重复]

    这个问题在这里已经有答案了 可能的重复 使用PHP获取屏幕分辨率 https stackoverflow com questions 1504459 getting the screen resolution using php 这个问题是

  • 通过 JS 调用 JSF 方法 [重复]

    这个问题在这里已经有答案了 我在 JS 代码中有一个 for 循环 我想调用一个方法 该方法的参数写在 JAVA 托管 bean 中 该方法计算一个值并返回一个将在 JS 中使用的新值 注意 我在 xhtml 页面中使用 primeface

  • QML ListView 如何估计其 contentItem 的高度/宽度

    我想知道如何ListView估计它的高度 宽度contentItem 尽管代表是Component您无法询问 并且不同委托实例的大小可能有所不同 它不使用当前实例的平均大小 否则在实施例1 如果按下一个元素 则估计大小将为3055 5如果计

  • FreeBSD 中的多行删除

    我们怎样才能在 FreeBSD 中实现这一点呢 FreeBSD 中包含模式的多行删除块 sed START TAG a N END TAG ba ID 222 d data txt See sed 多行删除与模式 https stackov

  • 汉明立方体顶点上的查询点

    我有 N 个点 仅位于 D 维立方体的顶点上 其中 D 约为 3 A vertex may not contain any point So every point has coordinates in 0 1 D I am only in

  • React-Bootstrap 切换按钮无法隐藏单选按钮圆圈

    在我的表单中 我想要切换按钮 以下代码是从切换按钮上的 React bootstrap 文档复制的 但是 单选按钮圆圈在应该隐藏的时候却显示了 我该如何隐藏它们 import ButtonGroup from react bootstrap

  • Kubernetes RBAC 动词：不带列表获取，反之亦然？没有列表就看？

    虽然有很多关于 Kubernetes RBAC 的文档和示例 以及不同资源的可用动词 但我找不到任何关于某些动词是否始终组合使用或是否有单独使用它们的用例的规则 我特别想知道动词 get list 和 watch 组合它们 尤其是不组合它们

  • 在 SQL 中添加额外的 Where 子句会严重影响性能

    我有一个运行多个视图和表的 SQL 查询 查询运行良好 但当我在 WHERE 子句中添加另一个条件时 它开始对性能产生巨大影响 查询的结构类似于 SELECT a FROM vw myView a LEFT OUTER JOIN tbl1

  • 从 API 返回字符串文字

    我正在编写一个用户 API 这样返回 const char 值是否正确 const char returnErrorString int errorCode switch errorCode return This error code m

  • 为什么不能使用整数作为 C# 中 while 循环的条件？ [关闭]

    Closed 这个问题需要调试细节 help minimal reproducible example 目前不接受答案 使用如下所示的 while 循环时出现错误 我不明白为什么 int count 5 while count here s

  • 如何在 Mysql 5.7 中更新 JSON 数组中的特定对象

    如何根据对象中的唯一值更新数组中的对象 假设这是我的 json 对象 存储在名为对象的表和名为内容的列中 table objects id 7383 content data id 111 active 1 id 222 active 1

  • 视图中嵌套的 ForEach（和列表）会产生意想不到的结果

    在 SwiftUI 视图中的另一个 ForEach 中执行一个 ForEach 会产生意想不到的结果 几乎就像它们踩在彼此的计数器上一样 不清楚发生了什么 我需要显示多分支数组并尝试了多种变体 但仍然遇到同样的问题 我有几个项目就出现过这种

  • 从 dict 列表中删除一个项目并分割 stdout_lines

    我试图从字典列表中删除一个项目 即 未找到结果 的项目 validar LPARNAME No results were found LPARNAME server1 server2 server4 LPARNAME server3

  • AutoHotkey-GDIp：从硬件加速窗口捕获屏幕截图

    我目前正在编写一个小脚本 该脚本可以从 BlueStacks 中的硬件加速窗口捕获屏幕截图 问题是 看起来窗口必须是硬件加速的 因此屏幕捕获保存了一个黑色方块 我使用 AutoHotkey 编写脚本 并添加了 GDIp 库来访问 GDI 我

  • 将每个Python字典值除以总值

    我有a foo 2 bar 3 baz 5 无论如何我能得到吗a foo 0 2 bar 0 3 baz 0 5 在一行 需要将每个值除以总价值 我只是无法完成它 太感谢了 对值求和 然后使用字典理解生成具有标准化值的新字典 total s

  • 如何在 python 中禁用 lambda 的默认日志消息

    我有一个用 python 编写的 AWS Lambda 函数 我只需要在 CloudWatch Logs 中记录的消息 我已经尝试了watchtower中给出的例子 但它仍然不起作用 START RequestId d0ba05dc 850

  • 如何使用特定日期的 Sitecore 项目进行 Lucene 搜索？

    我的内容项目是 Sitecore 其日期字段名为 EventDate 我想使用 Lucene Net 搜索具有特定日期的项目 下面是我尝试过的代码 但没有得到结果 var index SearchManager GetIndex event

  • JNLP应该使用特定的Java版本但错误结果

    我在这里面临一个问题 我想使用一个特殊版本来运行我们的 java webstart 应用程序 但仅用于一个 jnlp 经过测试 blabla 我们不能使用新版本 blabla 随机的风袋 所以我尝试像这样配置我们的 JNLP

  • z3 中的函数声明

    在 z3 中是否可以声明一个以另一个函数作为参数的函数 例如 这个 declare fun foo Int Bool Int 似乎不太管用 谢谢 正如 Leonardo 提到的 SMT Lib 确实not允许高阶函数 这不仅仅是语法限制 使

热门标签