Проблема при настройке параллельного Z3 с использованием z3 ‹smt2-file › CC_NUM_THREADS=3

Проблема при настройке параллельного Z3 с использованием z3 CC_NUM_THREADS=3

Я пытаюсь запустить параллельную версию z3 с CC_NUM_THREADS = 3 для моего файла smt2, появляется следующая ошибка.

ERROR: unknown parameter 'cc_num_threads'
Legal parameters are:
 auto_config (bool) (default: true)
 debug_ref_count (bool) (default: false)
 dump_models (bool) (default: false)
 memory_high_watermark (unsigned int) (default: 0)
 memory_max_alloc_count (unsigned int) (default: 0)
 memory_max_size (unsigned int) (default: 0)
 model (bool) (default: true)
 model_validate (bool) (default: false)
 proof (bool) (default: false)
 rlimit (unsigned int) (default: 4294967295)
 smtlib2_compliant (bool) (default: false)
 timeout (unsigned int) (default: 4294967295)
 trace (bool) (default: false)
 trace_file_name (string) (default: z3.log)
 type_check (bool) (default: true)
 unsat_core (bool) (default: false)
 verbose (unsigned int) (default: 0)
 warning (bool) (default: true)
 well_sorted_check (bool) (default: false)

person praveen gundaram    schedule 04.11.2016    source источник


Ответы (1)


Эта функция больше не поддерживается (и не поддерживается уже давно). Вы можете разработать свою собственную параллельную тактику, см., например, пример пар-ор в разделе «Тактика» Стратегии. Учебник.

person Christoph Wintersteiger    schedule 04.11.2016