Утверждения об индуктивных типах данных в CVC4

Question

Я пытаюсь немного поэкспериментировать с CVC4.

(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_UFDT)
(declare-datatypes ()
  (Color (Red) (Black))
)
(declare-const x C)
(declare-const y C)
(assert (not (= x y)))
(check-sat)
(get-value (x y))
(assert (distinct x y))
(check-sat)
(get-value (x y))

Когда я запускаю это с помощью CVC4, я получаю следующий вывод

sat
((x R) (y R))
sat
((x R) (y R))

Я смущен этим поведением этим выводом. Если я утверждаю, что x и y не должны быть равны, их значения должны быть разными, верно? То же самое в случае с четким утверждением. CVC4 рассматривает x и y как два разных "объекта" и, следовательно, дает вывод, который он дает?

Answer 1

Я не вижу таких же результатов. Вот сообщение, которое я получаю с последней версией разработки CVC4 ( http://cvc4.cs.stanford.edu/downloads/):

(error "Parse Error: stack.smt2:5.8: Sequence terminated early by token: 'Color'.

    (Color (Red) (Black))
     ^
")

В вашем примере есть несколько синтаксических ошибок, вот исправленная версия:

(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_UFDT)
(declare-datatypes () (
  (Color (Red) (Black))
))
(declare-const x Color)
(declare-const y Color)
(assert (not (= x y)))
(check-sat)
(get-value (x y))
(assert (distinct x y))
(check-sat)
(get-value (x y))

На этом входе cvc4 с опцией "--incremental" (которая включает несколько запросов) дает такой ответ:

sat
((x Red) (y Black))
sat
((x Red) (y Black))

Надеюсь, это поможет, Энди