Упрощенное выражение: 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. Вот почему вы видите эти отрицания в своем первом ограничении, и почему оператор является сложением вместо вычитания.
• Арифметические выражения переписываются так, что вторым аргументом оператора сравнения всегда является постоянное значение.

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

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