如何使用 Alt-Ergo 执行以下 SMT-LIB 代码答案

【问题标题】：How to execute the following SMT-LIB code using Alt-Ergo如何使用 Alt-Ergo 执行以下 SMT-LIB 代码
【发布时间】：2013-06-01 15:10:11
【问题描述】：

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

(set-logic QF_UF)
(set-option :incremental true)
(set-option :produce-models true)
(declare-fun m () Bool)
(declare-fun p () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun r () Bool)
(declare-fun al () Bool)
(declare-fun all () Bool)
(declare-fun la () Bool)
(declare-fun lal () Bool)
(declare-fun g () Bool)
(declare-fun a () Bool)
(define-fun conjecture () Bool
(and (= (and (not r) c) m) (= p m) (= b m) (= c (not g)) 
     (= (and (not al) (not all)) r) (= (and la b) al) 
     (= (or al la lal) all) (= (and (not g) p a) la) 
     (= (and (not g) (or la a)) lal)))
(push 1)
(assert (and conjecture (= a false) (= g false)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a false) (= g true)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a true) (= g true)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a true) (= g false)))
(check-sat)
(get-model)

【问题讨论】：

我已经尝试过 Windows 版本的 Alt-Ergo。它抱怨“（get-model）”。一旦我删除了这些行，我得到了应该是“sat”的未知/未饱和结果。我也尝试添加“-sat”命令行参数，但这并没有改变任何东西。奇怪！
非常感谢您的回答。你是对的，当删除“（get-model）”行时，代码在 Alt-Ergo 中运行，但生成的输出是错误的：unsat、unsat、unsat、unsat。

标签： z3 smt cvc4 alt-ergo mathsat

【解决方案1】：

目前，Alt-Ergo 不完全支持 SMT-2 格式。特别是，命令 get-model 无法识别。

此外，push 和 pop 命令被忽略。这就是为什么 Alt-Ergo 在给定的代码上说 sat, unsat, ..., unsat（当 get-model 被删除时）。

【讨论】：