标签: z3

我想在 Z3 中对固定大小的内存缓冲区及其访问操作进行建模。缓冲区的大小可以从几个字节到数百个字节不等。几个现有工具（例如，KLEE）采用的标准方法是在位向量的域和范围内创建数组变量。每个内存缓冲区都会获得这样一个数组，并且内存读/写使用select/store操作进行编码。

唉，在我的基准测试中，使用这种方法时，Z3(*) 似乎始终比 STP 慢。在更详细地分析查询以弄清楚发生了什么之前，我想确保我使用了“正确”的方法来编码 Z3 中的内存操作（因为，无可否认，STP 专门设计用于数组和位向量）。

那么在 Z3 中表示内存缓冲区的最有效方法是什么？到目前为止，我正在考虑几个替代方案：

1. 使用断言来指定内存缓冲区的初始值，而不是使用嵌套的store-s。然而，在我的初步测试中，这似乎更能减慢 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器是否可以有效地处理它。
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量。但是，我担心这会使模型复杂化并引入对量词的需求。
4. 使用未解释的函数而不是数组，但这需要以可能比 Z3 自己的内置数组理论效率低的方式重新定义数组公理。

有没有更好的方法我错过了？

(*) 默认非增量求解器，Z3 分支 unstable@aba79802cfb5

我需要你的帮助，用 Z3 Java API 定义一个函数。我尝试解决这样的问题（在 z3.exe 进程中工作正常）：

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)

(define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x))

(assert (and (>= a 0.0) (<= a 100.0)))
(assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))

(check-sat-using (then simplify bit-blast qfnra))
(get-model)

此 smt 文件的结果是：

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun c () Bool
    false) …

我无法让任何 z3py 示例正常工作。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了 python 路径以指向适当的目录。此外，我能够成功导入 z3，但每次声明变量时都会出现错误。编译器无法识别 Int、Ints、Real 和 RealVal。

我举了一个例子来说明。

代码：

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

错误：回溯（最近一次调用）：文件“test.py”，第 3 行，在 x = Int('x') 中 NameError: 名称 'Int' 未定义

我真的很感激任何帮助。太感谢了。

我知道非线性整数算术基本上是希尔伯特的第十个问题，并且被证明是不可判定的。然而，Z3 求解器能够为非线性实数算法提供完整的解决方案。我只是好奇这两个问题之间的根本区别是什么，以便有一个确定的非线性实数算法？

似乎有一篇关于 Z3 实现非线性多项式实数算法的论文。我没有很强的正式方法/数学背景。对这个问题背后的任何直觉表示赞赏！

是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，在其中我可以通过某些标签/名称唯一标识每个约束？

我想唯一地标识约束的原因是，我可以稍后通过指定该标签/名称来删除它们。需要删除约束是因为我之前的约束随着时间变得无关紧要。我看到使用 Z3 我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式“(check-sat p1 p2 p3)”的 check-sat，即如果我有三个断言要检查，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，

我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者有其他方法来处理它的 API。我将不胜感激任何建议或意见。

我想证明涉及矩阵和向量的表达式的属性（可能很大，但大小是固定的）。

例如我想证明一个表达式的结果是对角矩阵或三角矩阵，或者是正定的，...

为此，我想从线性代数中编码众所周知的属性和身份，例如：

||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
det(A+B) = det(A) + det(B)
Tr(zA) = z * Tr(A)
(I + AB) ^ (-1) = I - A(I + BA) ^ (-1) * B
...

我试图在 Z3 中实现这一点。但即使对于简单的属性，它也会返回未知或超时。我尝试过数组理论和量词。

我想知道这个问题是否可以用 SMT 求解器解决，还是不适合这类问题？你能举一个小例子来暗示吗？

假设我想检查公式 x+y=z（x,y,z 整数）是否可满足。使用 Z3 我可以输入如下内容：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= z (+ x y)))
(check-sat)

我可以等效地使用 OCaml api 并编写以下代码：

let ctx=Z3.mk_context  [("model", "true"); ("proof", "false")] in 
let v1=(Z3.Arithmetic.Integer.mk_const_s ctx "x") in
let v2=(Z3.Arithmetic.Integer.mk_const_s ctx "y") in
let res=(Z3.Arithmetic.Integer.mk_const_s ctx "z") in
let sum=Z3.Arithmetic.mk_add ctx [ v1 ; v2] in 
let phi=Z3.Boolean.mk_eq ctx sum res in
let solver = (Z3.Solver.mk_solver ctx None) in
let _= Z3.Solver.add solver [phi] in
let is_sat=Z3.Solver.check solver …

我正在 python 中试验 z3。我有以下模型：

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) …

为了学习 Z3，我尝试使用 Haskell 绑定解决我最喜欢的代码出现问题之一（一个特别困难的问题，2018 年第 23 天，第 2 部分）sbv。前面代码中的剧透......

module Lib
    ( solve
    ) where

import Data.SBV

puzzle :: [((SInteger, SInteger, SInteger), SInteger)]
puzzle = (\((x, y, z), r) -> ((literal x, literal y, literal z), literal r)) <$> [
      ((60118729,58965711,8716524), 71245377),
      {- 999 more values that are large like the first one... -}
]

manhattan (a1, a2, a3) (b1, b2, b3) =
  abs (a1 - b1) + abs (a2 - b2) + abs (a3 - …

如何为 z3 优化器设置超时，以便在超时时为您提供最知名的解决方案？

from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())

后续问题，你可以将z3设置为随机爬山还是始终执行完整搜索？