z3 python API中结果不一致
z3 Python API是一个用于解决数学逻辑问题的开源工具包。它提供了一种方便的方式来表达和求解布尔逻辑、整数线性算术、位向量和其他相关问题。z3 Python API的结果不一致可能是由于以下几个原因：
- 问题表达不准确：在使用z3 Python API时，问题的表达方式可能存在错误或不准确，导致结果不一致。这可能包括错误的逻辑表达式、错误的约束条件或错误的求解方法。
- 算法限制：z3 Python API使用了一系列算法来求解问题，不同的算法可能在不同的情况下产生不同的结果。这取决于问题的复杂性、约束条件的数量和类型等因素。因此，结果不一致可能是由于使用了不同的算法或参数设置。
- 环境差异：z3 Python API的结果可能受到运行环境的影响。例如，不同的操作系统、硬件配置或软件版本可能导致结果的差异。此外，z3 Python API还可能与其他库或依赖项存在兼容性问题，进一步导致结果不一致。
为了解决z3 Python API中结果不一致的问题，可以采取以下措施：
- 仔细检查问题表达：确保问题的表达方式准确无误，包括逻辑表达式、约束条件和求解目标等。可以使用调试工具或打印输出来验证问题表达的正确性。
- 尝试不同的算法和参数：尝试使用不同的求解算法或参数设置，以寻找更稳定和一致的结果。z3 Python API提供了多种算法和参数选项，可以根据具体情况进行调整。
- 更新环境和依赖项：确保使用最新版本的z3 Python API和相关依赖项，并在稳定的运行环境中进行测试。如果可能，可以尝试在不同的环境中运行代码，以验证结果的一致性。
总结起来，z3 Python API中结果不一致可能是由于问题表达不准确、算法限制或环境差异等原因。通过仔细检查问题表达、尝试不同的算法和参数，以及更新环境和依赖项，可以提高结果的一致性和准确性。
相关·内容
1回答
是否考虑在将来的版本中支持酸洗(或序列化) Z3对象？我目前正在尝试将Z3 Python API生成的模型打包到一个文件中，我得到了错误消息ctypes objects containing pointers cannot be pickled，我认为这意味着Python API仅仅是Z3 DLL的包装器。
或者，有没有更好的方法将Z3 Python API生成的对象保存到文件中以供将来使用？
谢谢!
浏览 1提问于2013-01-30得票数 3
1回答
我正在使用Z3的ocaml，以便在获得unsat内核时命名每个约束，例如 (set-option :produce-unsat-cores true)
(declare-fun x () Int)
(assert (!(> x 0) :named p1))
(assert (!(not (= x 1)) :named p2))
(assert (!(< x 0) :named p3))
(check-sat)
(get-unsat-core) 结果是unsat。然后，我在Z3的ocaml中找到了一个API assert_and_track，在python (Unsatisfiab
浏览 40提问于2021-01-13得票数 1
回答已采纳
我正在使用z3 python。当我使用z3 python解决约束时，求解程序将无限运行，并且不会引发任何错误。但是，当相同的约束以smtlib2格式转储，然后通过z3可执行文件进行求解时，它几乎立即给出了sat或unsat。smtlib2转储非常大(大约1000行)。尽管对于少量的约束，z3 api工作得很好。z3 python中是否存在用于处理大量约束的bug？
浏览 5提问于2016-03-10得票数 0
回答已采纳
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
为什么这样做： >>> from z3 import *
>>> s = Solver()
>>> s.add([True])
>>> s.check()
sat 但这不是： >>> from z3 import *
>>> s = Solver()
>>> s.check([True])
Traceback (most recent call last):
File "<stdin>", line 1, in <module&g
浏览 21提问于2020-06-28得票数 1
回答已采纳
在C++中，z3::context context生成一个新context.Through这个具有新上下文的Z3表达式可以被创建为context.bv_const(variable_name, 16)。 如何使用z3 python api实现相同的行为呢？
浏览 38提问于2021-01-03得票数 0
回答已采纳
我使用的是z3 C++ API，在非线性整数算法方面存在一些问题，z3似乎对幂和乘法的处理方式不同。
x*x*x > y*y是sat，x^3 > y^2是unknown
#include <z3++.h>
#include <iostream>
using namespace std;
int main() {
z3::context c;
auto x = c.int_const("x");
auto y = c.int_const("y");
z3::solver sol(c);
浏览 3提问于2015-10-29得票数 1
回答已采纳
1回答
我正在使用z3 C++ API。如果我创建这个简单的false表达式：
z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);
试着解决，我得到了一个未知的结果。我不是战略和战术方面的专家，但我相信，如果我使用正确的策略，z3可以解决这个问题。
我也试过了
z3::expr p = !z3::forall(x, x==0);
当然，结果也是一样的。
浏览 0提问于2013-04-19得票数 1
我们使用的是微软Z3 C和C# API (我有两个程序)。
在Microsoft Z3中，当我们试图求解一个公式时，当有两个或多个可满足的解决方案时，Z3总是以相同的顺序返回结果。
是否可以从Z3中获得随机结果，以便对相同的输入在不同的执行过程中产生不同的输出序列？
请注意，我不能直接使用smt2代码。我这个，人们建议使用"random_seed“和"smt.arith.random_initial_value”参数。
(设置选项:smt.arith.random_initial_value true)
(声明-)
(声明-const y Int)
(断言(> (+ x)
浏览 1提问于2016-02-17得票数 0
3回答
我正在尝试使用z3的Python API来创建一个SMT实例。首先，我想创建四个位向量，具有两个位和从0到3的值。我用Python编写的初始化代码如下： import z3
NONE = z3.BitVecVal(0, 2)
A = z3.BitVecVal(1, 2)
B = z3.BitVecVal(2, 2)
C = z3.BitVecVal(3, 2) 但是我在运行Python文件时遇到了这个错误：AttributeError: module 'z3' has no attribute 'BitVecVal'。我查找了BitVecV
浏览 124提问于2020-03-23得票数 1
回答已采纳
1回答
我正在尝试使用Z3绑定安装OCaml，并获得以下错误。
cp ../src/api/ml/z3.mli api/ml/z3.mli
ocamlc -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli
File "api/ml/z3.mli", line 1159, characters 35-50:
Error: Unbound module Big_int
make: *** [api/ml/z3.cmo] Error 2
我首先尝试安装via
opam install z3
然后我尝试克隆Z3回购并运行
python scripts/m
浏览 0提问于2018-01-22得票数 2
回答已采纳
1回答
我正在使用python API for Z3为我的研究构建一个工具。我遇到了以下问题:我正在使用Python脚本生成一组Z3约束。由于集合可能不一致，我使用assert_and_check跟踪每个公式。例如,
s.assert_and_track(occWrites_1== True, 'p16')
当然，occWrites被声明为布尔值：
occWrites_1 = Bool('occWrites_1')
但是，在模型中，Z3将occWrites报告为整数。为什么会发生这种情况？模型中occWrites的值不应该是True或False吗？
浏览 0提问于2013-06-13得票数 1
回答已采纳
如何使用Z3 python API作为一阶公式的一部分来实现if-then-else？例如：
s.add( F, H, (if then else)).
一个相关的问题是:如何使用Z3 python在线指南中给出的布尔“暗示”或“如果”命令来实现此目的？
浏览 0提问于2012-08-05得票数 2
回答已采纳
我正在修改一个使用Z3 (特别是Python )来解决位向量约束的工具。我需要使用一个特定的外部SAT解决程序，而不是内部的Z3解决程序，所以我首先使用的是这个策略。
Then('simplify', 'bit-blast', 'tseitin-cnf')
之后，我可以相对轻松地将子句转储到DIMACS文件中。问题是将结果的命题模型映射回原始约束的模型:据我所知，Python没有提供一种方法来访问与策略相对应的模型转换器。这是真的吗？如果是这样的话，是否可以使用不同的API来完成，或者是否有更简单的方法呢？基本上，我只需要知道最后的CNF子句中的
浏览 5提问于2015-06-18得票数 5
回答已采纳
假设我有一个z3表达式： c = z3.Int("x")
Expr = (-c) / 2 是否可以使用Z3查找任意C，从而使表达式的计算结果为整数？ 例如，如果为c==1，则整个方程式的计算结果应为-0.5，因此不是整数。 我尝试使用reminder==0方法对问题进行建模 >>> from z3 import *
>>> c = Int("c")
>>> s = Solver()
>>> s.add(((-c) %2)==0)
>>> s.check()
sat 这显然
浏览 111提问于2021-10-12得票数 0
回答已采纳
1回答
我是z3的新手。我正在尝试使用z3运行下面的python示例。
from z3 import *
x = Real('x')
y = Real('y')
s = Solver()
s.add(And(x+y>1,x==0.00001,y==0.1))
print(s.check())
返回的结果是sat，我认为它与x+y=0.10001<1不正确。
[And(x + y > 1, x == 1/0, y == 1/10)]
我注意到它的术语x==1/0，分母是0。我使用Python3.9.8，z3-solver 4.8.12.0运行在macO
浏览 3提问于2021-12-02得票数 0
回答已采纳
我正在使用Z3及其Python模块为Python构建一个符号执行引擎。
我需要对字符串进行推理，但在当前的中似乎不支持
我发现它可以通过某种方式完成：
我如何让Z3使用它的python API来推断字符串？(也许可以扩展它？)
如果不可能，我可能会尝试将它实现为int数组(其中每个int表示字符串中的一个char )，并编写一些助手来推断它们。这样行得通吗？
我使用的是带有python3的4.3.2版本。
浏览 3提问于2014-05-13得票数 2
1回答
有没有办法获得z3模型名对应的python变量名？ 假设我有以下代码： from z3 import *
s = Solver()
a = [Real('a_%s' % k) for k in range(10)]
for i in range(10):
s.add(a[i] > 10)
s.check()
m = s.model()
for d in m:
print(d, m[d]) 在这里，m中的d是a_0, a_1, a_2,..., a_9，它们的所有值都是11。我正在尝试设置一些约束，使变量与之前的检查结果不相等，如下所示： s.a
浏览 21提问于2019-01-10得票数 0
回答已采纳
1回答
你好，我是Z3 SMT解决方案的新手。我知道您可以通过使用相关的API以编程方式调用Z3。但是，我想用Z3 SMT解决程序做以下事情：
如何用一个输入文件给programmatically?how ，我能逐步得到解决方案吗？
例如：
while ((check-sat) returns sat)
get the assignments for all boolean vairables
最后，在求解公式后，如何让Z3将结果保存到一个输出文件中？
有什么想法或文件我可以看吗？
谢谢百万！
浏览 3提问于2012-02-08得票数 0
回答已采纳
下面的程序使用来自主git分支的最新版本的Z3 (提交89c1785b)生成一个无法打印的Z3模型(即，print solver.model()抛出异常)：
x = Int('x')
a = Array('a', IntSort(), BoolSort())
b = Array('b', IntSort(), BoolSort())
c = Array('c', BoolSort(), BoolSort())
e = ForAll(x, Or(Not(a[x]), c[b[x]]))
print e
solver = Solv
浏览 1提问于2012-12-18得票数 1
回答已采纳
我的问题是，“不同”在z3 python中是否有效？我比较了以下代码，结果似乎不一样：
(declare-const x Int)
(declare-const y Int)
(assert (distinct x y))
(check-sat)
(get-model)
结果是：
sat
(model
(define-fun y () Int
0)
(define-fun x () Int
1)
)
我只是为了测试而添加了否定断言，结果是unsat，这是正确的：
(assert (= x y))
unsat
Z3(6, 10): ERROR: model
浏览 2提问于2015-01-08得票数 3
回答已采纳
1回答
我目前正在使用Z3的最大化API (opt分支)，我偶然发现了以下一个bug：
每当我给它任何无界问题时，它只会返回OPT，并在结果模型中给出零(例如，最大化Real('x')，而模型上没有约束)。
Python示例：
from z3 import *
context = main_ctx()
x = Real('x')
optimize_context = Z3_mk_optimize(context.ctx)
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast)
Z3_opt
浏览 5提问于2014-09-26得票数 1
回答已采纳
我在z3 shell和java api中都尝试了相同的假设。如下所示：
(declare-const x (_ BitVec 32))
(assert (not (bvsle (bvadd x #xfffffff8) #x00000000)))
(check-sat)
(get-model)
在z3外壳中，解决方案是:x=9，但在z3应用程序接口中，解决方案是:x= 0x80000000在我的应用程序中，我更喜欢外壳结果。所以我想知道我是否错过了API使用中的一些选项。
顺便说一句。有没有什么选项可以用来控制解的值，我想要一些更合理的值。但通常Z3会给我一些非常大的值，看起来像是随机值。
浏览 0提问于2016-11-08得票数 1
1回答
我希望在z3 api中使用api_parsers来解析smt2命令，然后我希望看到结果vectors的内容(如排序、变量、参数等)。
但我不知道该怎么做？我写了一段如下代码：
#include<iostream>
#include<z3++.h>
#include<z3_api.h>
using namespace z3;
int main() {
context ctx;
//z3_string fname = ;
Z3_ast a = Z3_parse_smtlib2_file(ctx, "smt_z3.smt2", 0, 0
浏览 0提问于2016-04-10得票数 0
1回答
我使用Z3 Python绑定通过z3.And(exprs)创建一个And表达式，其中exprs是一个包含布尔变量上48000个等式约束的python。这个操作在2.6GHz处理器的MBP上需要2秒。
我做错什么了？这是z3 Python绑定的问题吗？对如何优化这种结构有什么想法吗？
顺便说一句，在我的实验中，这些表达式的构造比求解结果公式花费更多的时间:)
浏览 4提问于2014-10-15得票数 4
回答已采纳
1回答
我使用的是Z3版本4.4.2 - 64位的python API，我试图理解为什么z3在这种情况下简化了表达式：
>>> a = Array('a', IntSort(), IntSort())
>>> a = Store(a, 0, 1)
>>> a = Store(a, 0, 3)
>>> simplify(a)
Store(a, 0, 3)
但在本例中并非如此：
>>> a = Array('a', IntSort(), IntSort())
>>>
浏览 1提问于2016-10-18得票数 0
1回答
z3py安装
、、
我很难让z3使用Python。我正在运行Windows 7 64位。我下载了64位Python3.3.0和64位z3 4.3.0。我已经更新了我的PATH和PYTHONPATH以包括z3 \bin目录。但是，当我试图在python中使用z3时，会出现以下错误：
从z3导入*回溯(最近一次调用)：文件""，在ImportError中的第1行：'z3'：B‘\x03\xf3\r’中的坏魔术号
有人知道出了什么问题吗?怎么解决呢？
谢谢
浏览 1提问于2013-03-26得票数 0
回答已采纳
1回答
我刚刚发现Z3 JAVA API中名为"mkDiv()“的除法是指整数除法，而不是普通除法。例如： ArithExpr a = ctx.mkDiv(ctx.mkInt(3),ctx.mkInt(5)).simplify(); A的结果是"0“但"3/5”。 在tutor中，除法和整数除法似乎是分开的两部分：(assert (= r1 (Diva4)；整数除法(assert (>= b (/ c3.0)在Z3 java api中的除法在哪里？
浏览 14提问于2020-10-18得票数 0
回答已采纳
1回答
如果你不知道Z3求解器，请不要回答。我之前发布了这个问题，一些答案，比如如何用C实现up.There中的数组，是一些在这个forum.Its中开发Z3求解器的人，目的是为了them.If你不知道Z3求解器，请避免回答这个问题。
我早些时候发布了这个问题，并得到了解决方案，因为在Python.we中已经实现了以下问题已经在python.we中尝试移植Z3求解器来集成Z3求解器到内部工具作为我的thesis.Could的一部分，您帮我显示了解决方案的"C“语言，而不是在Python语言的以下要求。
我想要定义并创建一个二维数组，如下所示，使用z3求解器，使用C
示例: a3如何使用Z3求解
浏览 0提问于2013-04-22得票数 1
回答已采纳
2回答
我正尝试在python3中运行一个将Z3作为依赖项的程序(导入z3)
我能够安装Z3的不稳定版本(假设支持Python3)，但它只安装了python2.7的库。
项目中的：
python scripts/mk_make.py
cd build
make
sudo make install
有人知道如何在Python3上安装Z3 work吗？
谢谢。
浏览 1提问于2014-02-21得票数 2
我试过安装z3定理验证器。我正在使用Ubuntu 16.04。我正在使用Python2.7.12
我用两种方式进行了安装：
我用了sudo apt-get install z3
但是，当我试图通过使用z3从终端中打开python并使用import z3 as z导入时，我发现了一个错误：No Module named z3
我用过
python scripts/mk_make.py cd build make sudo make install
并且还将build/python添加到PYTHONPATH中，将build添加到LD_LIBRARY_PATH中，但当我尝试使用相同的
浏览 4提问于2017-09-22得票数 1
回答已采纳
2回答
我想对z3::expr对象进行一些转换。如何在C++接口中使用Z3_substitute_vars、Z3_translate和Z3_substitute_？它们是用C#实现的，但我在C++中找不到它们。奇怪的是，它们并没有被实现。
我尝试使用C api，但没有任何结果，下面是一个示例：
void substitute(){
z3::context c;
z3::expr a = c.int_const("a");
Z3_ast astA = a;
z3::expr plus = 2*a;
errs() << Z3_ast_to_string(c,plus);
z3:
浏览 0提问于2013-04-17得票数 0
回答已采纳
中指出的安装问题仍然存在。我曾尝试在Windows XP SP3 32位和Windows 7 64位下安装Windows4.3.0和4.1。所有的组合都不起作用！我可以执行"from z3 import *“命令，但Z3 dll的init()命令失败。我的Python版本是2.7.3。Z3单机版和Python单机版确实可以工作，但它们在一起工作时会有很多抱怨。
获取回答以下问题的最新安装方法会很有帮助：
应该使用哪种Z3下载(源代码版本、预编译版本)？
应该使用哪个Python版本？
在init()调用中应该引用哪些或各种Z3 DLL？举个例子会有所帮助(包括带空格的路径的原始字符串用
浏览 1提问于2013-02-13得票数 1
回答已采纳
1回答
我试图使用z3来证明以下身份：
x+y == x^y + 2*(x&y)
也就是说，我们可以用布尔指令和算术指令的混合代替任何加法(例如取自第2.2章，)。
我正在使用以下z3 python片段：
from z3 import *
x = BitVec("x", 32)
y = BitVec("y", 32)
lhs = x ^ y + (2*(x&y))
rhs = x + y
s = Solver()
s.add(lhs != rhs)
print s.check()
print s.model()
然而，z3给了我以下内容：
浏览 3提问于2015-02-02得票数 1
回答已采纳
1回答
我正在试验优化使用Z3来证明一阶理论的事实.目前，我在Python中指定了一阶理论，将量词放在那里，并将所有子句连同证明目标的否定一起发送给Z3。我有以下的想法，我希望能优化结果:我只想把理论中的公式发送给Z3，这些公式与证明目标相关。我不打算详细讨论这个概念，但我认为直觉很简单:我的理论是公式的结合，我只想发送可能影响证明目标的真值的连词。
我的问题是:这能导致效率的提高吗，还是Z3已经使用了类似的方法？我想不会，因为我不认为Z3总是假设最后的断言是证明的目标，所以它没有优化的方法。
浏览 4提问于2012-12-21得票数 1
回答已采纳
我正在尝试在b上使用ForAll量词，所以每个b的公式a * b == b都会给我a == 1作为结果。我在下面的代码(Z3 Python)中实现了这一点：
from z3 import *
a, b, a1 = BitVecs('a b a1', 32)
f = True
f = And(f, a1 == a * b)
f = And(f, a1 == b)
s = Solver()
s.add(ForAll(b, f))
if s.check() == sat:
print 'a =', s.model()[a]
else:
prin
浏览 2提问于2013-06-16得票数 2
回答已采纳
2回答
我在Windows XP上通过IDLE GUI使用Python2.7.3，并尝试通过Python API在本地运行Z3 4.0。
这一行运行得很好：
>>> from z3 import *
这一行不是：
>>> x = Int('x')
Traceback (most recent call last):
[...]
File "C:\Program Files\Microsoft Research\Z3-4.0\python\z3core.py", line 34, in init
_lib = ctypes
浏览 1提问于2012-06-28得票数 1
回答已采纳
1回答
我正在使用Z3的python API来解决一组约束是否可满足的问题。我有字符串形式的条件，我想尽可能直接将它们传递给z3，这样可以节省转码的处理时间。如果约束是像a=b这样的赋值，那么输入它的最佳方式是什么。我想要像这样的东西
str1 = "a = b"
a = BitVec('a', 3)
b = BitVec('b', 3)
s = Solver()
s.push()
s.add(str1)
此程序给出的错误为"True，False or Z3 Boolean expression e
浏览 1提问于2013-05-10得票数 3
回答已采纳
1回答
让z3在pydev上工作有困难。
下载Python后，我转到eclipse窗口>首选项> PyDev >解释器> z3解释器，然后将"z3/bin“添加到库中
运行Python2.7.11和z3 32位
当我尝试运行简单的代码时
from z3 import*
x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
获取错误
NameError: name 'Int' is not defined
浏览 2提问于2016-02-24得票数 0
1回答
我一直在使用一个非常基本的用户节流率与我的DRF API，并得到了刚刚..。当我试图运行基准测试时，结果是荒谬的。
例如，当我将节流阀设置为15/天时，我的python基准标记能够使29 (？？)请求在实际被节流之前。
以下是我的基本设置：
# Django Rest Framework
REST_FRAMEWORK = {
...
'DEFAULT_THROTTLE_CLASSES': [
'rest_framework.throttling.UserRateThrottle',
],
'DEFAULT_THR
浏览 5提问于2022-04-06得票数 1
回答已采纳
1回答
例如,
$ z3 -in
(declare-fun f (Int Real) Int)
(assert (= f f))
(check-sat)
sat
这样就可以了。
不过，我想用as对它进行限定
$ z3 -in
(declare-fun f (Int Real) Int)
(assert (= (as f ???) (as f ???)))
(check-sat)
sat
我应该填写什么???？
这一定是一种，但我应该用哪种呢？
我试过((Int Real) Int)、(-> (Int Real) Int)或(_ (Int Real) Int)，但没有一个是正确的。
可以在smtl
浏览 6提问于2021-09-29得票数 0
回答已采纳
我试图使用Z3 API为python找到一个最优的解决方案。我使用set_option("verbose", 1)打印Z3在检查sat时生成的语句。它打印的语句之一是pb.conflict语句。语句看起来像这样-- 。
我想知道pb.conflict到底是什么。这些声明意味着什么？还有，和它一起打印的两个数字是什么？
浏览 0提问于2018-11-02得票数 1
回答已采纳
我在Mac上看到了z3py的一个奇怪的问题，我想知道是否有人以前见过这个问题：
$ cat bug.py
from z3 import *
x = Int('x')
s = Solver()
s.add(x > 5)
print(s.check())
print(s.model())
$ python bug.py
sat
[x = ]
模型中缺少x的值。我尝试了主分支和不稳定分支，结果相同。但是，如果在类似的.smt2文件上运行，z3本身确实会给出正确的模型。我的配置是Mac 10.6.8，Python 2.7.4。
浏览 2提问于2013-05-09得票数 1
2回答
我使用Z3的python来做一些线性实运算。我遇到过这样一种情况，即非常接近于零的reals以某种方式被转换为1.0/0.0。这反过来又会导致Z3的C++部分内出现浮点异常。
例如，我有以下Python程序：
from z3 import *
s = Solver()
s.add(0.00001 * Real("a") + 0.00001 * Real("b") > 0.0)
print(s.to_smt2())
result = s.check()
print(result)
print(s.model())
它产生以下输出：
; benchmark g
浏览 0提问于2021-10-22得票数 0
回答已采纳
1回答
我正在尝试用python为Tausworthe随机数生成器实现以下c代码。代码需要生成0到1范围内的随机数，c代码如下：
#include <stdint.h>
#include <stdio.h>
/**** VERY IMPORTANT **** :
The initial seeds z1, z2, z3, z4 MUST be larger than
1, 7, 15, and 127 respectively.
****/
#define SEED 987654321
static uint32_t z1 = SEED, z2 = SEED,
浏览 15提问于2019-08-10得票数 0
回答已采纳
我看到了一个，它谈到了如何使用z3的python来获得最小化问题的次优解。
我遇到了MAXSMT问题，我想知道在指定超时时如何使用Z3命令行工具找到次优解决方案？
是否仅使用-t:timeout选项就能给出一个次优解？
Z3求解器花了150秒找到了我的MaxSMT问题的最优解。
我使用z3 -t:140000 smt2 <filename>将超时设置为140秒。但是z3求解器返回未知值(而不是sat和一个非零的目标值)。我也尝试了超时145秒，并看到了类似的结果。当我将超时设置为> 150时，我得到了最优解
我应该添加更多的东西来获得次优解吗？
浏览 2提问于2018-01-25得票数 3
回答已采纳
我正在使用Z3的Python，试图在我正在编写的一个研究工具中包含对它的支持。关于使用Python接口提取不可满足的核心，我有一个问题。
我有以下简单的查询：
(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)
通过z3可执行文件(对于Z3 4.1)运行此查询，我将收到预期的结果：
unsat
(__constraint0)
对于Z3 4.3，我获得一个分段错误：
u
浏览 8提问于2013-01-28得票数 3
回答已采纳
1回答
我尝试在pydev中使用z3，我将z3py和libz3.dll的路径添加到window/preferences/pydev/jython-interpreter，但得到的错误如下
回溯(最近一次调用)：文件python第11行，在导入z3文件“C：\Users\linda\ z3 \ "C:\Users\linda\workspace\LearningPyDev\main.py"，\z3.py”中，第45行，从z3printer导入*文件"C:\Users\linda\z3\python\z3printer.py"，第8行，在导入sys，io，z3 Import
浏览 1提问于2013-04-03得票数 0
2回答
我正在尝试使用make/g++和Python从源代码(v4.3.1.，2013年11月，z3-89c1785b7322)构建Z3，结果如下
autoconf -- succeeded
./configure -- succeeded
python scripts/mk_make.py -- error message, given below
Traceback (most recent call last):
File "scripts/mk_make.py", line 2
浏览 4提问于2014-01-18得票数 0
1回答
我是Z3求解器的新手，在C++中使用API，我想解决一组不等式并找到结果。 我读过the answer which written in Python并尝试用C++编写它，但它重复打印一个模型。 5 <= x + y + z <= 16
AND -4 <= x - y <= 6
AND 1 <= y - z <= 3
AND -1 <= x - z <= 7
AND x >= 0 AND y >= 0 AND z >= 0 不等式被添加到求解器中，并有许多评估。 C是上下文，s是求解器。 vector<const
浏览 16提问于2019-05-11得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
实时音视频
即时通信 IM活动推荐
腾讯云开发者
