Управляйте стратегией решения Z3

Question

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

eq1: x>5 
eq2: y<6 
eq3: x+y = 10 

Так что мой вопрос, является ли, например, можно было бы решить EQ1 и EQ2 первым. А затем используя результат, разрешите eq3.

assert eq1 
assert eq2 

(check-sat) 

assert eq3 
(check-sat) 
(get-model) 

, похоже, работает, но я не уверен, имеет ли смысл производительность? Может ли инкрементное решение помочь мне там? Или есть ли какая-либо другая функция z3, которую я могу использовать для разделения моей проблемы?

Answer 1

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