这是可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行的命令 z3，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
z3 - 来自 Microsoft Research 的最先进的定理证明器
概要
z3 [选项] [-文件：]文件
商品描述
本手册页简要记录了 z3 命令。
z3 Z3 是来自 Microsoft Research 的最先进的定理证明器。 它可以用来
检查逻辑公式对一种或多种理论的可满足性。 Z3 提供了一个
软件分析和验证工具的引人注目的匹配，因为几个常见的
软件结构直接映射到支持的理论。
输入 格式
-smt 对 SMT 输入格式使用解析器。
-smt2 对 SMT 2 输入格式使用解析器。
先生 对 Datalog 输入格式使用解析器。
-迪马克斯
对 DIMACS 输入格式使用解析器。
-日志 对 Z3 日志输入格式使用解析器。
-在 从标准输入读取公式。
其他
-h | -?
打印使用信息。
-版
打印 Z3 的版本号。
-v:级别
详细点，哪里是详细级别。
-西北 禁用警告消息。
-p 显示 Z3 全局（和模块）参数。
-PD 显示 Z3 全局（和模块）参数说明。
-pm:姓名
显示Z3模块参数。
-pp:名称
显示 Z3 参数说明，如果未提供，则所有模块名称
被列为。
-- 所有剩余的参数都假定为输入文件名的一部分。 这个选项
允许 Z3 读取具有奇怪名称的文件，例如：-foo.smt2。
资源中心
-T:超时
设置超时（以秒为单位）。
-t:超时
设置软超时（以毫秒为单位）。 它只会终止当前的查询。
-内存：兆字节
设置虚拟内存消耗的限制。
输出
-st 显示统计信息。
参数 设置
全局和模块参数可以在命令行中设置。 使用“z3 -p”来完成
全局和模块参数列表。
参数名称=值
用于设置全局参数。
module_name.param_name=值
用于设置模块参数。
使用 onworks.net 服务在线使用 z3
