Как запустить следующий код SMT-LIB с помощью Alt-Ergo

Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, большое спасибо:

(set-logic QF_LIA)
(set-option :interactive-mode true) 
(set-option :incremental true)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat)
(pop 1)
(get-info :all-statistics)
(push 1)
(assert (= x w))
(check-sat)
(get-assertions)
(exit)

Запустите этот пример онлайн здесь

  1. В Z3 сообщение unsupported ; :incremental генерируется, но это не меняет вычисления и получается правильный ответ.

  2. В mathsat некоторые сообщения unsupportedгенерируются, но отображается правильный ответ.

  3. В Cvc4 код выполняется без проблем и получается правильный ответ.

  4. В Alt-Ergo код выполняется без сообщений, но неправильный ответ unsat генерируется (правильный ответ: unsat, sat).

Источник

1 ответ

Решение

Что касается Alt-Ergo и SMT-LIB2, пожалуйста, прочитайте ответ на один из ваших предыдущих постов здесь: Как выполнить следующий код SMT-LIB с помощью Alt-Ergo

Источник
Другие вопросы по тегам