1回答
我正在使用python API for Z3为我的研究构建一个工具。我遇到了以下问题:我正在使用Python脚本生成一组Z3约束。由于集合可能不一致，我使用assert_and_check跟踪每个公式。s.assert_and_track(occWrites_1== True, 'p16')occWrites_1 = Bool('occWrites_1')
但是，在模型中，Z3<
浏览 0提问于2013-06-13得票数 1
回答已采纳
1回答
(< x 0) :named p3))(get-unsat-core) 结果是unsat。然后，我在Z3的ocaml中找到了一个API assert_and_track，在python (Unsatisfiable Cores in Z3 Python)中找到了一个解决方案，然后我有了以下简单的示例unsat(set-info :status
浏览 40提问于2021-01-13得票数 1
回答已采纳
1回答
有没有一种方法可以像在Python中那样以人类可读的形式打印AST？我想要一些像这样的东西而不是
(and (= x 3) (> (f 3) 2)
浏览 2提问于2013-04-23得票数 1
回答已采纳
1回答
我的程序使用Z3_open_log()创建所有z3交互的日志。然后在另一个程序中，我用Z3_parse_z3_file()将其读回。它给了我在输入上做出的所有断言的连接。然后通过解析z3文件，我得到(和a1 a2)。如果这不是我应该走的路，你会推荐哪条路？AG.
浏览 1提问于2012-03-29得票数 1
回答已采纳
1回答
是否考虑在将来的版本中支持酸洗(或序列化) Z3对象？我目前正在尝试将Z3 Python API生成的模型打包到一个文件中，我得到了错误消息ctypes objects containing pointers cannot be pickled，我认为这意味着Python API仅仅是Z3 DLL的包装器。或者，有没有更好的方法将Z3 Python API生成的对象保存到文件中以供
浏览 1提问于2013-01-30得票数 3
2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。
浏览 1提问于2012-09-03得票数 3
回答已采纳
我在Linux上安装了Python，并且正在使用它的绑定(Z3Py)。我如何解决这个问题，并启动并运行Z3？Z3文档和教程似乎没有提到这一点或关于init()的任何内容，也没有列出任何名为init()的函数。更详细地说，下面是我尝试过的(略有摘录)：Python 2.7.13 (default, Jan 12 2017, 17:59:37)>>File "/usr/
浏览 12提问于2017-03-28得票数 2
我正在使用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
回答已采纳
我想将Z3中的boolExpression转换为中缀表示。例如，有一个z3表达式(>= t 3)，我想得到中缀字符串"t>=3"，有没有现有的Z3应用程序接口可以在C#中实现它？
浏览 3提问于2012-07-23得票数 1
1回答
目前，我正试图将一个问题编码到Z3中，并且我希望建模一个“三态”布尔(即带有true、false和unknown的布尔值)。#!/usr/bin/env python
from collections import OrderedDict
Tristate!
浏览 2提问于2017-10-17得票数 1
1回答
我想学习用于c++的z3 API以及如何在c++程序中使用它们。我试着找一个教程，但是找不到。我可以从哪里学到呢？有什么教程什么的吗？谢谢。
浏览 1提问于2013-07-08得票数 1
1回答
我们有一个使用.NET API v4.0的Z3项目。我们希望能够在Mono上编译和运行该项目。这听起来很奇怪，但我们的情况如下。我们有一个使用Z3的课程，所有的实验室计算机都安装了Windows和.NET框架。标记下添加以下信息：
<dllmap dll="z3.dll" target="libz3.dylib" os="osx" cpu="
浏览 3提问于2013-01-13得票数 10
回答已采纳
下面的程序使用来自主git分支的最新版本的Z3 (提交89c1785b)生成一个无法打印的Z3模型(即，print solver.model()抛出异常)：a = ArrayFile "src/api/python/z3printer.py", line 841, in __call__
File "src/api/python/z3printer
浏览 1提问于2012-12-18得票数 1
回答已采纳
在C++中，z3::context context生成一个新context.Through这个具有新上下文的Z3表达式可以被创建为context.bv_const(variable_name, 16)如何使用z3 python api实现相同的行为呢？
浏览 38提问于2021-01-03得票数 0
回答已采纳
(m.evaluate(X[k])): else:输出为:在线运行此示例
在此示例中，在本例中，引入矩阵M作为手工输入。请告诉我如何自动介绍矩阵M ()。非常感谢。
浏览 1提问于2013-07-13得票数 0
回答已采纳
我使用的是z3 C++ API，在非线性整数算法方面存在一些问题，z3似乎对幂和乘法的处理方式不同。::pw(x,3) > z3::pw(y,2));}
我已经读过一些关于python问题()的文章，但是我使用了z3的4.4.0版本，在这里应该修复这个问题。我知道非线性整数算法在一般情况下是不可判定的，但我感到有点惊
浏览 3提问于2015-10-29得票数 1
回答已采纳
1回答
我想找到一个纯python z3包，它将帮助我在google应用程序引擎中运行z3。我已经在本地运行了以下python测试并运行： y = Real('y') s.add我的问题是纯python z3库的可用性。从google关于沙箱的文档中，我非常肯定这些*.pyc文件是正
浏览 1提问于2014-06-29得票数 1
回答已采纳
我只是想研究一下z3及其.NET接口。我使用PowerShell来实现它，以使它更具有交互性。我的第一个hello world在下面。当我在python (在google中)尝试这一点时，它就变得更加混乱了。solve(x*x-1==0)
在这两种情况下我都做错了什么？
浏览 3提问于2022-01-18得票数 0
回答已采纳
1回答
我正在尝试用z3做一件有点奇怪的事情。我正在尝试看看是否可以使用z3从交互式定理证明者那里获得类似"apply“的策略。有没有一种方法可以用z3得到适当的x？我不能只使用一个模型，因为c可能包含自由变量。我一直在尝试看看是否可以在Implies(ForAll([x],b(x)), c)这样的查询的z3验证术语中找到它，或者以某种方式使用E-matching pattern工具，但我被难住了。z3内部必须具有复杂的匹配和统一功能，但我看不出它们会在python接口中暴露在哪里。
浏览 11提问于2019-12-19得票数 0
云服务器
对象存储
ICP备案
云点播
实时音视频
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号