У меня есть эта проблема:
(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): ОШИБКА: недопустимый квалифицированный/индексированный идентификатор, ожидаемый «_» или «как»
как я могу решить это?
