В Z3: как, если сформулировать условия, основанные на else (на основе оценок переменных)?

Я новичок в Z3 и до сих пор не могу найти, как выразить условные новые назначения на основе различных возможных оценок. В примере If-then-else в https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L1846 Мне все еще нужно сделать присвоение истинным или ложным, и когда я хочу сделать его истинным или ложным на основе возможных оценок другой переменной. Как я могу это сделать?

В примере оценки я хочу вычислить значение который будет использоваться для воздействия на еще не оцененные значения, которые будут проверены утверждением позже. Итак, если это так, как я могу снова вернуть модель, не оцененную с новыми (основанными на оценке) условиями, в контекст? т. е. я хочу сделать составные условия без окончательных оценок. Это возможно?


c-api z3
person user3131978    schedule 25.05.2016    source источник
comment
Ваше описание проблемы очень сложно понять. Вы хотите сказать, что тот факт, что ite_example делает ссылку на функцию Z3_mk_false, в некотором роде нежелателен?   -  person Christoph Wintersteiger    schedule 25.05.2016
comment
Я хочу, чтобы это условие = Z3_mk_false вызывалось только тогда, когда происходит какое-то условие (например: в случае, если какая-то переменная принимает определенное значение), чтобы я мог использовать условие = Z3_mk_true в других случаях (например, когда переменная принимает другие значения).   -  person user3131978    schedule 25.05.2016
comment
Смотрите мой ответ ниже. Это отвечает на ваш вопрос?   -  person Christoph Wintersteiger    schedule 25.05.2016

Ответы (1)


arrow_upward
1
arrow_downward

Следующая строка из ite_example():

ite  = Z3_mk_ite(ctx, f, one, zero)

создает выражение, которое будет оцениваться как значение (символического) термина one, если f оценивается как истинное, или, альтернативно, как любое значение zero, если f оценивается как ложное. В ite_example f всегда оценивается как false, но это может быть любой другой (символический) термин логического типа.

Например,

x = mk_int_var(ctx, "x"); 
y = mk_int_var(ctx, "y"); 
x_eq_y = Z3_mk_eq(ctx, x, y);

создаст терм с именем x_eq_y, представляющий «x = y», который имеет логическую сортировку.

person Christoph Wintersteiger    schedule 25.05.2016
comment
Я пробовал это, но когда я использовал логическую сортировку (для f), я получил это предупреждающее сообщение: недопустимое преобразование из «Z3_bool {aka int}» в «Z3_ast {aka _Z3_ast*}». И когда я подавил его с помощью -fpermissive, я получил ошибку сегментации. - person user3131978; 25.05.2016
comment
Давайте вызовем сортировку типа. Вы не можете передать тип в Z3_mk_ite, ему нужно выражение, например переменная (которая может быть какого-то типа) - person Christoph Wintersteiger; 25.05.2016
comment
Я добавил еще один пример, это проясняет ситуацию? - person Christoph Wintersteiger; 25.05.2016