Как упростить объединение двух выражений: Z3 решатель

Question

Результат производится по SMT решатель:

(or (and (>= c1 2) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4)) 
    (and (>= c1 1) (<= c1 3) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4))) 

Но я ожидал что-то вроде:

(and (>= c1 1) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4) 

может кто-то наставит меня, чтобы достичь это с решателем Z3?

Ссылка: http://rise4fun.com/Z3/1Xz3

Answer 1

Z3 не поддерживает такого рода упрощения. Он не поддерживает упрощение в «нормальную форму». Напомним, что основной интерфейс для Z3 состоит в том, чтобы проверить, является ли формула выполнимой или неудовлетворительной. Вы можете задать много запросов решателю SMT, чтобы извлечь конъюнкцию, эквивалентную формуле, если вы сможете определить, какие литералы должны быть проверены на членство в соединении. Это не всегда можно сделать синтаксическим способом, как показывает ваш пример.