Ошибка при использовании операции остатка в z3py

Question

Выполнение операции с остатком выдает ошибку в коде z3py

Ниже приведен мой код

    x = Real("x")
    solve( x%2 == 3 )

Код выдает следующую ошибку:

    z3.z3types.Z3Exception: Z3 integer expression expected

, тогда как когдаЯ делаю операцию деления, она работает отлично

    solve( x/2 == 3 )

(дает ответ 6)

Не поддерживается ли операция остатка в z3?Если это так, как можно этого достичь?

Answer 1

Модуль для реальной стоимости не имеет смысла;как вещественное деление является точным.

Это имеет смысл для целых чисел.Это то, что вы хотели?(Обратите внимание, что ваше определение x означает Real.)