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

Я пытаюсь немного поэкспериментировать с 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 как два разных «объекта» и, следовательно, дает результат, который он дает?


algebraic-data-types smt cvc4
person ankitrokdeonsns    schedule 22.04.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я не вижу тех же результатов. Это сообщение, которое я получаю с последней разрабатываемой версией 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))

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

person Andrew Reynolds    schedule 22.04.2017
comment
Я скачал CVC4 из репозиториев Fedora. Я попробую эту версию. Спасибо. Извините за синтаксические ошибки. Спасибо - person ankitrokdeonsns; 22.04.2017