简化模型中的函数解释
在 SMT:检查函数的唯一性和完整性中，我给出了函数公理化并要求 Z3 提供模型.但是，由于解决带有量词的问题通常是不可判定的，因此 Z3 超时. 这是一个修改版本，其中“int"大小写被建模为单个值: (declare-datatypes()((ABC int error none)))(declare-fun f (ABC ABC) ABC)(assert (forall ((x AB
..
z3相关内容
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 ...) 会
..
优化乘法和除法
我设置了一些边界/约束并想解决它们，但是当我使用乘法和除法函数时，优化并不像我认为的那样. 这是我的代码: import com.microsoft.z3.*;导入 java.util.*;System.setProperty( "java.library.path", "/local/Programs/z3-4.6.0-x64-osx-10.11.6/bin/" );//设置sys_pa
..
Z3 中相同代码的不同运行时间
我用了z3的定点，发现定点的运行时间总是不一样.你遇到过同样的问题吗?为什么会这样? 解决方案 如果您从相同的状态开始获得大量的相同代码，这听起来很意外.如果您从不同的状态开始(即如果您对 Z3 进行了杂项调用无论是通过文本 API 还是编程 API，在回合之间).Z3 否则不应表现出极大的非确定性行为.非确定性行为可能由错误引起，因此如果您能进一步、更准确地描述正在执行它的场景，我们将不
..
两个 boolexpr 是否相等
给定两个 booleexpr b1,b2说 b1=x1>=4&&x2>=5b2=x2>=5&&x1>=4 我们可以使用 Z3 的 .net API 来知道 b1 和 b2 是否实际上是相同的约束吗?)(意思是b1和b2允许的x1和x2的值是一样的) 解决方案 是的.你想证明 b1 等于 b2，你可以证明 b1 == b2 的否定是不可满足的.这是一个示例，展示了如何在 Z3Py 中执行
..
整数除法给出不正确的结果
我尝试检查 x div y == 2 和 x/y == 2 的可满足性，但两次都得到了错误的结果.貌似Z3还不支持这些? (declare-fun x () Int)(declare-fun y() Int)(断言(=(div x y)2))(检查周六)(获取模型)(出口)坐(模型(define-fun y() int0)(define-fun x() int38))(declare-fun x
..
如何用Z3-SMT-LIB证明Z3群满足结合律
我正在尝试使用以下 Z3-SMT-LIB 代码证明 Z3 群满足结合律 (设置选项:mbqi true)(声明排序 S)(declare-fun f(S S) S)(declare-const a S)(声明-const b S)(declare-const c S)(断言(forall((x S)(y S))(= (f x y) (f y x))))(断言(forall ((x S)))(=
..
Z3 中的程序附件
我正在使用 z3py 我有一个关于需要使用自定义算法评估的两个整数的谓词.我一直在努力实现它，但没有取得多大成功.显然，我需要的是一个程序附件，现在已弃用.有人能告诉我如何在 z3py 中实现这个吗?我知道它涉及使用 Tactics，但恐怕我还没有弄清楚如何使用它们.我也不介意使用已弃用的方式，只要它有效. 解决方案 没有程序附件策略.所有战术都在Z3内部实施；你可以从外面制定战术.以前版
..
如何使用 Z3 SMT-LIB 证明 D3 群的定理
D3 组的产品表是: 使用以下 Z3 SMT-LIB 代码可以获得一个表示: (设置选项:mbqi true)(声明排序 S)(declare-fun f(S S) S)(declare-fun g (S) S)(declare-const E S)(声明-const R1 S)(声明-const R2 S)(声明-const R3 S)(声明-const R4 S)(声明-const R
..
Z3 Java API - 获得 unsat 核心
我想弄清楚如何使用 Z3 的 Java API 获取 unsat 核心.我们的场景如下(代码在下面，在rise4fun中有效): 我们以编程方式创建 SMT2 输入 输入包含函数定义、数据类型声明和断言 我们使用 parseSMTLIB2String API 解析它 我们确保上下文和求解器具有 unsat_core -> true Z3 为提供的输入返回 UNSAT，这是正确的 不
..
带前提的非线性实数算法的可解性
一个小例子表明，当 NRA 断言由与 (sat p1 ... pn) 检查相关的前提 pi 标记时，非线性实数算术 (NRA) 求解器会受到阻碍. 以下 SMT2 示例返回具有正确模型的 SAT: (declare-const p1 Bool)(declare-const p2 Bool)(declare-const p3 Bool)(declare-const p4 Bool)(decl
..
Z3分段错误
我编写了以下 Perl 脚本来生成 smt2 格式的逻辑约束，以解决给定输入文件的数独难题.输入文件格式如下: 5 3 * * 7 * * * *6 * * 1 9 5 * * ** 9 8 * * * * 6 *8 * * * 6 * * * 34 * * 8 * 3 * * 17 * * * 2 * * * 6* 6 * * * * 2 8 ** * * 4 1 9 * * 5* * * *
..
Z3 是否支持量化公式中的仅变量模式?
我想使用仅变量模式来获得使用量化公理编码的某些理论的决策程序.更准确地说，我想强制这些公理中的某些变量使用相应类型的所有项进行实例化.这些变量仅出现在谓词符号下方，因此不会有创建匹配循环的危险. 例如，考虑以下部分查询: (声明排序 Loc 0)(声明排序映射 2)(declare-fun read ((Map Loc Loc) Loc) Loc)(declare-fun Btwn ((M
..
如何从 z3py 中的 Z3 Solver 对象中获取现有约束?
例如，我想将现有的约束从 s 获取到 Optimize 对象中. from z3 import *a = Int('a')x = Int('x')b = Array('I', IntSort(), IntSort())s = 求解器()s.add(a >= 0)s.add(x == 0)s.add(选择(b, 0) == 10)s.add(Select(b, x) >= a)选择 = 优化()o
..
获取一个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,.
..
关闭 Z3py 打印截断
我需要打印整个 Z3 问题来调试它，但是当我打印它时，输出被截断了. from z3 import *s = 求解器()... 添加许多断言到 s ...印刷) 如何显示所有内容? 解决方案 尝试: set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000) 您可
..
使用文本文件输入 Z3 模型
我正在通过其 .Net Api 使用 Z3.我构建了具有大量约束的模型.到目前为止，我一直在使用相应的 Z3 命令(在 .Net Api 中)逐行构建我的模型.但是现在模型的大小增加了，创建模型所花费的时间非常可观.我在想有没有办法将模型构建为文本文件并将完成的模型一次性输入到 Z3 求解器中? 解决方案 您的问题相当神秘，但所有 SMT 求解器都支持所谓的 SMTLib2 输入格式:ht
..
z3py 在尝试消除量词时死了
我有一个 Python 程序，可以在其中生成不同的 z3 公式，然后对其中一些公式进行存在量化.我的程序过去运行良好，但突然间它开始尝试对某些表达式进行量词消除.代码不会返回并挂在这些示例上.这是出现问题的输入之一.所有变量都是整数.我尝试打印 expr 但它从不打印.在有问题的情况下，进程也不能轻易终止.我必须通过关闭终端(ubuntu)来强制它. Exists([R_1_0, R__0, R
..
Z3py，随机不同解生成
from z3 import *随机导入a = Int('a')b = Int('b')s = Tactic('qflra').solver()s.add(a > 10)set_option('smt.arith.random_initial_value', True)set_option('smt.random_seed', random.randint(0, 2 ** 8))而 s.check
..