(check-sat) vs (check-sat-using smt)

Question

Прочитав strategies guide от Z3 и this answer от Leo, я ожидал, что (check-sat) и (check-sat-using smt) эквивалентны. Однако при запуске Z3 4.3.2 три раза по сравнению с нашим набором тестов (230 файлов SMTLIB2) потребовалось 198 с/192 с/195 секунд с (check-sat), но 275s/283s/270s с (check-sat-using smt). Я также пробовал ночной сборщик Z3 4.4.0 d3fb5f2a4cda, и разница была аналогичной.

Почему это может быть?

немного больше информации, которая может иметь отношение:

• Windows 7 x64, Z3 x64
• Все наши тесты выполнены с auto_config false и smt.mbqi false
• Все использование кванторов и интерпретируемые функции
• Некоторые использование (нелинейная) int и/или действительная арифметика
• Все интенсивно используют блоки push-pop

Edit: То, что я в конечном счете, хотел бы сделать, это установить тайм-аут для некоторыхcheck-sat звонков, но не для всех. AFAIK, это невозможно с check-sat, но check-sat-using (using-params smt :soft_timeout $timeout) должен работать. Это правильно?

Answer 1

Предполагаю, что вы используете Z3 в файле SMT2?

В Z3 имеются средства для определения логики эталонного теста, если ни один не указан (см., Например, default_tactic.cpp). Тактика smt - это откат, когда другая тактика не применяется. Когда Z3 запускается с -v: 10, он покажет, какая (суб) -тактика запускается.

В недавнем прошлом у нас также возникли проблемы с параметрами конфигурации, которые не передавались ядру smt. Мы исправили их, но, конечно, возможно, что где-то есть ошибка.