Z3的旧版本与新版本
我有一个实例，旧版本的Z3(2.18版)可以非常高效地解决这个问题。它会在几秒钟内返回SAT。 然而，当我在当前版本的Z3(版本4.3.1)上试用它时。10分钟后不返回任何结果。 这里是关于这个实验的一些细节。有谁能给点建议吗？ 共有4000个Bool变量和200个Int变量 所有约束都在命题逻辑中，并在整数之间进行比较，如a<；b 平台：Open SuSE Linux
..
smt相关内容
Z3py SMT编码跟随变量及公式
我对Z3和SMT解算器真的很陌生。 我有以下问题，我不知道如何在Z3py中编码。 在上图中，N是节点集，因此N={Node1，Node2，Node3，Node4，Node5，Node6，Node7} i是输入集合，i={i1，i2，i3，i4} O是输出集合，O={O1，O2，O3} G是这样一个组，其中对于任何连续的2个输出(O i、O j)，如果Oi是第一个生成的输出，并且
..
Z3求解器中MAxSMT与用户自定义代价函数的结合
我正在使用Z3来优化具有一些软约束的成本函数(具有加权的MaxSMT)。我很好奇MaxSMT和用户定义的成本函数是如何交互的。求解器是否同时最小化MaxSMT成本和目标函数，是否有优先机制？我找不到任何有关这方面的文档，如果遗漏了什么，请告诉我。 推荐答案 @alias从技术角度回答了这个问题；我从可用性角度解释了这个问题，所以我添加了一个带有一些细节的答案。 如@alias所述
..
Z3整流2bv运行
我遇到了一些有关位向量操作的问题。特别是，在给定以下模型的情况下。我原以为var0应该是11。 (declare-const var1 Int) (declare-const var0 Int) (assert (= var1 10)) (assert (= var0 ((_ bv2int 32) (bvor ((_ int2bv 32) var1) ((_ int2bv 32) 1))))
..
用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) -> Bool # p is unspecified predicate def q = (a:A,
..
如何使用Z3解算器解决柯克曼的女学生问题？
我是SMT问题的新手，并尝试使用Dennis Yurichev编写的一个例子来复制如何在SAT/SMT中使用Z3/MK85解决Kirkman的女学生问题。但当我试图获得模型(我使用的是Z3)时： m["%d_%d" % (person , day)] Python有一些错误： 回溯(最近一次调用)： 文件“”，第1行， 文件“D：3z3-master z3-maste
..
哪些统计数据表明 Z3 有效运行?
SMTLib2 指令 (get-info all-statistics) 显示多个数字，例如 编号.冲突:4数量传播:0(二进制:0)数量质量.安装:23 为了测试不同的公理化和编码，我想知道哪些数字适合声明一个 Z3 运行比另一个更好/更有效. 从名字猜测我会说num.质量.inst - 量词实例化的数量 - 是一个很好的指标(越低 = 越好)，但其他的呢? 解决方案 量词实例
..
从 z3 模型读取 z3 数组的 func interp
假设我在一个公式中有 2 个数组，我想使用 z3 检查其可满足性.如果 z3 返回 sat，我想读取 z3 模型中的第一个数组并将其打印为键、值对和默认值.后来我想把它转换成地图，并对其做进一步的分析.这是我运行的示例: void find_model_example_arr() {std::cout
..
Z3:使用 C API 寻找所有可能的解决方案
我是 Z3 求解器的新手，使用 Windows 10，VS2013 命令提示符. 我正在尝试使用 C，并且尝试使用 Z3 求解器解决以下问题. 问题集:满足的a、b、c的可能组合是什么?a + 2*b + 3*c = 7? 所以我根据Z3的C代码示例编写了以下C代码: void 示例(){Z3_context ctx = mk_context();Z3_solver s = m
..
(check-sat) 然后 (check-sat-using qfnra-nlsat)
我想做什么:我想调用(check-sat)，然后如果结果是unknown，调用(check-sat-using qfnra-nlsat). 我为什么要这样做?:对于我的应用程序，使用 (check-sat) 应用的 Z3 默认策略优于我使用 (check-sat-using).但是，在某些情况下，(check-sat) 返回 unknown，但 (check-sat-using ...) 会
..
Z3 Java API - 获得 unsat 核心
我想弄清楚如何使用 Z3 的 Java API 获取 unsat 核心.我们的场景如下(代码在下面，在rise4fun中有效): 我们以编程方式创建 SMT2 输入 输入包含函数定义、数据类型声明和断言 我们使用 parseSMTLIB2String API 解析它 我们确保上下文和求解器具有 unsat_core -> true Z3 为提供的输入返回 UNSAT，这是正确的 不
..
获取一个Z3模型名对应的python变量名
有没有办法得到一个z3模型名对应的python变量名? 假设我有以下代码: from z3 import *s = 求解器()a = [Real('a_%s' % k) for k in range(10)]对于范围内的我(10):s.add(a[i] > 10)s.check()m = s.model()对于 m 中的 d:打印(d，m[d]) 这里m中的d是a_0,a_1,a_2,.
..
将循环语义转换为 SMT-LIB
是否有将命令式语言(例如 C 或 Java)中的 for 循环语义转换为 SMT-LIB 的标准方法?我正在考虑将它们定义为 SMT-LIB 公理，但它似乎是临时的，而且我知道解算器并不总是可以确定翻译，比如 z3. 解决方案 经典的“技巧"是在边界内展开循环.这个想法源于硬件社区，在那里有界证明更为常见.但它也适用于软件.CBMC (https://www.cprover.org/cbm
..
是否可以证明这个定义的函数是 z3 的对合?
我试图了解如何定义断言，以证明已定义函数的某些数学特性.如 this post SMT 求解器不太适合用于证明数学质量的归纳法. 在我的例子中，我有一个 identity function f(x) = x 的递归函数定义(只是一个简单的例子): (define-fun-rec identity-rec((l String)) String(ite (= 0 (str.len l))“"(
..
使用 MAXSMT 进行增量学习
我们能否在 z3 中以增量方式使用 MaxSMT 求解器(优化)的先前解决方案?另外，有没有办法打印出优化器上的软断言? 解决方案 如果您问技术上是否可以运行任一，答案是YESz3 或 OptiMathSAT 增量 与 MaxSMT 问题.(使用 API). 具有相同id 的所有软子句--在执行check-sat--的那一刻被认为是一部分相同的 MaxSMT 目标.本质上，OMT 求
..
获取 SMT 公式的较小模型
假设我有一些可以设置的公式，但我想获得更小(或更大)的可能值，因此请设置该公式. 有没有办法告诉 SMT 求解器给出那种小的解决方案? 示例: a+1>10 在那个例子中，我希望 SMT 求解器给我解决方案 10 而不是 100. 干杯 注意:我刚刚看到一个类似的问题z3 作者说，三年前，他们正在 z3 中实现该功能.你知道它是否已经实施了吗? 解决方案
..
SMT:检查功能的唯一性和整体性
Give 是一个函数及其行为的描述: add: (ℤ ∪ {Error, None})² → (ℤ ∪ {Error, None})对于 x ∈ (ℤ ∪ {Error, None}):添加(x，无)=添加(无，x)=无对于 x ∈ (ℤ ∪ {Error}):添加(x，错误)=添加(错误，x)=错误对于 x, y ∈ ℤ:添加(x，y)= x + y 如何将此描述转换为 SMT(我使用的是
..
QF_NRA 中是否包含除以零?
QF_NRA 中是否包含除以零? SMT-LIB 标准在这方面令人困惑.定义标准的论文根本没有讨论这一点，事实上 NRA和 QF_NRA 没有出现在该文档的任何地方.标准网站上提供了一些信息.实数定义为包括: - 形式为 (/m n) 或 (/(- m) n) 的所有术语，其中- m 是 0 以外的数字，- n 是 0 和 1 以外的数字，- 作为整数，m 和 n 除了 1 没有公因数.
..
位向量策略导致 Z3Py 中的退出代码 139
这是一个简单的位向量问题: 导入z3s = z3.Tactic('bv').solver()m = z3.Function('m', z3.BitVecSort(32), z3.BitVecSort(32))a, b = z3.BitVecs('a b', 32)公理 = [a == m(12432),z3.Not(a == b)]s.add(公理)打印(s.check()) Python 崩
..
将一阶微分方程编码为一阶公式
有人可以帮助我指出使用一阶公式对以下方程进行最佳编码，以便将其作为 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_
..