как решить уравнение вместо того, чтобы давать одну модель в z3

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

Например, я хочу, чтобы следующее уравнение всегда было верным для любого значения a. Использование квантификатора ForAll в этом случае вернет unsat.

     a == b - c + 2

Решение, которое я ожидаю, представляет собой формулу для одной указанной переменной, в то время как упрощение не имеет дело с этим, например

     b == a + c - 2 or c == b - a + 2

Есть ли для этого какой-нибудь API? Заранее спасибо.


z3 z3py
person Pounce    schedule 09.07.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Не уверен, в чем именно заключается вопрос, но похоже, что вы хотите получить все удовлетворительные решения вместо одного удовлетворительного решения. Это можно закодировать (с помощью кванторов), но не обязательно легко решить; в зависимости от фрагмента логики, используемого в квантификаторах, Z3 может работать медленно или просто отказываться от него относительно рано (возвращая неизвестное). Для этой цели нет специального API, но в существующем API есть все части, необходимые для решения головоломки (например, используйте неинтерпретируемую функцию f для символического кодирования решения, а затем получите func_interp для f из модели.)

Для получения дополнительной информации о получении нескольких решений см. Также Z3: поиск всех подходящих моделей и Z3 Перечисление всех удовлетворительных заданий.

person Christoph Wintersteiger    schedule 02.08.2015
comment
Спасибо за ответ, возможно вопрос сбивает с толку. Предположим, у меня есть набор выражений, и цель состоит в том, чтобы выбрать некоторые выражения, чтобы формула x = y + 1 всегда была истинной. Выбрано первое выражение x = z - 3, затем я ожидаю, что z3 даст решение, которое отображает z в y + 4. Если я попытаюсь упростить формулу, у нее не будет точного значения z в качестве решения. Интересно, можно ли таким образом представить интерпретацию функций. - person Pounce; 03.08.2015