Simplfying Expression: Z3 SMT Solver

Question

Выполнение следующего запроса с Z3 решателя:

(assert (exists ((c0_s Int) (c1_s Int) (c2_s Int)) 
     (and 
     (= (+ c0 c1 c2) 5) (>= c0 0) (>= c1 1) (>= c2 1) 
     (= c0_s c0) (= c1_s (- c1 1)) (= c2_s (+ c2 1)) 
     (= c2_s 3) (= (+ c0_s c1_s) 2)  
    )) 
    ) 

    (apply (then qe ctx-solver-simplify propagate-ineqs)) 

производит следующий вывод:

(goals 
    (goal 
     (>= c0 0) 
     (<= c0 2) 
     (>= c1 1) 
     (<= c1 3) 
     (<= (+ (* (- 1) c0) (* (- 1) c1)) (- 3)) 
     (<= (+ c1 c0) 3) 
     (= c2 2) 
     :precision precise :depth 3) 
    ) 

где я ожидал результата от Z3 решателя, как это:

(goals 
    (goal 
     (>= c0 0) 
     (<= c0 2) 
     (>= c1 1) 
     (<= c1 3) 
     (= (+ c1 c0) 3) 
     (= c2 2) 
     :precision precise :depth 3) 
    ) 

Может ли кто-нибудь объяснить, почему Z3 производит такой сложный результат вместо того, что я ожидал? Есть ли способ заставить Z3 упростить этот вывод?

Answer 1

Вы можете получить более подробный ответ от члена основной группы Z3, но из моего опыта работы с решателем целочисленных чисел Z3 на низком уровне я могу дать немного интуиции относительно того, почему это происходит.

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

Ограничения, которые применяются здесь (что я знаю), которые помогают объяснить, почему вы видите это странного вида вывода, заключаются в следующем:

• Целое решатель может представлять собой ограничение равенства (= a b), как два отдельных ограничения неравенства (<= a b) и (>= a b). Вот почему вы видите два отдельных ограничения над вашими переменными в модели, а не только одно равенство.
• Целочисленный решатель переписывает вычитания или отрицательные термины как умножение на -1. Вот почему вы видите эти отрицания в своем первом ограничении и почему оператор является добавлением, а не вычитанием.
• Арифметические выражения переписываются так, что второй аргумент оператора сравнения всегда является постоянным значением.

Короче говоря, то, что вы видите, вероятно, является артефактом того, как решатель арифметической теории представляет собой внутренние ограничения.

Поскольку вывод вашего экземпляра является целью, а не моделью или доказательством, эти выражения, возможно, еще не были полностью упрощены, поскольку я считаю, что промежуточные цели не всегда упрощаются (но у меня нет опыта с этим часть решателя).