Я работаю над проблемой над массивами Bit-Vector, кодирующими логические отношения между данными разных временных рядов в разных временных масштабах, для создания синтетических данных с произвольными свойствами. Я обнаружил, что лучше всего получается постепенно добавлять ограничения для каждого временного шага, а не заставлять Z3 назначать их все сразу, но это все равно требует очень много времени. Мне было интересно, можно ли использовать Max-SMT, чтобы справиться с этим, явно заявив, что предыдущие назначения временных рядов должны оставаться одинаковыми, насколько это возможно, и, кроме того, возвращая наиболее близкую возможную модель, если определенный временной порог достигнуто, а точное решение не найдено. Однако я не думаю, что Z3 обеспечивает сочетание инкрементальности и Max-SMT. Кроме того, я не думаю, что можно заставить Z3 предоставить «наиболее близкую возможную модель» в режиме решателя.
Кто-нибудь знает инструмент, который обеспечивает эти функции?
Спасибо!
