Блог

Я храню числа как z3::expr и хочу их сравнить. Я попробовал следующее:

 z3::context c; z3::expr a = c.real_val("0"); z3::expr b = c.real_val("1"); z3::expr comp = (a lt; b); std::cout lt;lt; comp.is_bool() lt;lt; std::endl; std::cout lt;lt; comp.bool_value() lt;lt; std::endl;  

Я немного сбит с толку, почему это comp.bool_value() ложь?

Если я использую решатель, все работает так, как ожидалось:

 z3::solver s(c); s.add(comp); std::cout lt;lt; s.check() lt;lt; std::endl;  

Мне приходится z3::expr сравнительно часто сравнивать, каков был бы метод голодания для этого? Использование решателя кажется мне большим количеством накладных расходов.

lt; Оператор (и почти все другие операторы) просто передает решение решателю: то есть это символьное выражение, которое не «оценивает» во время выполнения, а скорее создает выражение, которое будет выполнять сравнение при вызове решателя, над произвольными выражениями.

Сказав это, вы можете использовать упрощитель для достижения желаемого в определенных случаях. Если вы попытаетесь:

 z3::expr simpComp = comp.simplify();  std::cout lt;lt; simpComp.bool_value() lt;lt; std::endl;  

вы увидите, что он будет напечатан 1 для вас. Однако вы не должны рассчитывать на то, что упрощатель сможет уменьшить произвольные выражения, подобные этому. Для простейших случаев он справится с этой задачей, но откажется, если у вас будут более сложные выражения.

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

Примечание: В некоторых случаях вы можете создавать свои собственные функции, чтобы выполнять некоторые постоянные свертки самостоятельно. Это будет возможно Bool , например, для значений (поскольку они могут быть полностью представлены в C ) и битовых векторов различных размеров (вплоть до размера вашего машинного слова), плавающих и т. Д. Но не для вещественных чисел (потому что вещественные числа z3 имеют бесконечную точность, и вы не можете представить их непосредственно в C ), а для целых чисел (потому что они неограниченны). Но это не тривиальная вещь, и если вы не хорошо знакомы с внутренними функциями z3, я бы рекомендовал не идти по этому пути.

Итог: Если у вас много констант такого рода, посмотрите, можете ли вы перепроектировать свою программу, чтобы не создавать real_val ее в первую очередь; и сохраните их как константы и преобразуйте их в z3-выражения только тогда, когда вы больше не сможете их сохранять как таковые. На вас можно положиться simplify в определенных случаях, хотя и не ожидайте, что это будет очень эффективно.