奇怪輸出使用CTX-簡化戰術

Question

小例子如下製備：

(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)))手段？錯誤？

謝謝。

Answer 1

感謝您指出這一點。 我同意它看起來很奇怪，「和」在打印輸出中沒有任何參數。 上下文簡化器使用0個參數創建一個連接。 它被打印成簡單的「和」。 所以由ctx-simplify返回的表達式等價於（not（= x a））。 我將更新ctx-簡化策略以返回不含空連詞的表達式。