哪些技术用于处理 z3 中的非线性整数实数问题?
以下是针对 问题 的 z3 统计数据Linear Integer Real Fragment(我的很多问题都与此类似): (:add-rows 11062574:add-eqs 34:arith-conflicts 37293:assert-lower 837747:assert-upper 1909779:二进制传播 13807730:bound-prop 32666:冲突 47631:决定
..
z3相关内容
为什么 Z3 中的运算符 '/' 和 'div' 给出不同的结果?
我试图用两个整数来表示一个实数，将它们用作实数的分子和分母.我编写了以下程序: (declare-const a Int)(declare-const b Int)(declare-const f Real)(断言(= f(/a b)))(断言(= f 0.5))(断言 (> b 2))(断言(> b a))(检查周六)(获取模型) 程序返回的SAT结果如下: sat(模型(define-f
..
可以从 Z3 得到最终的 CNF 公式吗?
这是我的简单编码.我想得到呈现所有这些约束的最终布尔 CNF.Z3求解器中是否有任何选项可以获得最终的布尔CNF? x = Int('x')y = Int('y')c1 = And(x >= 1, x 谢谢&问候 解决方案 正如 Ayrat 所说，使用目标和策略.这是一个例子:http://rise4fun.com/Z3Py/4I3 x = Int('x')y = Int('y')
..
Z3 Solver Java API:意外行为
通过向求解器添加条件，我想用“solver.check()"检查是否存在解决方案.因此，我创建了一个简单的示例来为 t1 找到解决方案.我知道 t1 有一个解，即 t1 = 0.然而，解算器没有状态“满足". public static void main(String[] args) {int h_max = 7;HashMapcfg = new HashMap();cfg.put("mode
..
Z3 表明如果 a^3=x*y*z 那么 3a <= x+y+z
我是 Z3 的新手(从今天开始).到目前为止非常喜欢它.很棒的工具.不幸的是，语法让我有点困惑. 我想证明如果: a^3 = xyz = m (带有 a, x, y, z, m (0..1) ) 然后: 3a 我通过尝试找到满足以下条件的模型来做到这一点: 3a > (x+y+z) 这是Z3代码: (declare-const a Real)(decla
..
(Z3Py) 函数声明有什么限制吗?
函数声明有什么限制吗? 比如这段代码返回unsat. from z3 import *def one_op (op, arg1, arg2):如果操作==1:返回 arg1*arg2如果操作==2:返回 arg1-arg2如果操作==3:返回 arg1+arg2返回 arg1+arg2 # 默认s=求解器()arg1, arg2, result, unk_op=Ints ('arg1 ar
..
如何使用量词访问 Z3 表达式
我想访问一个z3::expr.示例目录提供了以下代码段: void visit(expr const & e) {如果(e.is_app()){无符号数 = e.num_args();for (unsigned i = 0; i 我对函数应用部分没问题，但当我遇到量词时我错过了一些部分. 当 e.is_quantifier() 为真时，如何获得我拥有的量词(存在或全部)? 我知道
..
Z3 实数算法和数据类型理论整合得不是很好
这与我之前在 Z3 SMT 2.0 提出的问题有关vs Z3 py 实现我为无穷大的正实数实现了完整的代数，但求解器行为不端.当注释约束给出约束的实际解决方案时，我对这个简单实例一无所知. # 数据类型声明MyR = 数据类型('MyR')MyR.declare('inf');MyR.declare('num',('re',RealSort()))MyR = MyR.create()inf =
..
调整 Z3 中的“简化"策略
我有几个关于 Z3 策略的问题，其中大部分与 simplify 相关. 我注意到应用 simplify 后的线性不等式经常被否定.例如 (> x y) 被 simplify 转化为 (not (= 中，最好在简化公式中的所
..
Z3统计中的内存使用单位是什么?
z3 统计中衡量内存使用的单位是什么?是 MB 还是 KB? 内存到底是什么意思?是最大内存使用量还是执行过程中所有分配的总和? 解决方案 它是执行时最大堆大小的近似值，通过cmd_context.cpp中的以下函数添加到统计对象中: void cmd_context::display_statistics(...) {统计 st;...unsigned long long mem
..
如何使用 Z3 C++ api 读取 smtlib2 字符串?
我想从给定的 SMTLIB2 文件创建一个 expr 对象.我可以在 C 示例中看到 Z3_parse_smtlib_string 函数.expr 类中是否有一个包装器? 解决方案 Z3 C++ API 没有明确提供此功能作为 expr 类的一部分.但是，C++ API 可以与 C API 一起使用，即可以使用函数 Z3_parse_smtlib_string(或 ..._file)来实现
..
Z3 将数组的默认值设置为零
我正在尝试求解数组表达式的模型，其中数组的默认值等于 0. 例如，我试图解决这个例子，但我一直得到未知的结果 (declare-const arr (Array Int Int))(declare-const arr2 (Array Int Int))(declar-const 一个 Int)(declare-const b Int)(断言(forall((x Int))(=(选择arr
..
编码“at-most-k/at-least-k 布尔值为真"；Z3 中的约束
在 Z3 中对任意 k 和布尔变量的数量? 我正在考虑通过引入新的 PB 变量(使用 此编码)，通过双条件将它们与我的布尔变量相关联(例如 x == true iff y == 1)，并断言它们的总和大于或等于 k.这是一种合理的方法，还是我应该使用更简单/更有效的编码? 解决方案 最简单的方法是使用算术对基数约束进行编码.所以如果你想说 a + b + c = 2.底层求解器 Si
..
Z3 python 对待 x**2 与 x*x 不同?
Z3 Python 接口似乎不喜欢 ** 运算符，它可以处理 x*x 但不能处理 x**2，如下例所示 >>>x,y = x,y=Reals('x y')>>>z3.prove(暗示(x -6 == 0,x**2 -36 == 0))未能证明[x = 6]>>>z3.prove(暗示(x -6 == 0,x*x -36 == 0))证实 解决方案 您可能在 Linux 或 OSX 上使用
..
继续“未知"结果与 :pattern 在 SMTLIB v2 输入中的使用
我在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题:我一直使用以下输入获得结果“未知": (declare-datatypes () ((L L0 L1)))(declare-fun path() (List L))(declare-fun checkTransition((List L)) Bool)(define-fun isCons ((p (List L))) Bool(不是
..
“拉式嵌套量词"选项似乎在 UFBV 的上下文中引起问题?
我目前正在试验 Z3 作为用 Alloy(一种关系逻辑/语言)编写的规范的有界引擎.我使用 UFBV 作为目标语言. 我使用 Z3 选项 (set-option :pull-nested-quantifiers true) 检测到问题. 对于两个语义相同的 SMT 规范 Spec1 和 Spec2，Z3 超时(200 秒)以证明 Spec1 但证明 Spec2. Spec1 和
..
如果评论中间的`(check-sat)`调用，为什么查询结果会改变?
在调试 UNSAT 查询时，我注意到查询状态有一个有趣的差异.查询结构为: assert(...)(推) ;评论这两个电话中的任何一个(检查周六)；使整个查询 UNSAT，否则就是 SAT断言(...)(检查周六)；SAT 或 UNSAT 取决于先前通话的存在(出口) 查询中没有 pop 调用.触发此行为的查询是此处. 想法为什么? 注意:我实际上不需要增量，它仅用于调试
..
如何解决 Z3 中的最小化约束?
谁能告诉我如何通过 Z3py 实现像下面这样的最小化整数问题?我如何定义所有语句?这里所有的变量都是 int 排序的. Z3 中是否有专门的求解器可以解决此类问题?如果有，那么我如何为该求解器设置配置? 谢谢 解决方案 以下是一些相关/类似的问题和答案: 变量的最小值和最大值 确定上/下任意命题公式中变量的界限 如何优化Z3中的一段代码?(PI_NON_NES
..
Z3 支持指数
我是 Z3 的新手，我正在尝试了解它是如何工作的，以及它可以做什么和不能做什么.我知道 Z3 通过幂 (^) 运算符至少一些支持指数(参见 Z3py 使用 pow() 函数返回未知的方程，如何在 z3py 中表示对数公式 和 使用 Z3 和 SMT-LIB 定义带有实数的 sqrt 函数).我不清楚这种支持有多广泛，以及 z3 可以对指数做出什么样的推断. 这是一个简单的例子，涉及 z3 可
..
在没有python的posix系统上安装Z3?
是否可以在不安装 python 的情况下让 Z3 在提供 posix API 的系统上运行? 我已经看到新版本 4.3 在构建过程中使用了 python (scripts/mk_make.py).像 4.1 这样的旧版本怎么样?可以想象让它在没有 python 的情况下在 posix 上运行吗? 解决方案 Python 在您的系统中不可用吗? Python 一直用于自动生成 Z
..