1

次の 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)
4

1 に答える 1

2

今のところ、Alt-Ergo は SMT-2 フォーマットを完全にはサポートしていません。特に、コマンド get-model は認識されません。

さらに、コマンド push および pop は無視されます。これが、Alt-Ergo が特定のコードで sat、unsat、...、unsat と言う理由です (get-model が削除された場合)。

于 2013-06-23T05:59:18.227 に答える