程序员经验分享-hwhale

  • z3 处理非线性实数运算的局限性

    我有一个程序可以生成非线性实数算术中的一组约束 考虑以下两个约束 gt v0 x v2 x v1 y v2 y v3 x v2 x v3 x v2 x v3 y v2 y v3 y v2 y v0 y v2 y v3 x v2 x v1 x
    z3

  • Z3 结果的随机性

    我正在使用 Z3 Python 接口作为我正在编写的研究工具的一部分 当我在同一查询上重复运行 Z3 求解器时 我注意到一些非常奇怪的行为 特别是 我似乎每次都不会得到相同的结果 即使我在运行之前明确重置了求解器 作为参考 这是我的代码 i
    python z3

  • 哪些统计数据表明 Z3 运行高效？

    SMTLib2 指令 get info all statistics 显示多个数字 例如 num conflicts 4 num propagations 0 binary 0 num qa inst 23 为了测试不同的公理化和编码 我想
    encoding statistics solver SMT z3

  • 使用 Z3 命令行工具和超时查找次优解决方案（迄今为止最佳解决方案）

    I saw a post其中谈到了如何使用 Z3 的 python API 来获得最小化问题的次优解决方案 我有一个 MAXSMT 问题 我想知道如何使用 Z3 命令行工具在指定超时时找到次优解决方案 正在使用 t timeout单独的选项
    z3 SMT

  • 如何让 Z3 返回最小模型？

    如果我给 Z3 一个像 p 这样的公式q 我希望 Z3 返回 p true q dont care 或者 p 和 q 切换 但它似乎坚持为 p 和 q 赋值 即使我没有完成转换 通话时亮起Eval 除了对此感到惊讶之外 我的问题是如果 p
    z3

  • Z3 中断言的顺序有何重要性？

    我有两个文件 除了放置断言的顺序之外 其内容相同 在一个文件中 断言的放置顺序与另一个文件的顺序相反 第一个文件 po 9 z3 在不到一秒的时间内被 Z3 声明为不可满足 而另一个文件 po z3 在一分钟内无法验证 造成这种差异的原因是
    z3

  • 量词中的非零向量

    我想验证以下形式的公式 Exists p ForAll x 0 f x p gt 0 一个实现 不起作用 如下 def f0 x0 x1 x y return x1 2 y x0 2 x s Solver x0 x1 Reals x0 x1
    z3 solver z3py

  • 如何解释统计数据 Z3

    我在 Z3 中得到以下统计数据 added eqs 24529 binary propagations 43837 bv bit2core 7115 bv conflicts 156 bv diseqs 10395 bv dynamic d
    z3 SMT

  • 是否可以克隆 Z3_context？

    我需要它在符号执行 Klee 的上下文中进行增量求解 在符号执行路径的分支点 有必要将求解器上下文分为两部分 条件为真和条件为假 当然 有一个昂贵的解决方法 创建空上下文并重播所有约束 有没有办法分割Z3 context 您打算添加这样的功
    z3

  • 如何使用 C-API 设置 z3_solver 的超时？

    我使用 Z3 solver 进行非线性实数运算 我还想为求解器设置超时 我正在使用以下代码 但看起来超时不起作用 因为求解器永远运行 谁能帮我找出问题所在 Z3 solver solver cfg Z3 mk config ctx Z3 m
    z3

  • Z3是否支持优化问题

    我在去年八月份的一篇文章中看到Z3不支持优化 但它也表示 开发人员正计划添加此类支持 我在来源中找不到任何表明发生这种情况的内容 谁能告诉我我关于没有支持的假设是否正确 或者是否已添加但我不知何故错过了它 谢谢 奥马尔 如果您的优化具有整数
    z3

  • 在 Z3 中的多个值处评估逻辑公式

    我需要使用 Z3 计算变量的各种值的表达式的值 我知道 Z3 是一个可满足性检查器 但 model Eval Args 会导致对模型生成的变量值的表达式进行评估 那么我们是否可以迭代各种值来计算表达式 示例 p 和 q 为 p 和 q 的所
    c z3

  • Z3 4.3.1 C-API parse_smtlib2_string：从哪里获取声明？

    不幸的是 我没有足够的声誉来评论其他问题的答案 所以我必须开始一个新问题 基本上我有与描述相同的问题here 我想使用 Z3 进行增量求解 为了将约束引入 Z3 我使用 smtlib2 字符串 对于第一组约束 一切正常 我可以将变量等的声明
    z3

  • 获取 QF_UFNRA 中实数的小数部分

    使用 smtlib 我想使用 QF UFNRA 进行类似模数的操作 这使我无法使用 mod to int to real 之类的东西 最后我想在以下代码中获取 z 的小数部分 set logic QF UFNRA declare fun z
    z3 SMT cvc4

  • z3Opt 使用 qfnra-nlsat 优化非线性函数

    我正在尝试使用 z3Opt 来优化真正的非线性函数 但即使对于像下面这样的简单情况 http rise4fun com Z3Opt JbaU 结果不是预期的那样 就像 z3 一样 它根本没有优化 任何人都可以帮助我理解吗 目前不支持非线性函
    z3

  • 在线使用Z3Py证明n^5 <= 5 ^n for n >= 5

    使用以下代码 n Int n s Solver s add n gt 5 s add Not n 5 lt 5 n print s print s check 我们得到以下输出 n 5 n 5 5 n unknown 也就是说 Z3Py 无
    z3

  • SMT 求解器中约束强化的效率

    解决优化问题的一种方法是使用 SMT 求解器来询问是否存在 坏 解决方案 然后逐步添加更严格的成本约束 直到命题不再可满足 例如 该方法在以下内容中进行了讨论 http www lsi upc edu oliveras espai pape
    z3 SMT

  • 编码返回“未知”

    对于这个例子 http pastebin com QyebfD1pz3 和 cvc4 返回 未知 作为 check sat 的结果 两者对于原因都不是很详细 有没有办法让 z3 关于其执行更加详细 你的脚本使用了这个策略 s Then si
    z3 cvc4

  • bv-enable-int2bv-传播选项

    set option bv enable int2bv propagation true 在线工作 但是 我的本地版本对此有所抱怨 说 错误 第 1 行第 43 列 未知参数 bv enable int2bv propagation 这是一
    z3

  • 适用于 Linux 的 Z3 的先前版本

    有谁知道我们如何获得适用于 linux 64 的 z3 的早期版本 我使用的是 Ubuntu 10 04 它不包括 z3 3 2 我当前拥有的版本 所需的 GLIBGXX 3 4 14 所以我想知道是否可以访问以前的版本 另外 如果有人知道
    z3