В настоящее время я использую Z3 C ++ API для решения запросов по битовым векторам. Некоторые запросы могут содержать квантификатор существования на верхнем уровне.
Часто исключение квантификатора является простым и может быть выполнено Z3 быстро. Однако в тех случаях, когда исключение квантора возвращается к перечислению тысяч возможных решений, я бы хотел прервать эту тактику и обработать запрос самостоятельно каким-либо другим способом.
Я попытался обернуть тактику qe тактикой «попытка», надеясь, что если исключение квантификатора не удастся (скажем, 100 мс), я буду знать, что мне лучше обработать запрос каким-либо другим способом. К сожалению, тактика «попытка» не может отменить исключение квантора (для любого временного ограничения).
В старом сообщении аналогичное вопрос обсуждается, и тактика «smt» обвиняется в том, что она не реагирует. Применимы ли те же рассуждения к тактике «qe»? В том же сообщении указано, что «будущие» версии должны быть более отзывчивыми. Есть ли какой-либо способ или эвристика, чтобы определить, займет ли устранение квантификатора много времени (кроме запуска решателя в отдельном потоке и его отключения по таймауту)?
Я приложил минимальный пример, чтобы вы могли попробовать сами:
z3::context ctx;
z3::expr bv1 = ctx.bv_const("bv1", 10);
z3::expr bv2 = ctx.bv_const("bv2", 10);
z3::goal goal(ctx);
goal.add(z3::exists(bv1, bv1 != bv2));
z3::tactic t = z3::try_for(z3::tactic(ctx,"qe"), 100);
auto res = t.apply(goal);
std::cout << res << std::endl;
Спасибо!
