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

Question

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

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

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

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

Спасибо

Answer 1

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

Если вы используете исполняемый файл 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 поддерживают ее. Надеемся, что в этом случае вы получите хорошее предупреждение / ошибку!)

Answer 2

Краткий ответ: Как указывает @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 для другой проблемы.

---

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

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

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

Спецификация для этих свойств и их значений по умолчанию для каждого модуля в файле .pyg. Это просто Python, который загружается в процессе подготовки сборки и eval () 'с несколькими вещами, определенными . Параметры параллельного решателя указаны в 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); }