如何在Python中使用Z3解决SMT问题
我在使用Python的软件包Z3来解决一些SMT问题时有一些问题，
我的老师告诉我输入：Z3 km_test.smt在Pycharm的终端中，但我收到了：
用法：z3 [-h] [-s3-prefix s3_prefix] [ - s3 prefix s3_prefix] [ - 文件系统文件系统] [ - snapshot-prefix snapshot_prefix] {backup，restore，status} ... Z3：错误：参数子命令：无效的选择：'KM_TEST.SMT'（从'Backup'，'Restore'，'状态'中选择），
他们可以回答我如何处理此问题。
I have some problem in using python's package z3 to solve some smt question
my teacher told me to input: z3 km_test.smt in terminal of pycharm,but I received :
usage: z3 [-h] [--s3-prefix S3_PREFIX] [--filesystem FILESYSTEM] [--snapshot-prefix SNAPSHOT_PREFIX] {backup,restore,status} ...
z3: error: argument subcommand: invalid choice: 'km_test.smt' (choose from 'backup', 'restore', 'status')
who can answer me how to deal with this problem.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您正在运行 zfs zfs to Zfs to AWS S3备份工具，而不是 Z3定理供您来自Microsoft Research 。
如果要使用python的稍后Z3
you're running z3 for ZFS to AWS S3 backup tool, not z3 theorem prover from Microsoft Research.
if you want to use the later Z3 for python, You should install the Python wrapper for Z3 for the latest release from pypi using the command