标签: z3

关于Z3如何逐步解决问题,我有一个问题.在阅读了一些答案后,我发现了以下内容:

1. 有两种方法可以使用Z3进行增量求解:一种是推/弹(堆栈)模式,另一种是使用假设.Z3中的软/硬约束.
2. 在堆栈模式下,z3会忘记全局(我是对吗？)范围内所有学习的引理,即使在SMT求解器中有一个局部"弹出" 约束强化效率之后
3. 在假设模式中(我不知道名称,这是我想到的名称),z3不会简化一些公式,例如值传播.z3行为根据不满核心的要求而变化

我做了一些比较(欢迎你问一下这些公式,它们太大而无法放在rise4fun上),但这里是我的观察:在一些公式中,包括量词,假设模式更快.在一些包含大量布尔变量(假设变量)的公式中,堆栈模式比假设模式更快.

它们是否针对特定目的实施？增量求解如何在Z3中起作用？

我想知道是否有人可以告诉我Z3和coq之间的区别？在我看来,coq是一个证明助手,因为它要求用户填写证明步骤,而Z3没有这个要求.但似乎coq也有类似于Z3的自动战术？或者也许coq中的证明搜索能力不如Z3强大？

我知道乘法的整数理论通常是不可判定的.然而,在某些情况下,Z3确实返回了一个模型.我很想知道这是怎么做到的.它是否与用于实数的非线性算术的新决策程序有关？已经识别出哪些特定实例(例如:有限模数下的整数等),Z3为其返回乘法查询的模型？任何帮助深表感谢.

我正在尝试使用微软研究院开发的SMT求解器Z3检索所有可能的一阶理论模型.这是一个最小的工作示例:

(declare-const f Bool)
(assert (or (= f true) (= f false)))

在这个命题案例中,有两个令人满意的任务:f->true和f->false.因为Z3(以及一般的SMT求解器)只会尝试找到一个令人满意的模型,所以找不到所有解决方案是不可能的.在这里,我发现了一个有用的命令(next-sat),但似乎最新版本的Z3不再支持这一点.这对我来说有点不幸,总的来说我觉得这个命令非常有用.还有另一种方法吗？

我正在尝试将OpenJML与Z3结合使用,而我正试图推理double或float重视:

class Test {

  //@ requires b > 0;
  void a(double b) {
  }

  void b() {
    a(2.4);
  }
}

我已经发现OpenJML AUFLIA用作默认逻辑,不支持reals.我现在正在使用AUFNIRA.

不幸的是,该工具无法证明此类:

? java -jar openjml.jar -esc -prover z3_4_3 -exec ./z3 Test.java -noInternalSpecs -logic AUFNIRA

Test.java:8: warning: The prover cannot establish an assertion (Precondition: Test.java:3: ) in method b
    a(2.4);
     ^
Test.java:3: warning: Associated declaration: Test.java:8: 
  //@ requires b > 0;
      ^
2 warnings

为什么是这样？

我是 SAT 求解器的新手，需要一些有关以下问题的指导。

考虑到：

? 我在 4*4 网格中选择了 14 个相邻的单元格

? 我有 5 个多联骨牌（A、B、C、D、E），大小分别为 4、2、5、2 和 1

? 这些多联骨是自由的，即它们的形状不是固定的，可以形成不同的图案。

如何使用 SAT 求解器计算所选区域（灰色单元格）内这 5 个自由多联骨牌的所有可能组合？

借用@spinkus 有见地的答案和 OR-tools 文档，我可以制作以下示例代码（在 Jupyter Notebook 中运行）：

from ortools.sat.python import cp_model

import numpy as np
import more_itertools as mit
import matplotlib.pyplot as plt
%matplotlib inline


W, H = 4, 4 #Dimensions of grid
sizes = (4, 2, 5, 2, 1) #Size of each polyomino
labels = np.arange(len(sizes))  #Label of each …

在Z3Py中,如何检查给定约束的方程是否只有一个解？

如果有多个解决方案,我该如何枚举它们？

如何从Z3模型中获取真正的python值？

例如

p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
s.check()
print s.model()[x]
print s.model()[p]

版画

-1.4142135623?
False

但那些是Z3对象而不是python float/bool对象.

我知道我可以使用is_true/ 检查布尔值is_false,但是如何优雅地将ints/reals/...转换回可用值(例如,不通过字符串并删除这个额外的?符号).

我正在尝试使用SMTLIB接口为Z3定义集合理论(并集,交集等).不幸的是,我的当前定义为一个简单的查询挂起z3,所以我想我错过了一些简单的选项/标志.

这是固定链接:http: //rise4fun.com/Z3/JomY

(declare-sort Set)
(declare-fun emp () Set)
(declare-fun add (Set Int) Set)
(declare-fun cup (Set Set) Set)
(declare-fun cap (Set Set) Set)
(declare-fun dif (Set Set) Set)
(declare-fun sub (Set Set) Bool)
(declare-fun mem (Int Set) Bool)
(assert (forall ((x Int)) (not (mem x emp))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem …

当使用使用Z3(我在Visual Studio命令提示符中构建)的python脚本(oyente)时,我遇到以下错误:

File "C:\Python27\Lib\site-packages\oyente\z3\z3core.py", line 23, in lib
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3.z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.__del__ of <z3.z3.Context instance at 0x0000000003A5AC48>> ignored

我libz3.dll在z3和oyente目录中有文件,在系统变量的PYTHONPATH中,我添加了可能需要的每个目录,例如: