получение неизвестного результата с тривиальным forall

Я использую API z3 C++. если я создам это простое ложное выражение:

z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);

и пытаюсь решить, я получаю неизвестный результат. Я не специалист по стратегиям и тактикам, но уверен, что z3 может решить эту проблему, если использовать правильную тактику.

я тоже пробовал

z3::expr p = !z3::forall(x, x==0);

с, разумеется, тем же самым известным результатом.


c++ z3
person Giacomo Tagliabue    schedule 18.04.2013    source источник
comment
См. соответствующий вопрос: stackoverflow.com/questions/14988298/   -  person Leonardo de Moura    schedule 19.04.2013

Ответы (1)


arrow_upward
0
arrow_downward

Я не знаком с z3, но с общей точки зрения C++, не будет ли x==0 сначала выполнять оценку, т.е. разве ваш вызов не будет эквивалентен implies(x, 1)? Из быстрого поиска кажется, что вам, возможно, придется построить каждую часть оператора как объект z3, например:

Z3_ast consequent = Z3_mk_eq(ctx, x, 0);
Z3_ast theorem = Z3_mk_implies(ctx, x, consequent);

Но вышесказанное тоже неверно. Я считаю, что сами параметры x и 0 должны быть экземплярами Z3_ast, которые инкапсулируют утверждение, которое вы имеете в виду (в отличие от их интерполированных значений или ссылок).

person slackwing    schedule 18.04.2013
comment
Это неправда, это допустимая конструкция z3. Если я заменю forall на exists, оно станет истинным, как и следовало ожидать. возможно вы запутались, потому что я плохо написал выражение, извините. Я обновил его сейчас. - person Giacomo Tagliabue; 19.04.2013
comment
Хм, возможно, я действительно ошибаюсь. Но вы говорите, что z3 перегружает оператор C++ ==, а затем создает оператор из x==0 вместо его оценки? - person slackwing; 19.04.2013
comment
точно, API С++ делает это;) он переопределяет почти все - person Giacomo Tagliabue; 19.04.2013