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