程序员经验分享-hwhale

QF_FPA？ Z3支持IEEE-754算法吗？

2023-11-24

浏览 Z3 源代码，我发现了一堆引用 QF_FPA 的文件，它似乎代表无量词、浮点算术。但是，我似乎无法找到有关其状态或如何通过各种前端（特别是 SMT-Lib2）使用它的任何文档。这是 IEEE-754 FP 的编码吗？如果是这样，支持哪些精度/操作？任何文档都会非常有帮助..


是的，Z3 支持浮点运算，正如 Ruemmer 和 Wahl 在最近的 SMT 研讨会上提出的那样paper。现阶段还没有官方的FPA理论，Z3的支持非常基础（只有bit-blaster）。我们还没有积极宣传这一点，但它可以完全按照 Ruemmer/Wahl 的论文中提出的方式使用（设置逻辑 QF_FPA 和 QF_FPABV）。目前，我们正在为 FPA 制定新的决策程序，但该程序的推出还需要一段时间。

以下是 FPA SMT2 公式的简要示例：

(set-logic QF_FPA)    

(declare-const x (_ FP 11 53))
(declare-const y (_ FP 11 53))
(declare-const r (_ FP 11 53))

(assert (and 
    (= x ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= y ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= r (+ roundTowardZero x y))
))

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

z3

QF_FPA？ Z3支持IEEE-754算法吗？ 的相关文章

  • 如何从 Lambda 表达式获取值？

    我正在 python 中试验 z3 我有以下模型 set option produce models true set logic QF AUFBV declare fun a Array BitVec 32 BitVec 8 declar

  • Z3：int2bv 的异常

    declare const a Int declare const b Int declare const c BitVec 32 declare const d BitVec 32 assert b bv2int c assert c i

  • 表示 SMT-LIB 中的时间约束

    我试图在 SMT LIB 中表示时间约束 以检查它们的可满足性 我正在寻找有关我所采取的方向的反馈 我对 SMT LIB 比较陌生 非常感谢您的意见 我所面临的限制是事件的时间和持续时间 例如 考虑以自然语言给出的以下约束 约翰在 13 0

  • z3 实数的存在主义理论

    Z3决定非线性实数运算的存在片段吗 也就是说 我可以用它作为决策程序来测试是否 带有 和 x 的无量词公式有实数解吗 是的 Z3有一个非线性多项式实数运算的存在片段的判定过程 当然 该过程是以可用资源为模完成的 该过程相当昂贵 本文 htt

  • SMT 中的混合理论

    我想构造一个 SMT 公式 其中包含对整数线性算术和布尔变量的多个断言 以及对实际非线性算术和布尔变量的一些断言 对整数和实数的断言仅共享布尔变量 例如 请考虑以下公式 declare fun b Bool assert b true de

  • Z3中的parthood定义

    我试图在 Z3 中定义集合对 使用数组定义 之间的部分关系 在下面的代码中称为 C 我写了 3 个断言来定义自反性 传递性和反对称性 但 Z3 返回 未知 我不明白为什么 define sort Set Array Int Bool dec

  • 关于 Z3 for Java 的性能问题

    我在当前使用 Z3 for Java 的项目中遇到了一些性能问题 基本上我当前的大多数限制都非常简单 例如 f x 2 f y lt 3 f x lt 5 我正在使用整个项目共享的静态上下文和解算器实例 public class Const

  • 避免 Z3 中的量词

    我正在尝试 Z3 其中结合了算术 量词和等式的理论 这似乎不是很有效 事实上 在可能的情况下用所有实例化的基础实例替换量词似乎更有效 考虑以下示例 其中我对函数的唯一名称公理进行了编码f需要两个参数Obj并返回解释的排序S 该公理指出 每个

  • 从Z3能得到最终的CNF公式吗？

    这是我的简单编码 我想得到包含所有这些约束的最终布尔 CNF Z3 解算器中是否有任何选项可以获得最终的布尔 CNF x Int x y Int y c1 And x gt 1 x lt 10 c2 And y gt 1 y lt 10 c

  • z3 中如何定义 Int 排序（SMT-LIB 2.0 Ints 理论）和动态声明排序？

    这是我使用 z3 执行的 SMT LIB 2 0 基准测试 set logic AUFLIA declare sort PZ 0 declare fun MS Int PZ Bool assert forall x Int exists X

  • 为什么0=0.5？

    我注意到 Z3 4 3 1 在处理 smt2 文件时出现一些奇怪的行为 If I do assert 0 0 5 就会得到满足 但是 如果我改变顺序并执行 assert 0 5 0 这是不能令人满意的 我对发生的情况的猜测是 如果第一个参数

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

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

  • 使用 Z3 SMT 解决谓词演算问题

    我想使用 Z3 来解决最自然地用原子 符号 集合 谓词和一阶逻辑表达的问题 例如 伪代码 A a1 a2 a3 A is a set B b1 b2 b3 C c1 c2 c3 def p a A b B c C gt Bool p is

  • 如何估计在 z3 for SMT 中解决 SAT 部分所花费的时间？

    我已经使用探查器 gprof statshere http www ccs neu edu jaideep example2 stats包括调用图 并试图将所花费的时间分为两类 I SAT 求解部分 包括 纯 布尔传播和 纯 布尔冲突子句检

  • 将理论插件与求解器结合使用

    最新版本Z3 http z3 codeplex com解耦了以下概念Z3 context and Z3 solver The API http research microsoft com en us um redmond projects

  • 目标没有战术支持

    我有一些代码 我想在一些策略的帮助下检查它们 因为我有很多if then else声明 我要申请elim term ite tactic 我使用了以下策略 check sat using then simplify arith lhs tr

  • 为什么 Z3 在这个简单的输入上返回“未知”？

    这是输入 set option auto config false set option mbqi false declare sort T6 declare sort T7 declare fun set23 T7 T7 Bool ass

  • Z3统计中内存使用量的单位是什么？

    z3 统计中测量内存使用情况的单位是什么 是MB还是KB 记忆到底意味着什么 是执行期间的最大内存使用量还是所有分配的总和 它是执行期间最大堆大小的近似值 并通过 cmd context cpp 中的以下函数将其添加到统计对象中 void

  • 为什么 Z3 对于很小的搜索空间来说很慢？

    我正在尝试制作一个 Z3 程序 在 Python 中 它生成执行某些任务的布尔电路 例如 添加两个 n 位数字 但性能非常糟糕 以至于对整个解决方案空间进行强力搜索将导致快一点 这是我第一次使用 Z3 所以我可能会做一些影响我性能的事情 但

  • 通过 C/C++ API 对 Z3 中的 LIA 进行量词消除

    我想使用 Z3 通过 C C API 消除线性整数算术公式中的量词 考虑一个简单的例子 Exists x x 0 我尝试这样做 context ctx ctx set ELIM QUANTIFIERS true expr x ctx int

随机推荐

  • web.config 中的 IIS 重写规则将 HTTPS 请求重定向到 HTTP

    我需要将所有 https 请求重定向到 http 例如 如果有人访问https www example com another page to http www example com another page 我的 web config

  • Spring Data JPA saveAll 不执行批量插入

    所以我使用一个简单的 JpaRepository 和保存全部 方法被调用 hibernate jdbc batch size 500 hibernate order inserts true hibernate generate stati

  • 寻找 HTTPHandler 来动态修改页面以指向 CDN

    我想做的是创建 或者可能已经存在 一个 HTTPHandler 它将过滤生成的 ASP NET HTML 以使用内容交付网络 CDN 例如 我想重写这样的引用 Portals default default css to http cdn

  • 查询 MongoDB GridFS 元数据 (Java)

    我想做的是通过查询元数据字段来获取 GridFS 文件列表 例如 我得到一个 GridFS 文件文档 如下所示 id oid 4f95475f5ef4fb269dbac954 chunkSize 262144 length 3077 md5

  • Plink 在连接时不获取 bashrc 或 bash_profile

    我试图在 Windows 上使用 plink 作为 ssh 替代方案 但我发现当 plink 连接到远程 Linux 计算机时 它不会获取 bash profile 或 bashrc 我应该创建不同的点文件吗 或者还有其他选择吗 例如 我的

  • 用 PHP 实现的 IMAP 或 POP3 服务器

    PHP 中是否有可用的 POP3 IMAP 服务器实现 我正在使用以下方式处理我的电子邮件服务sendgrid 我将使用 files db whatever 将邮件存储在我的服务器上 现在我想为我的用户提供对其邮箱的完整 POP3 或 IM

  • AudioTrack - 使用 jlayer（java mp3 解码器）的短数组到字节数组失真

    我使用 jLayer 来解码 MP3 数据 通过以下调用 SampleBuffer output SampleBuffer decoder decodeFrame frameHeader bitstream 此调用返回解码后的数据 返回一个

  • 在 Azure 上的 WebJob 中使用连接字符串

    有没有一种简单的方法可以在 Azure 上的网站和 WebJob 之间共享连接字符串 我发现的唯一方法是从控制台应用程序读取 web config 但它对我来说看起来不太好 Azure 网站和 WebJob 共享在 Azure 门户上设置的

  • 有没有办法使用 ADO.NET 来确定与任何数据提供程序一起使用的数据库中是否存在表？

    有没有办法使用 ADO NET 来确定与任何数据提供程序一起使用的数据库中是否存在表 我目前正在做这样的事情 bool DoesTableExist string tableName DbCommand command this dbCon

  • C# - 预测文件夹删除时的文件系统事件

    这更多的是一个关于实现这一点的最佳实践是什么的问题 我有一个FileSystemWatcher这应该告诉我用户对文件和文件夹的更改 子目录也会被监视 在同一目录中 我的程序有时也会发生变化 我不想要FileSystemWatcher检测有关

  • 使用多列进行熊猫滚动应用

    我正在尝试使用pandas DataFrame rolling apply 多列滚动功能 Python版本是3 7 pandas是1 0 2 import pandas as pd function to calculate def mas

  • React 触发调整大小但实际上并不调整屏幕大小

    我试图触发调整大小而不实际调整屏幕大小 因为它修复了我的滑块 window dispatchEvent new Event resize 上面的代码不起作用 有没有人有其他方法在反应中触发调整大小 必须使用 jQuery jQuery wi

  • SQL Server 2005 自动更新日期时间列 - LastUpdated

    我定义了一个表 请参阅下面的代码片段 如何添加约束或其他约束 以便在行更改时 LastUpdate 列自动更新 CREATE TABLE dbo Profiles UserName varchar 100 NOT NULL LastUpda

  • 资源文件中的图像未在 Qt 中加载

    我试图通过资源文件将图像插入到我的程序中 如下所示

  • SpriteKit 没有释放所有已用内存

    我已经在 SO 和其他网站上准备了许多 如果不是全部 关于处理 SpriteKit 和内存问题的灾难的文章 正如许多其他人所遇到的那样 我的问题是在我离开 SpriteKit 场景后 几乎没有释放在场景会话期间添加的任何内存 我尝试实施我找

  • 构建像 SongBird 这样的 XUL 应用程序

    我已经开始探索 XUL Runner 作为即将推出的应用程序的潜在工具 我可以使用命令行 xulrunner bin myapp 运行一些很好的示例 如何像 SongBird 那样将其全部编译到本机外观的应用程序中 我知道 SongBird

  • JArray.Contains 问题

    我有一个 JArray 从文件中读取 private void RemoveCatalog Catalog catalog System IO StreamReader filereader new System IO StreamRead

  • 如何删除字符？

    如何删除字符串中的特殊字符和字母 qwert1234 90 this might be my cell value 我必须将其转换为 123490 I mean I have to remove everything but keep on

  • 检测并重新启动崩溃的 .NET 应用程序

    如何检测我的 NET 应用程序已崩溃 然后重新启动它 另一种解决方案 基于这个例子 是创建一个控制应用程序的启动器 class LauncherProgram static int count 3 static void Main Laun

  • QF_FPA？ Z3支持IEEE-754算法吗？

    浏览 Z3 源代码 我发现了一堆引用 QF FPA 的文件 它似乎代表无量词 浮点算术 但是 我似乎无法找到有关其状态或如何通过各种前端 特别是 SMT Lib2 使用它的任何文档 这是 IEEE 754 FP 的编码吗 如果是这样 支持哪

热门标签