Z3: использование операторов сравнения (<,

#c #z3 #comparison-operators

Вопрос:

Я храню числа как 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 сравнительно часто сравнивать, каков был бы метод голодания для этого? Использование решателя кажется мне большим количеством накладных расходов.

Комментарии:

1. В любом случае вы не можете избежать использования решателя, если у вас есть какие-либо переменные, поэтому измеряли ли вы «накладные расходы» при использовании решателя для статически разрешимых выражений?

2. @Botje В некоторых случаях simplify может быть в состоянии уменьшить выражения; но вы правы, что в целом это будет невозможно, пока вы не вызовете решатель и не проверите модель.

3. к вашему сведению, я сделал несколько очень простых измерений. Примерно за 5 секунд я смог (i) сравнить два двойника 2 000 000 000 раз (ii) позвонить simplify 1 000 000 раз, (iii) использовать a solver для одной и той же проблемы 1000 раз.

Ответ №1:

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 в определенных случаях, хотя и не ожидайте, что это будет очень эффективно.

Комментарии:

1.Я предполагаю, что, говоря «сохраняйте их как константы», вы имеете в виду, что я должен избегать их использования z3::expr как можно дольше, верно? Потому что, если я использую c.real_const вместо этого, я столкнусь с той же проблемой. (Кроме того, использование c.real_const simplify тоже не работает.) Или есть еще одна возможность хранить номера в z3, в которых lt; оператор будет «мгновенно» работать? К сожалению, мне приходится использовать z3::expr , потому что мне нужна точность. Однако, simplify вероятно, это сработает.

2. Это правда. Если вам нужна точность, то лучшее, что вы можете сделать, — это надеяться, что simplify это справится с нужными вам делами; хотя я бы на это не рассчитывал. (Представьте, что реальное значение является решением многочлена, например x*x == 2 . Упрощатель никоим образом не сведет это к реальной константе, хотя решатель, несомненно, сделает это.)