Параллельное решение в Z3

Question

Одной из новых функций в Z3 4.8.1 является параллельное решение:

Параллельный режим доступен для избранных теорий, включая QF_BV. Если установить значение parallel.enable=true, Z3 будет порождать количество рабочих потоков, пропорциональное количеству доступных ядер ЦП, для применения куба и решения задач.

Упоминается, что просто parallel.enable=true должен быть установлен, но я не могу найти это parallel структура в коде.

Может кто-нибудь предоставить пример кода, чтобы увидеть, как реализовать эту новую функцию?

Спасибо

Answer 1

Краткий ответ: как указывает @LeventErkok, синтаксис parallel.enable=true для использования в командной строке самого исполняемого файла z3. И, как он говорит, и ссылка @Claies указала, что если вы используете привязку, вы захотите использовать соответствующие set_param() метод. Для C++ это set_param("parallel.enable", true);

Когда я добавил это в пример привязки C++, он вывел в основном тот же результат... хотя он выдал некоторую дополнительную информацию в stderr, несколько строк вроде:

(tactic.parallel :progress 0% :closed 0 :open 1)
(tactic.parallel :progress 100% :status sat :closed 0 :open 0)

Что соответствует наблюдаемой разнице @LeventErkrok с использованием инструмента z3 для другой проблемы.

---

В нем упоминается, что нужно установить justrallel.enable=true, но я не могу найти эту параллельную структуру в коде.

(Мне было любопытно, что же такое Z3, поэтому я также отправился искать в источниках C++ файл Parallel.enable. Так вот, откуда мой ответ начался, прежде чем люди, которые знали больше, ответили. Мои выводы оставлены здесь для всех, кто интересуется...)

Длинный ответ: Если вы просматриваете источники для самого z3, вы не найдете объект C++ с именем parallel где бы ты написал parallel.enable = true;, Это свойство хранится в объекте конфигурации, управляемом строковыми именами. Этот объект конфигурации называется parallel_params это не в GitHub, потому что он генерируется как часть процесса сборки, в src/solver/parallel_params.hpp

Спецификация для этих свойств и их значений по умолчанию для каждого модуля в .pyg файл. Это всего лишь Python, который загружается процессом подготовки сборки и eval () d с несколькими определенными вещами. Параметры параллельного решателя находятся в src/solver/parallel_params.pyg Например:

def_module_params('parallel',
    description='parameters for parallel solver',
    class_name='parallel_params',
    export=True,
    params=(
        ('enable', BOOL, False, 'enable parallel solver ...'),
        ('threads.max', UINT, 10000, 'caps maximal number of threads ...'),
        # ...etc.

Если вы хотите изменить эти значения по умолчанию при сборке z3, похоже, что вы должны отредактировать .pyg файл, как кажется, нет параметризации для чего-то вроде python scripts/mk_make.py parallel.enable=true,

В качестве примера того, как изменение этого файла влияет на сгенерированный заголовок, определяющий параллельные свойства, я непосредственно изменил parallel_params.pyg сказать "True" вместо "False" для его значения по умолчанию. Следствием стало следующее двухстрочное сравнение с созданным src/solver/parallel_params.hpp файл:

-- a/src/solver/parallel_params.hpp
+++ b/src/solver/parallel_params.hpp
@@ -9,7 +9,7 @@ struct parallel_params {
   parallel_params(params_ref const & _p = params_ref::get_empty()):
      p(_p), g(gparams::get_module("parallel")) {}
   static void collect_param_descrs(param_descrs & d) {
-    d.insert("enable", CPK_BOOL, "enable parallel solver by default on selected tactics (for QF_BV)", "false","parallel");
+    d.insert("enable", CPK_BOOL, "enable parallel solver by default on selected tactics (for QF_BV)", "true","parallel");
     d.insert("threads.max", CPK_UINT, "caps maximal number of threads below the number of processors", "10000","parallel");
     d.insert("conquer.batch_size", CPK_UINT, "number of cubes to batch together for fast conquer", "100","parallel");
     d.insert("conquer.restart.max", CPK_UINT, "maximal number of restarts during conquer phase", "5","parallel");
@@ -23,7 +23,7 @@ struct parallel_params {
      REG_MODULE_PARAMS('parallel', 'parallel_params::collect_param_descrs')
      REG_MODULE_DESCRIPTION('parallel', 'parameters for parallel solver')
   */
-  bool enable() const { return p.get_bool("enable", g, false); }
+  bool enable() const { return p.get_bool("enable", g, true); }
   unsigned threads_max() const { return p.get_uint("threads.max", g, 10000u); }
   unsigned conquer_batch_size() const { return p.get_uint("conquer.batch_size", g, 100u); }
   unsigned conquer_restart_max() const { return p.get_uint("conquer.restart.max", g, 5u); }

Answer 2

Из командной строки

Если вы используете исполняемый файл z3, вы просто передаете настройку в командной строке. То есть, если ваш скрипт находится в файле a.smt2, используйте:

 z3 parallel.enable=true a.smt2

и z3 будет использовать параллельный решатель при обработке эталона. Например:

$ cat a.smt2
(set-logic QF_AUFBV )
(set-option :produce-models true)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(assert (bvult a b))
(check-sat)
(get-model)

Обычный звонок:

$ z3 a.smt2
sat
(model
  (define-fun a () (_ BitVec 32)
    #x00000000)
  (define-fun b () (_ BitVec 32)
    #x00000001)
)

Параллельный режим:

$ z3 parallel.enable=true a.smt2
(tactic.parallel :progress 0% :closed 0 :open 1)
(tactic.parallel :progress 100% :status sat :closed 0 :open 0)
sat
(model
  (define-fun a () (_ BitVec 32)
    #x00000000)
  (define-fun b () (_ BitVec 32)
    #x00000001)
)

Обратите внимание на дополнительные комментарии, касающиеся выполнения параллельного режима во втором запуске.

Программный

Если вы спрашиваете, как использовать его из программного API? Для Python это будет выглядеть так:

from z3 import *
set_param('parallel.enable', True)

Я уверен, что другие API имеют аналогичные вызовы. (Предостережение: я на самом деле не использовал / не тестировал эту функцию сам; и, поскольку она довольно новая, возможно, не все программные API поддерживают ее. Надеюсь, вы получите приятное предупреждение / ошибку, если это так!)