0

我正在尝试使用 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 视为两个不同的“对象”并因此给出它给出的输出？

4

1 回答 1

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))

在此输入上，带有选项“--incremental”（启用多个查询）的 cvc4 给出以下响应：

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

希望这会有所帮助，安迪

于 2017-04-22T16:25:23.567 回答