В настоящее время я моделирую набор тегов (как и теги Stackoverflow) как BitVec. Я заранее знаю, какие есть все возможные теги, и у меня их 150.
Моя текущая стратегия заключалась в использовании BitVec, где каждый бит представлял данный тег. Это позволяет мне использовать BitVec в качестве набора. Но это значит, что у меня есть набор BitVecSort шириной 150 бит.
Я делаю много проверок членства и добавляю / удаляю теги, с кодом, похожим на
bitmask = 1 << property_index[value]
return my_set & bitmask == bitmask
После того, как я все заработало, я понял, что SetSort - это вещь.
Существуют ли рекомендации о том, когда я увижу выигрыш в производительности или ущерб при переходе от BitVec к SetSort? Я знаю, что SetSort построен поверх массивов BoolSort, но я все еще слишком новичок в z3, чтобы иметь представление о влиянии на производительность.
Я создаю модель проверки, которая выполняет МНОГО работы, и на ее запуск обычно уходит 20-90 минут. И я в порядке с этим. У меня ~ 10000 переменных, в основном целые числа, но несколько сотен этих «наборов». Но было бы неплохо устранить любые «ошибки новичка» с точки зрения производительности.