程序员经验分享-hwhale

  • 有没有办法获取Z3中的默认上下文？

    我正在使用 z3py API 4 3 0 我可以轻松翻译一个表达expr从默认上下文到新上下文target ctx using expr translate target ctx 但是我如何从给定的上下文中进行翻译ctx进入默认的 Z3 上
    z3 z3py

  • 如何使用 z3py 进行增量求解

    我正在使用 Z3 求解器的 python API 来搜索优化的时间表 它工作得很好 除了有时即使对于小图也非常慢 但有时非常快 原因可能是我的调度问题的约束相当复杂 我试图加快速度 并偶然发现了一些关于增量解决方案的文章 据我了解 您可以使
    z3 SMT z3py

  • 哪里可以找到 z3py 教程

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

  • 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必须是一个完美的正方形 我不明白为什
    z3

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

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

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

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

  • Z3 上下文序列化/反序列化？

    是否可以序列化 反序列化 Z3 上下文 来自 C 如果没有 这个功能有计划吗 我认为这个功能对于现实世界的应用程序很重要 当前 API 不直接支持此功能 下一版本将支持多个求解器 我们将提供用于将断言从一个求解器复制到另一个求解器并检索断言
    z3

  • 如何在线使用Z3Py解决运算放大器的问题

    求下列电路中R的值 使用以下代码可以解决此问题 R V1 V2 Vo Reals R V1 V2 Vo I1 V1 R 50 I2 V2 R 10 g R I1 I2 print g equations Vo g print equatio
    z3

  • 通过 Z3 C++ API 使用浮点运算

    我正在尝试使用 Z3 解决非线性实数问题 我需要 Z3 来生成多个解决方案 在问题域中 精度并不是关键问题 我只需要小数点后一位或两位小数 因此 我需要设置 Z3 不探索实数的所有搜索空间 以最大限度地减少找到多个解决方案的时间 我正在尝试
    c floatingpoint z3

  • 从 z3 模型中仅提取一个值

    我正在寻找相当于 z3 源 API获取价值 例如 当我有以下查询时 我可以轻松指定我想要查看哪些值 declare const s1 String declare const s2 String assert 8 str len s1 as
    string z3

  • z3在处理非线性实数运算时能否始终给出结果

    我有一个问题需要解决一组非线性多项式约束 在处理非线性实数算术时 z3 能否始终给出结果 sat 或 unsat 结果也还好吗 是的 假设 1 资源可用 并且 2 您仅使用实际约束 以便nlsat使用了策略 正如我上次检查的那样 它没有与其
    z3

  • 使用布尔运算符在 Z3 中定义约束

    比方说 我想使用 Z3 约束将字符串的每个字符限制为字符集 a zA Z0 9 我可以使用布尔运算符来指定吗 举个例子 input BitVec input s i 8 for i in range 10 for i in range 10
    python z3 z3py

  • 从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 z3py

  • 避免 Z3 中的量词

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

  • 关于 Z3 for Java 的性能问题

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

  • Z3中的parthood定义

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

  • 确定任意命题公式中变量的上/下界[关闭]

    Closed 这个问题不符合堆栈溢出指南 help closed questions 目前不接受答案 给定一个任意命题公式 PHI 某些变量的线性约束 确定每个变量的 近似 上限和下限的最佳方法是什么 有些变量可能是无界的 在这种情况下 算
    z3 satsolvers

  • 使用 C++ API 进行数组选择和存储

    我正在使用 z3 v 4 1 我正在使用 C API 并尝试在上下文中添加一些数组约束 我在 C API 中没有看到选择和排序函数 我尝试混合使用 C 和 C API 在示例中array example1 如果我将上下文变量从Z3 Cont
    c z3

  • 增量求解有什么好处？

    如果 pop 完全破坏了上下文 即学到的引理 增量约束求解使用 堆栈 的目的是什么 模式 理由 我想如果我只有 1 个约束 几个 合词 最好进行单个查询 而不是 将单独帧中的合取词堆叠到堆栈上 如果我 有超过 1 个约束并决定使用增量求解
    z3

  • 为什么已经弹出的范围会影响后续范围中的 check-sat 时间？

    一般问题 我已经注意到好几次了push pop已经弹出的范围似乎会影响check sat在后续范围的需要 也就是说 假设一个程序具有多个 可能任意嵌套 push pop 作用域 每个作用域都包含一个 check sat 命令 此外 假设第二
    scope z3 SAT