Получите случайные результаты от Microsoft Z3 C или C# API

Question

Мы используем Microsoft Z3 C и C# API (у меня есть 2 программы).

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

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

Обратите внимание, что я не могу напрямую использовать smt2-код. Я этот issue, люди предложили использовать параметры «random_seed» и «smt.arith.random_initial_value».

(вариант установленный: smt.arith.random_initial_value истина)
(объявлять-Const х Int)
(объявлять-Const у Int)
(утверждать (> (+ ху) 0))
(чек-сБ-используя (с помощью-PARAMS qflra: RANDOM_SEED 1))
(получить-модель)
(чек-сБ-используя (с помощью-PARAMS qflra: RANDOM_SEED 2))
(получить-модель)
(check-sat-using (using-params qflra: random_seed 3))
(get-model)

Это решение smt2 работает, и я смог проверить его с помощью boost4fun. Но эти параметры недоступны в Z3 C или C# API.

В коде C мы пытаемся установить эти параметры с помощью функции «Z3_set_param_value», я получаю предупреждение, как это.

ВНИМАНИЕ: неизвестный параметр «smt.arith.random_initial_value»
ВНИМАНИЕ: неизвестный параметр «RANDOM_SEED»

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

Answer 1

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

Эти конкретные опции, упомянутые в вопросе, также могут быть установлены через API, но они должны быть установлены на нужные объекты. Как указано в документации (комментарии в файле заголовка), Z3_set_param_value может использоваться только для тех 10 упомянутых здесь опций. Другие опции должны быть установлены на объектах Z3_params, которые позже могут быть переданы тактике и решателям, используя Z3_params_set_*. Если необходимо, их также можно установить, изменив глобальное значение по умолчанию для этих параметров через Z3_global_param_set.