在 z3 中断言数据类型的数据类型时出错

【问题标题】：error asserting datatype of datatype in z3在 z3 中断言数据类型的数据类型时出错
【发布时间】：2013-12-04 12:49:26
【问题描述】：

我有这个问题：

(set-option :print-success true)
(declare-datatypes () (( Data nil (cons (giorno Int) (mese Int)(anno Int) ))))
(declare-datatypes () (( Eta  (cons1  (data Data) (io Int)))))
(assert (forall ( (e Eta) )
(and (< 0 ((giorno data) e)) (> 0 ((giorno data) e))
) ) )
(check-sat)

然后 z3 回复我这个：

Z3(7, 12): 错误: 无效的限定/索引标识符，'_' 或 'as' 预期

我该如何解决这个问题？

【问题讨论】：

标签： z3 smt

【解决方案1】：

我认为正确的代码是

(set-option :print-success true)
(declare-datatypes () (( Data nil (cons (giorno Int) (mese Int)(anno Int) ))))
(declare-datatypes () (( Eta  (cons1  (data Data) (io Int)))))
(assert (forall ( (e Eta) )
(and (< 0 (giorno (data e))) (> 0 (giorno (data e))))))
(check-sat)

输出是

success 
success 
success 
success 
unsat

【讨论】：