Как установить шаблон в переменной с помощью Z3Py

Question

Я довольно новичок в Z3, но это проблема, с которой моя проблема может быть решена. У меня есть две переменные А и В и два шаблона так: pattern_1: 1010x11x pattern_2: x0x01111 , где 1 и 0 являются биты нулем и единицей, и х (не заботятся) холодный быть Бит 0 или 1. I хотел бы использовать Z3Py для проверки того, может ли A с шаблоном_1 и B с pattern_2 быть истинным одновременно. В этом случае, если A = 10101111 и B = 10101111, чем A и B холодно, будут истинными одновременно. Может ли кто-нибудь помочь мне с этим? Можно решить эту проблему с Z3Py

Answer 1

пересмотренный ответ после уточнения

Вот один способ, которым Вы могли бы представлять эти ограничения. Существует операция, называемая Extract, которая может применяться к терминам бит-вектора. Она определяется следующим образом:

, где high является высокий бит должен быть извлечен, low это младший бит должен быть извлечен, и a является bitvector. Эта функция представляет собой биты a междуии low включительно.

Используя функцию Extract, вы можете ограничить каждый бит любого члена, который вы хотите проверить, чтобы он соответствовал шаблону. Например, если седьмой бит D должен быть 1, то вы можете написать s.add(Extract(7, 7, D) == 1). Повторите это для каждого бита в шаблоне, который не является x.