Как создать дополнительные ограничения из модели, полученной решателем в z3 Python API?

Question

Как только у меня возникнет проблема с ограничением, я хотел бы посмотреть, выполнима ли она. На основе возвращенной модели (когда она установлена) я хотел бы добавить утверждения, а затем снова запустить решатель. Однако, похоже, я неправильно понимаю некоторые типы/значения, содержащиеся в возвращаемой модели. Рассмотрим следующий пример:

      solv = z3.Solver()
n = z3.Int("n")
solv.add(n >= 42)
solv.check()  # This is satisfiable
model = solv.model()
for var in model:
    # do something
    solv.add(var == model[var])
solv.check() # This is unsat

Я ожидал бы, что после цикла у меня по существу есть два ограничения n >= 42а также n == 42, предполагая, конечно, что z3 создает модель n=42 при первом вызове. Несмотря на это, во втором звонке check()возвращается ненасыщенным. Что мне не хватает?

Примечание : при замене solv.add(var == model[var])с solv.add(var >= model[var])я получаю z3.z3types.Z3Exception: Python value cannot be used as a Z3 integer. Почему это?

Answer 1

Когда вы перебираете модель, вы не получаете переменную, которую вы можете запросить напрямую. Вы получаете внутреннее представление, которое может соответствовать константе или чему-то более сложному, например, функции или массиву. Как правило, вы должны запрашивать модель с имеющимися у вас переменными, т. е. с n. (Как в model[n].)

Вы можете решить свою непосредственную проблему следующим образом:

      for var in model:
  solve.add(var() == model[var()])

но это будет работать только при условии, что в модели есть простые переменные, т. е. нет неинтерпретируемых функций, массивов или других объектов. См. этот вопрос для подробного обсуждения: /questions/45649668/z3py-proverka-vseh-reshenij-dlya-uravneniya/45649685#45649685

Точно так же ваше второе выражение вызывает исключение, потому что while определено для произвольных объектов (хотя здесь это делается неправильно), >=нет. Итак, в каком-то смысле это «правильно» сделать здесь исключение. (То есть, ==должно было быть выброшено исключение.) Увы, привязки Python слабо типизированы, а это означает, что он попытается разобраться в том, что вы написали, не обязательно всегда делая то, что вы намеревались по пути.