将一阶微分方程编码为一阶公式
有人可以帮助我指出使用一阶公式对以下方程进行最佳编码，以便将其作为 SMT 求解器的输入吗?? x`=Ax+b 解决方案 您可以在 Z3 中轻松地对微分方程进行编码，因为它只是 n^2 + n 个实常数 (n^2 来自 a_ij，n 来自 b_i) 和 n 个实变量 (x_i).您可以直接在 Z3 中对其进行编码. dotx_1 = a_11 * x_1 + a_12 * x_2 + a_
..
z3相关内容
奇怪的Z3模型值
我使用的是最新的 Z3 3.2 版.我从“get-value"命令中得到了意外的响应.这是我在 SMT-LIB2 兼容模式下运行的小脚本: (set-option :produce-models true)(declare-datatypes () ((Object o0 null)))(声明有趣的 IF (Object) Int)(declare-fun i2() Int)(断言(=(IF o
..
等效量词免费公式
我想知道Z3是否可以在量词消除后显示等效公式. 示例(存在 k)(i x k) = 1 且 k > 5相当于 i > 0 和 5 i - 1 这里，量词 k 已被删除. 这可能吗? 谢谢，考斯图布. 解决方案 是的，Z3 可以检查两个公式是否等价.检查 p 和 q 是否等价.我们必须检查 (not (iff p q)) 是否不可满足. 您的示例使用非线性算术
..
我如何知道z3中有多少个数组?
我正在使用 Z3py 但是当我定义一个数组时 array = Array('array', IntSort(), IntSort()) 我不知道如何知道数组有多少个值. 解决方案 Z3(和 SMT)中的数组具有无限大小.例如，参见 创建一个固定大小的数组并初始化它
..
Python 和 Z3:整数和浮点数，如何以正确的方式管理它们?
需要 Z3 和 Python 方面的帮助...看起来我太笨了.我的代码: from z3 import *num1 = Int('num1')num2 = Int('num2')num3 = Int('num3')s = 求解器()s.add( 2 * num1 - num2 + 0.5 * num3 == 5412.0)s.add( 2 * num1 + 3 * num2 + 4 * num3
..
是否有任何函数可用于计算 Z3/cvc4 中以 2 为底的对数?
我想证明一个简化，它涉及计算以 2 为底的对数.z3/cvc4 中是否有任何函数可用于计算它? 解决方案 简而言之，这两种工具都无法直接支持整数.对于无界整数，存在通过固定常数对 Presburger 取幂的决策程序.由此您可以构造对数函数(反之亦然).我不是专家，但我的理解是这些非常复杂.欲了解更多信息: http://www.logique.jussieu.fr/~point/p
..
Z3+布吉安装
我很难从 codeplex 将 Boogie 和 Z3 安装在 Windows 7 和 Z3 版本 4.3.2 上.我试图通过 register.cmd 命令在提示符下像 spec# 一样安装它，但它不起作用.谁能告诉我怎么做? 解决方案 Boogie 不支持 Z3 4.3 版.您需要 4.1 版(请参阅 boogie.codeplex.com 上的安装页面，我刚刚更新了该页面).
..
Z3 C API 管理 Z3_VAR_AST
我尝试在 C 中为 Z3 的 Z3_ast 编写自定义打印，但我不知道如何管理 Z3_VAR_AST 的 Z3_ast_kind 和 Z3_FUNC_DECL_AST，我只知道如何打印 Z3_VAR_AST 的 Z3_sort (Z3_get_sort)，关于这个变量价值我没有想法???.关于Z3_FUNC_DECL_AST，我找不到任何可以获取函数名称、参数数量和参数的访问器.你们能帮帮我吗?干
..
Z3 java中的替换
注意到在z3中调用替换时，总是简化表达式，但是在我们的项目中，只需要替换并保持原来的结构即可.根据下面的帖子，这个功能将被修复，不知道它是否已经存在?或者是否有任何方法可以关闭简化? Z3Py 中的替代 解决方案 是的，这个问题已经在unstable分支中修复了(见这里);这现在应该完全符合预期.
..
如何在 Z3_mk_forall_const 中声明常量以用作绑定变量?
假设我想在以下公式中对 x 和 y 进行普遍量化: f(x,y) x=y 使用 Z3_mk_forall_const .我必须首先构造上面的公式，它需要 Z3_ast 类型的常量 x 和 y.使用 Z3_mk_const 创建 x 和 y 会导致全局声明.理想情况下，我想避免这种情况.有没有替代品? 解决方案 是的，有一个替代方案；您可以使用 Z3_mk_forall 使用 de-Br
..
z3 中的叉积
z3 是否提供两个列表的叉积功能?如果不是，是否可以在不使用高阶函数或使用提供的列表函数的情况下定义一个?我一直在尝试定义一个问题.我知道如何使用 map 定义一个，但我认为 z3 不支持. 解决方案 您可以在 SMT 2.0 中声明叉积函数.然而，任何非平凡的财产都需要归纳证明.Z3 目前不支持归纳证明.因此，它只能证明非常简单的事实.顺便说一句，通过列表的交叉乘积，我假设您想要一个函数
..
代数实数:漂亮打印时 z3 是否进行四舍五入?
如果我发出: (set-option :pp-decimal true)(设置选项:pp-十进制精度10) Z3 是否在实数的第 10 位后进行四舍五入?或者它只是将剩余的数字切掉而不进行任何四舍五入? 解决方案 在 Z3 4.0 中，代数数 alpha 使用单变量多项式 p 和两个二进制有理数表示: lower 和 upper.二进制有理数是 a/2^k 形式的有理数，其中 a 是整
..
使用分辨率定理证明 Z3
我是 Z3 的新手，但之前有一些使用 Prolog 的经验. 我已经设法解决了以下“难题"，即使用 Prolog 证明该女孩是女巫，但我不知道如何在 Z3(在 C++ 或 Python 中)实现它:https://www.netfunny.com/rhf/jokes/90q4/burnher.html 我是否需要为诸如此类的断言声明 Function()BURNS(x)/\ WOMAN
..
基于模型的量词实例化和分层排序片段
Z3 的文档说明了基于模型的量词实例化 (MBQI): 分层排序片段 statified sorts 片段是另一个可判定的片段排序的一阶逻辑公式.它对应于以下公式，当以 prenex 范式编写时，有一个函数级别来自排序到自然，并为每个功能 (declare-fun f (S_1 ... S_n) R) 等级(R)＜级别(S_i). Z3 是否支持任何 prenex 范
..
使用 check() 检查 sat 并假设上升 AttributeError: 'bool' object has no attribute 'as_ast'
为什么会这样: >>>从 z3 导入 *>>>s = 求解器()>>>s.add([真])>>>s.check()坐 但这不会: >>>从 z3 导入 *>>>s = 求解器()>>>s.check([真])回溯(最近一次调用最后一次):文件“"，第 1 行，在 中.文件“$HOME/.local/lib/python3.6/site-packages/z
..
如何在带有声明函数的 Z3 的 Python API 中正确使用 Solver() 命令
我通过使用 Z3 的 Python API 的某些脚本得到了意想不到的结果.我认为我误解了某些过程或只是错误地使用了某些命令.例如，假设我有以下脚本: from z3 import *x = Int('x')定义 g(x):如果 x == 0:返回 1elif x >0:返回 x**(x+1)s = 求解器()s.add(g(x) > x)打印 s.check()如果 s.check()== 坐
..
Z3Python 中的散列表达式
看起来 z3 表达式有一个 hash() 方法但没有 __hash__().有没有理由不使用 __hash__() ?这允许表达式是可散列的. 解决方案 没有理由不叫它__hash__().我称它为 hash() 因为我是 Python 新手.我将在下一个版本 (Z3 4.2) 中添加 __hash__(). 编辑: 正如评论中所指出的，我们还需要 __eq__ 或 __cmp__
..
目标不受战术支持
我有一些代码，我想借助一些策略进行检查.由于我有很多 if-then-else 语句，我想应用 elim-term-ite 策略. 我使用了以下策略 (check-sat-using (then (!simple :arith-lhs true) elim-term-ite solve-eqs lia2pb pb2bv bit-blast sat)) 但是，如果我的错误是 - “
..
linux/mac 上的 z3 超时
嗨 Leonardo:看起来 z3 (v3.2) 接受命令行开关“-T:10"来指定 Mac 和 Linux 上的超时，但忽略了它.(尚未在 Windows 上尝试过.)如果 linux/mac 版本也支持超时，那就太好了. 解决方案 是的，-T 开关仅适用于 Z3 3.2 中的 Windows.这将在下一个版本中修复.
..
python中z3求解器的超时
我在为求解器设置超时时遇到问题: s = Solver()编码 = parse_smt2_file("ex.smt2")s.add(编码)s.set("超时", 600)解决方案 = s.check() 但我收到以下错误 回溯(最近一次调用最后一次):文件“/Users/X/Documents/encode.py"，第 145 行，在 parse_polyedra("file")文件“/Us
..