Здравствуйте, rg45, Вы писали:

R>Ещё пара уточнений. Можно ли ввести какое-либо упорядочение элементов множества.
Да, можно. Выше я немного приврал что тип делает элементы строго отличными друг от друга. Попробую объяснить ниже.
Суть в том, что это a la дерево "symbolic calculation", в котором для узлов в процессе вычисления определяется множество вероятно принимаемых значений.
Например, в какой-то момент решатель видит что результат op(a, b)->bool. Соответственно, допустимые значения {0,1}. not({0,1})={1,0}. Порядок следования важен.
И так далее, двигаясь к корню мы в результате получаем некоторое множество (область) допустимых значений "функций" (МДЗ).
При этом, технически есть еще ограничение размера типа (битовая маска — Mask).
Грубо говоря, если у нас есть

MOV al,0a5h
SHL ax,3

То по итогу у нас Mask=11 бит, МДЗ={0x528} (технически это rax=0x528 & Mask). Теперь если сделать

AND ax,01a5h

Результатом будет Mask=16 бит, MДЗ={0x120}. Неопределенность затронутой части не играет роли. Но если бы мы _вместо_ предыдущего сделали

AND ax,0a5a5h

Результатом будет Mask=11 бит, а вот MДЗ={}, поскольку затронуты были _значимые_ неопределенные биты.
В общем, это напоминает проблемы с неинициализированной памятью в сях, обращение к которой дает неопределенный результат.

R>И допускается ли дублирование элементов. Например, можно ли добавить в множество диапазон [1-10], а потом еще отдельно, например, 3.
Дублирование элементов не критично. Их можно отсеивать со временем.

Пока писал сам осознал несколько дополнительных подводных камней. Вероятно, есть смысл посмотреть специализированные решатели типа z3 и интегрировать их.