这是命令 cvc3，可以使用我们的多个免费在线工作站之一（例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器）在 OnWorks 免费托管提供商中运行
程序：
您的姓名
cvc3 - 自动 SMT 定理证明器
概要
CV3 [选项] ... [文件名]
商品描述
CVC3 是一个用于多排序（类型化）一阶逻辑的自动有效性检查器
内置理论，包括对量词、偏函数和的一些支持
谓词子类型。 当前的内置理论是
· 自由（又名未解释）函数和谓词符号的平等，
· 实数和整数线性算术（对非线性算术有一定支持），
· 位向量，
· 数组，
· 元组，
· 记录，
· 用户定义的归纳数据类型。
CVC3 对 CVC 中的文件进行操作 企业介绍 输入 语言选择 或者 SMTLIB 输入
语言。 如果命令行上没有给出输入文件，CVC3 读取标准输入。
配置
下面仅给出了一些最常用的选项。 有关更多详细信息，请参阅
CVC3的内置帮助（CV3 -救命）或 CVC3 网站。
-帮助]
列出用于控制 CVC3 的所有选项。 布尔选项已标记 （二）。 他们
通过前缀启用 + 并通过前缀禁用 -。 在帮助中
输出，则 当前 给出设置。 例如，输出列表
(b)-interactive 交互模式
表示交互模式已禁用。 要启用交互模式，
选项 +互动 因此被使用。 其他选项已标记 （） 对于字符串
参数，或 （ⅰ） 对于整数参数。
-版
打印 CVC3 的版本并退出。
-郎 ( |smtlib|内部) 选择使用的输入语言。 默认为
.
+int[有效]
启用交互模式。 从标准输入读取命令并进行处理
立即。
+统计数据 打印运行时统计信息。
-暂停 t
之后自动终止 CVC3 t 秒。
使用 onworks.net 服务在线使用 cvc3
