0

小さな例を以下に示します。

(declare-datatypes () ((Type1 a b c d e g h i f k l m n o p q r s t u v w z)))
(declare-const x Type1)
(declare-const y Type1)
(assert (and (= y x) (or (and (not (= x g)) (not (= x a))) (and (or (not (= x g)) (not (= x q))) (not (= x a))))))
(apply ctx-simplify)

出力は次のとおりです。

(goals
(goal
  (= y x)
  (or (not and) (not (= x a)))
  :precision precise :depth 1)
)

どういう(or (not and) (not (= x a)))意味ですか？バグ？

ありがとうございました。

4

1 に答える 1

1

ご指摘ありがとうございます。プリントアウトで「and」が引数を取らないのは奇妙に見えることに同意します。コンテキスト単純化は、引数が 0 の論理積を作成します。単に「and」として出力されます。したがって、ctx-simplify によって返される式は (not (= xa)) と同等です。ctx-simplify タクティックを更新して、空の接続詞なしで式を返すようにします。

于 2013-04-23T15:41:02.863 に答える